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?

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.

StackExchange Computer Science Q#77043, answer score: 10