4 ms·

> That passes the type checker just fine. I think you are running into some weird haskellisms with your Bottom-type. The normal way of defining that in haskel

> That passes the type checker just fine. I think you are running into some weird haskellisms with your Bottom-type. The normal way of defining that in haskell is using the "EmptyDataDecls" pragma, like this: {-# LANGUAGE EmptyDataDecls #-} data Empty g :: Empty -> a g x = x Which doesn't pass the type checker. (From a theoretic standpoint, I would have thought your Bottom was a essentially a type-level identity function..)

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".

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".