[Haskell-cafe] question about "singletons"

[Richard Eisenberg]

On Jun 1, 2013, at 8:18 PM, TP wrote:

> 
> In other words, bottom can be an inhabitant of a concrete type, not a type 
> constructor, which I can understand. But a type of kind Nat is a concrete 
> type, so why bottom cannot be an inhabitant of this type?
> 
>> We also have the nice maxim that every type that appears to the right of a
>> :: must be of kind *.
> 
> This is a rule set into Haskell, but why not a type of kind Nat, which is a 
> concrete type?
> 

There are three explanations I can think of here:
- What would the inhabitants of 'Zero be, for example? Not Zero, because Zero is of type Nat, not of type 'Zero. So, something else would have to be in type 'Zero… but what? The only thing I can think of is bottom. If a type's only inhabitant is bottom, then a term of that type is inherently uninteresting, as it can be only one thing, and that thing is inherently uninteresting, as I elaborate below.

- One of the interesting details of Haskell is that (->) is just another type constructor. It's a little more baked in than, say, Maybe, but the syntax of the language treats (->) as the same as Maybe. Specifically, (->) has a kind, and it is (* -> * -> *). That is, (->) takes two concrete types and produces a third concrete type. This is as we expect. (Again, ignore strange things like the kind # here.) This "ordinariness" of (->) is why, for example, we can define a Monad instance for ((->) r), which is of kind (* -> *), as Monads must be. If expressions of types of non-* kinds could be allowed, we would have to do something much stranger with the kind of (->) to be able to pass such expressions between functions. Pure kind polymorphism wouldn't quite work, because we want to prohibit "non-concrete" types (as TP has used the term "concrete") such as Maybe, being on either side of an arrow.

- The type system of Haskell is based on theoretical work that resolutely assumes that types of non-* kind are uninhabited. While it is possible to stretch imagination to allow types like 'Zero to be inhabited, the designers of Haskell would have a lot of work to do to prove that the new language is actually type-safe.

> I can understand that if indeed the definition of undefined is `forall (a :: 
> *). a` (see above), undefined is not suitable to represent ”bottom” for a 
> type of kind Nat. But I don't see why there cannot be a bottom in a type of 
> kind Nat; isn't it more a limitation related to the Haskell definition of 
> "undefined" that prevents "undefined" to be used to mean "bottom" in Haskell 
> for a type of kind different from `*`?

I hope I've addressed this above. Technically, yes, we could have a different definition of undefined, but it would fly in the face of a lot of theory about type-safe programming languages. This is not to say that such a thing is impossible, but just perhaps imprudent.

> I think I understand what you say, but I am not sure to understand the 
> reason. For example, consider the trivial examples in part (1) of Post 
> Scriptum below. We have a concrete type Foo clearly of kind `*`, so bottom 
> (undefined in Haskell) is an inhabitant of Foo. Why should I be compelled to 
> add another inhabitant (a data constructor) to get bottom printed? Bottom 
> existence is independent from other inhabitants, isn't it?

Bottom is inherently uninteresting, because you never see bottom in running code, and you can never know where bottom is lurking (other than after your program has crashed). Technically, bottom should have this definition (which is perfectly valid Haskell):

> bottom :: a
> bottom = bottom

In other words, bottom is infinite recursion -- a term that never finishes evaluating. Let's say a show method tried to print its argument and its argument is bottom. Well, that method would have to examine its argument and would immediately fall into an infinite loop. Bottom is a little like Medusa when you have no mirrors around. Once you look at it, it's too late.

In Haskell, we don't usually use bottom in this way; we use undefined. undefined masquerades as bottom, but instead of forcing a running program into an infinite loop, looking at undefined causes a running program to instantly terminate. This is generally much nicer than an infinite loop, but this niceness is simply a convenience that the compiler gives us. From a theoretical point of view, a hung program is much cleaner. To recover the consistency of the theory, Haskell provides no way to recover from a discovery of undefined in a running program. (GHC has implemented an exception that allows exception-handling code, written in the IO monad, to catch a use of undefined, but I would be highly suspicious of code that used this feature.)

So, all of this is to say that undefined is entirely uninteresting, as your program can never know when it encounters one without dying.

>  I began with 
> OCaml, but switched rapidly to Haskell (for reasons that seems derisory to 
> you: mainly the syntax closer to Python that I know well, the possibility to 
> print values at data level automatically by deriving Show instances, and the 
> GREAT wiki of Haskell).

These are fine reasons to choose a language, especially if you're just starting out. In the end, programming is a practical pursuit, and these are very practical reasons. It can be easy for us theorists to overlook this very important point.

Richard