3 ms·
> Many practical type systems (like Haskell with type classes) break it with ad-hoc polymorphism or runtime types. Haskell does not break parametricity. Any p
by tome 11mo ago
> Many practical type systems (like Haskell with type classes) break it with ad-hoc polymorphism or runtime types.
Haskell does not break parametricity. Any presence of ad-hoc polymorphism (via type classes) or runtime types (via something like Typeable, itself a type class) is reflected in the type signature and thus completely preserves parametricity.
- aatd86 11mo agoI think what they meant is that it is not purely parametric polymorphism. Not that parametricity is broken.
- tome 11mo agoHmm, maybe > most type theories don't enforce full parametricity at runtime means "sometimes types can appear at run time"? If so it's true, but it's not what I understand by "parametricity".
- aatd86 11mo agoNot sure, either : Parametric polymorphism is compile time. Adding runtime behaviors is a sort of escape hatch. Which is fair although necessary. It's not so much a breakage as it is a necessity, since non parametric code may rely on this too. Or maybe it is about constrained parametricity. In any case this doesn't seem a big issue.