# Can literals in functional languages be thought of as functions from the empty type?

A while ago, I think on Stack Overflow, I saw someone say that Haskell literals can be thought of as functions that don't operate on anything. This makes sense to me but I remember someone else vehemently disagreeing with him.

If I understand correctly, all values in primitive types, or at least those in Bool, are type constructors, and type constructors are a special kind of function into the type. Since values like 2.87, True, or 'f' don't have any parameters passed to them it seems like it wouldn't effect the semantics of the language whether you think of them just as elements of their type or a functions from a type containing nothing into their type that always returns their value. Is there anything wrong with thinking of literals in this way?

• Do you mean functions from the unit type (i.e. the empty tuple)? In this case yes. Commented Jun 20, 2017 at 22:32
• @gallais Ah yes, I was thinking about it from the perspective of a dependent type theory where unit has one element. But this makes sense, thanks, you should turn this into an answer. Commented Jun 20, 2017 at 23:37

Let's start in a total language like Agda. Then, as gallais states, this only makes sense if by "empty type" you mean the unit type, i.e. the 0-ary tuple, which has exactly one value. The empty type can be thought of as a 0-case sum type, and has no values at all. In Agda, you can easily prove that Unit -> A is isomorphic to A. In that sense, you can consider them the same, though they still aren't literally the same. I can't, for example, do a case analysis on a Unit -> Bool nor can I apply True : Bool to anything as a function.

The story for Haskell is quite different. () -> A and A are semantically non-isomorphic types. In particular, () -> () has four values, while () has only 2. The four observationally distinct values are undefined, \_ -> undefined, \x -> x, \_ -> (). So () isn't actually a unit type, in the sense that there is exactly one function into (). (In Agda, on the other hand, we can prove that if x : Unit and y : Unit, then they are equal [definitionally so if we define Unit with the record syntax as opposed to the data syntax]. That means, Unit has only one value. Further, we can prove that Unit and A -> Unit are isomorphic for any A.)

In fact, an "empty" type like Void defined as data Void is closer to being a unit type in this sense. Void has only one value, but Void -> Void still has two. In fact, every function type A -> B, has at least two observationally distinct values, namely undefined and \_ -> undefined. Therefore, Haskell has no true unit or void type.

A lot of this is due to Haskell being a non-strict language and is exasperated by the existence of seq (and its equivalents). For example, the distinction between undefined and \_ -> undefined can only be seen with seq. If we eliminated seq and its equivalents from Haskell, then Void would serve as a unit type, though, ironically, still not as an empty type.

Usually, when people talk about such things in Haskell, they are tacitly pretending that Haskell is a better behaved language than it is. That is, they are assuming bottoms don't exist for their purposes, i.e. that you're working in a total language like Agda. For the purposes of designing your code, this is usually adequate; it's not common that we care about or expect bottoms. These distinctions can become important if we're doing something like circular programming, or if safety guarantees of our program rely on these properties, e.g. a function can never be called if it has an empty type as its domain.

• Out of curiosity, does Haskell anywhere official define the notion of a value (as opposed to a term)? Commented Jun 21, 2017 at 8:03
• @AndrejBauer As you know, Haskell doesn't have a formal semantics, so there is no formal definition of value. The Haskell Report does use the word "value" but doesn't really define it except partially in passing as it explains expressions. For example, it does explicitly say that errors/non-termination are values. Commented Jun 21, 2017 at 8:41
• Yeah, I just like to tease Haskellites about lack of an actual defintion of the language. Commented Jun 21, 2017 at 8:55
• @AndrejBauer That is indeed unfortunate. Folklore wants that there are semantics of some fragments of Haskell, but no single unifying definition. It probably grew too much to be handled with a reasonable effort: things like ST, safe coercions, eqT, GADTs, type families, very general typeclasses (incoherent?!), etc. look a bit cumbersome to handle. There could even be a return-of-investment problem here: even if one might (?) produce a formal semantics at a large cost, would it have a correspondingly large impact? Probably not. And in 2 years a new GHC extension would break it... :-(
– chi
Commented Jun 21, 2017 at 10:50
• @chi Actually, the K Framework project in general looks pretty interesting and there is an active project to provide a mechanized formulation of GHC Core in it. The work applying the K Framework to C, Java, and JavaScript seems pretty promising, and the idea behind the K Framework (and the related Matching Logic) is to increase the ROI on mechanized semantics by generating multiple tools from a common semantics. Commented Jun 21, 2017 at 11:43