4 ms·
Where does an instance of a come from in that case? A function of that type has no way to construct one.
by 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 agoYes, 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 agoThe 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.