4 ms·

Again, languages with a built in bottom usually have sub typing behavior that makes bottom a subtype of everything (so you can give a value of type bottom to ev

by tpush 8y ago

Again, languages with a built in bottom usually have sub typing behavior that makes bottom a subtype of everything (so you can give a value of type bottom to everything). 'forall a. a' is just how you define the bottom type in System F, which Haskell is somewhat based on. As a type it describes that a term of that type can just conjure a value of any type out of thin air, which is obviously nonsense. That what makes it the bottom type. The sub typing behavior associated with that is just the normal subsumption rule of polymorphic functions. The same reason why you can pass a function of type 'forall a. a -> a' to something expecting a function of type 'Int -> Int'. The types don't 'match' directly, but they do under the subsumption rule.

joel_ms 8y ago
Yeah, I just wanted to show that (GHC) haskell has a way of getting a type with "zero" inhabitants that actually gets caught by the type checker. (I say "zero" since of course my Empty-type above does contain non-terminating programs and (undefined :: a).) With "forall a. a" I was coming from the persepctive of intuisionistic type theory where the usual parametric polymorphism just get subsumed by Π-types and universal quantification is usually represented with Π-types, so you would have: forall a.a (Universal Quantification) <==> Π(a : Type) a (Π-type) <==> (a : Type) -> a (Agda-notation) ==> a -> a (Π-type as regular function type) where Type represents any type. That's what I meant by "type-level identity function".