4 ms·

Such functions can’t exist. The “C” void is expressed by the unit singleton. So it is |a|^1.

by jpfr 8y ago

Sharlin 8y ago
Yes, C void is a kinda-sorta unit type. But I’m talking about the real uninhabited type, ie. Void in Haskell, Nothing in Scala, ! (Never) in Rust. Real-world languages including Haskell are not total, so all functions a->b are in reality a->(b|Void). And for a good reason, as totality means loss of Turing completeness. In a total language, a function `a->Void` does not exist, but what about `Void->a`, then? What is the single inhabitant of that type?
- erdeszt 8y ago
  This one typechecks but loops forever: f :: Void -> a f _ = let x = x in x
- amboo7 8y ago
  It is the so-called empty function, which diverges, e.g. throws an exception if called.
- tpush 8y ago
  Since one can prove anything if you're assuming nonsense, a function of the type 'Void -> a' should be able to just return its argument. And assuming the theory is consistent(so no infinite loops etc.) this is the only instance of that function, so the cardinality is 1.
  - Sharlin 8y ago
    That makes sense, thanks!
  - maweki 8y ago
    Where does an instance of a come from in that case? A function of that type has no way to construct one.
    - theoh 8y ago
      Yes, there are no possible return values. But there is a unique vacuous total function because no return values are ever needed. A function can be considered as a set of ordered pairs, one for each value in the domain. Since there are no values in the domain, no pairs need exist. Another way to look at it is as a constrained subset of the Cartesian product of domain and codomain. In this case the domain is the empty set, so the Cartesian product is empty too.
    - tpush 8y ago
      The key is that you can (in theory, I don't know if Haskell has a proper bottom that can act as a type) give a value of Void/Bottom to anything, analogous to logic in that a proof of nonsense can be used as a proof of anything. Take this Haskell code that passes the type checker: bottom = bottom f :: Int -> a f _ = bottom Here 'bottom' has the conceptual type Void/Bottom and checks successfully against the 'a'. So assuming we have this Void type in Haskell (I don't know if Haskell has it or not), this should also type check: f :: Void -> a f x = x Just like bottom (of type Void) checked against the 'a' earlier, an argument of that type should also type check.
  - Sharlin 8y ago
    And correspondingly `a->Void` must be empty because you can’t prove a contradiction given a true proposition in a consistent system? Makes sense from the Curry-Howard point of view.
  - matt-noonan 8y ago
    The "should be able to just return its argument" part is wrong; the types pretty clearly don't match, yeah? It is true that there is a unique function of type `Void -> a` for each `a`, but that isn't it.
    - tpush 8y ago
      When the Bottom type is included in a language it usually exhibits sub typing behavior. That can be expressed in Haskell, too: {-# LANGUAGE RankNTypes #-} type Bottom = forall a. a -- zero inhabitants f :: Bottom -> a f x = x That passes the type checker just fine.
      - joel_ms 8y ago
        > 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

Such functions can’t exist. The “C” void is expressed by the unit singleton. So it is |a|^1.

by jpfr 8y ago

Such functions can’t exist. The “C” void is expressed by the unit singleton. So it is |a|^1.

Yes, C void is a kinda-sorta unit type. But I’m talking about the real uninhabited type, ie. Void in Haskell, Nothing in Scala, ! (Never) in Rust. Real-world languages including Haskell are not total, so all functions a->b are in reality a->(b|Void). And for a good reason, as totality means loss of Turing completeness. In a total language, a function `a->Void` does not exist, but what about `Void->a`, then? What is the single inhabitant of that type?

erdeszt 8y ago
This one typechecks but loops forever: f :: Void -> a f _ = let x = x in x
amboo7 8y ago
It is the so-called empty function, which diverges, e.g. throws an exception if called.
tpush 8y ago
Since one can prove anything if you're assuming nonsense, a function of the type 'Void -> a' should be able to just return its argument. And assuming the theory is consistent(so no infinite loops etc.) this is the only instance of that function, so the cardinality is 1.
- Sharlin 8y ago
  That makes sense, thanks!
- maweki 8y ago
  Where does an instance of a come from in that case? A function of that type has no way to construct one.
  - theoh 8y ago
    Yes, there are no possible return values. But there is a unique vacuous total function because no return values are ever needed. A function can be considered as a set of ordered pairs, one for each value in the domain. Since there are no values in the domain, no pairs need exist. Another way to look at it is as a constrained subset of the Cartesian product of domain and codomain. In this case the domain is the empty set, so the Cartesian product is empty too.
  - tpush 8y ago
    The key is that you can (in theory, I don't know if Haskell has a proper bottom that can act as a type) give a value of Void/Bottom to anything, analogous to logic in that a proof of nonsense can be used as a proof of anything. Take this Haskell code that passes the type checker: bottom = bottom f :: Int -> a f _ = bottom Here 'bottom' has the conceptual type Void/Bottom and checks successfully against the 'a'. So assuming we have this Void type in Haskell (I don't know if Haskell has it or not), this should also type check: f :: Void -> a f x = x Just like bottom (of type Void) checked against the 'a' earlier, an argument of that type should also type check.
- Sharlin 8y ago
  And correspondingly `a->Void` must be empty because you can’t prove a contradiction given a true proposition in a consistent system? Makes sense from the Curry-Howard point of view.
- matt-noonan 8y ago
  The "should be able to just return its argument" part is wrong; the types pretty clearly don't match, yeah? It is true that there is a unique function of type `Void -> a` for each `a`, but that isn't it.
  - tpush 8y ago
    When the Bottom type is included in a language it usually exhibits sub typing behavior. That can be expressed in Haskell, too: {-# LANGUAGE RankNTypes #-} type Bottom = forall a. a -- zero inhabitants f :: Bottom -> a f x = x That passes the type checker just fine.
    - joel_ms 8y ago
      > 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