[Haskell-cafe] question about "singletons"

[Richard Eisenberg]

Hi TP,

You bring up a few interesting points in your email.

(A note to those who have visited this playground before: to keep things
sane, let's just pretend that the kind # doesn't exist. Of course, if you
don't know about kind #, then you're a step ahead of the rest of us! While
you're at it, forget about the kind `Constraint` also.)

* Types at kind other than * do not have any inhabitants -- in fact, some
people would hesitate to call type-like things at kind other than * types!
(Though, I will call these things types because there's just not another
good moniker. Type-level data? Type indices? Type constructors? All are
somehow lacking.) Let's start with a more familiar example: Maybe. To form
an inhabited type, we must apply Maybe to something. So, we can have values
of type (Maybe Int) and values of type (Maybe Bool), but not values of plain
old type (Maybe). That's because Maybe has kind (* -> *), not kind *.
Another way to say this is what I said above: Maybe requires something
(something at kind *, specifically) to become a proper, inhabited type. And,
even though we say `undefined` exists at all types, that's a bit of a
simplification. `undefined` exists at all types _of kind *_. The full type
of `undefined` is `forall (a :: *). a`. Thus, we can't have `undefined` at
Maybe, because Maybe is not of kind *.

This argument extends directly to where we have types derived from promoted
data constructors. The type 'Zero has kind Nat, not *, so 'Zero is
uninhabitable, even by `undefined`.

(When I first wandered down this road, I was confused by this too. Part of
the confusion was somehow deciding that * had some vague association with *
as used on the command line -- a notation that could expand to something
else. This is totally, completely, and in every way False. In at least one
other programming language [Coq], what Haskell spells * is spelled `Type`.
[Well, almost.])

When I am programming with promoted data constructors, I often find the
following definition useful:

> data Proxy a = P

With PolyKinds, the type constructor Proxy has kind `forall k. k -> *`. So,
if we need to quickly make a value associated with the type 'Zero, we can
just use `Proxy 'Zero`. Because Proxy is kind-polymorphic, this works just
fine.

Why have the restriction that kinds other than * are uninhabited? Well, for
one, (->) would be a strange beast indeed if other types could be inhabited.
What would be the kind of (->)? I don't want to think about it. We also have
the nice maxim that every type that appears to the right of a :: must be of
kind *.

* Singletons are a useful mechanism for type-level programming. But, there
is more to singletons than just defining `Sing` as you have. Instead, you
should import the definitions from GHC.TypeLits, which comes with singleton
definitions for the built-in Nat and Symbol kinds. One drawback of the
built-in Nat and Symbol kinds is that they are not recursively defined; you
can't pattern-match on them. So, if you want your own Nat, you can define a
singleton like this:

> data SNat :: Nat -> * where
>   SZero :: SNat 'Zero
>   SSucc :: SNat n -> SNat ('Succ n)

Now, you can have values that are tightly associated with types. Yay!

* Why did you get that error with `show`? Because the `Sing` type you
defined is uninhabited -- not because it has a funny kind, but because it
has no constructors. So, when a `Show` instance is derived, the `show`
method just fails -- GHC knows `show` at type `Sing` cannot be called
because there are no `Sing`s. Then, when you subvert this logic by using
`undefined`, the derived `show` method doesn't quite know what to do with
itself.

I hope this helps! I do have to say I'm impressed, TP, by your intrepid
path of discovery down this road. You're asking all the right questions!
Richard

-----Original Message-----
From: haskell-cafe-bounces at haskell.org
[mailto:haskell-cafe-bounces at haskell.org] On Behalf Of TP
Sent: 31 May 2013 13:58
To: haskell-cafe at haskell.org
Subject: [Haskell-cafe] question about "singletons"

Hi all,


Following a discussion on Haskell Cafe some time ago (1), Roman C. wrote:

"""
On the other hand, the type 'Succ 'Zero has kind 'Nat and doesn't have any
inhabitants — only types of kind * do.
"""

Indeed, this is what seems to occur in the following example:

-----------------------
{-# LANGUAGE DataKinds #-}

data Nat = Zero | Succ Nat
    deriving ( Show, Eq, Ord )

main = do

let one = undefined :: 'Succ 'Zero
print one
-----------------------

We obtain an error (ghc 7.6.2):
-----------------------
    Kind mis-match
    Expected kind `OpenKind', but `Succ Zero' has kind `Nat'
    In an expression type signature: Succ Zero
    In the expression: undefined :: Succ Zero
    In an equation for `one': one = undefined :: Succ Zero
-----------------------

(note that the error is slightly different in the HEAD version of GHC (2)).
Is it related to the sentence "As bottom is an inhabitant of every type
(though with some caveats concerning types of unboxed kind), bottoms can be
used wherever a value of that type would be. " found at address (3)? Here we
have a non-* kind, such that bottom would not be an inhabitant of ('Succ
'Zero). Why is this so? This seems to be an assumed choice (4), but I would
like to understand the reason for this design, which makes necessary to use
singletons, as explained at (4).

Now, if I use a singleton to make my example work, I obtain an error when
trying to make the type (Sing a) an instance of Show:

-----------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

data Nat = Zero | Succ Nat
    deriving ( Show, Eq, Ord )

data Sing :: a -> *

deriving instance Show (Sing a)

main = do

let one = undefined :: Sing ('Succ 'Zero) print one
-----------------------

The error is simply:

-----------------------
test_noinhabitant_corrected.hs: Void showsPrec
-----------------------

Why?

Thanks,

TP


References:
----------

(1):
https://groups.google.com/forum/?fromgroups#!topic/haskell-cafe/AltmX5iCFi8

(2):
-----------------------
    Expected a type, but ‛Succ Zero’ has kind ‛Nat’
    In an expression type signature: Succ Zero
    In the expression: undefined :: Succ Zero
    In an equation for ‛one’: one = undefined :: Succ Zero
-----------------------

(3):
http://www.haskell.org/haskellwiki/Bottom

(4):
http://hackage.haskell.org/trac/ghc/wiki/TypeNats/Basics

"""
Both numeric and symbol literal types are empty---they have no inhabitants.
However, they may be used as parameters to other type constructors, which
makes them useful. 
"""

"""
A singleton type is simply a type that has only one interesting inhabitant.
"""



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe at haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 5494 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130531/77e7ff87/attachment.bin>