[Haskell-cafe] dependent types, singleton types....

[Richard Eisenberg]

See below.

On Apr 30, 2015, at 1:02 PM, "Nicholls, Mark" <nicholls.mark at vimn.com> wrote:

> Here we go....1st 2 lines feel ok ish....
> (now the chimps take over...tap tap boom...tap tap tap boom...hmmmm)
> 3rd line feels a bit lightweight....b & c seemingly can be anything!...but I test this naïve assumumption later.
> 
>> data instance Sing (n :: BTree a) where
>>  SLeaf :: Sing ('Leaf)
>>  SBranch :: Sing a -> Sing b -> Sing c -> Sing ('Branch a b c)

Your comment "b & c seemingly can be anything" is telling: they *can't* be anything. Types in Haskell are classified by /kinds/, in much the same way that terms are classified by types. GHC infers kinds for type variables. Let me rewrite SBranch with more kinds explicit:

> SBranch :: forall (a :: k) (b :: BTree k) (c :: BTree k).
>            Sing a -> Sing b -> Sing c -> Sing ('Branch a b c)

How does GHC infer the kinds? From the appearance of the type variables as arguments to `'Branch`. `'Branch` has kind `forall k. k -> BTree k -> BTree k -> BTree k`, where I've used `k`, as is common, to denote a kind variable. (The variable is, of course, `a` in the declaration for `Branch`.) So, when GHC sees you write `('Branch a b c)`, it can infer the correct kinds for the variables.

> 
> <snip> 
> 
> Now let's do something stupid
> 
>> a = SBranch SZ SZ SZ
> 
> BOOOM....(which is a GOOD BOOM).
> 
> exerviceOnDependentTypes.lhs:34:18:
>    Couldn't match kind 'Nat' with 'BTree Nat'
>    Expected type: Sing b
>      Actual type: Sing 'Z
>    In the second argument of 'SBranch', namely 'SZ'
>    In the expression: SBranch SZ SZ SZ
> 
> But I'm not convinced the chimp knows why!

This follows from the kinds I was talking about earlier. `SBranch` expects three arguments. The first is `Sing a`, where `a` can have *any* kind `k`. `SZ` has type `Sing Z`, where `Z` has kind `Nat`. All good. The next argument to `SBranch` has type `Sing b`, where `b` has kind `BTree k` for the *same* kind `k`. Thus, because `Z` has kind `Nat`, we know that `k` really is `Nat` in this case. The second argument to `SBranch` then has type `Sing b`, where `b` has kind `BTree Nat`. But, when you provide `SZ` there, you've given something of type `Sing Z`, and `Z` has the wrong kind. Exactly as reported in the error message. (My "exactly" there is not to mean that any of this is obvious to someone who hasn't spent a lot of time thinking about it... just that GHC got lucky here in producing something rather sensible.)

> 
> It all comes down to substituting the "b" in "'Branch a b c" with an SZ...
> It knows it's wrong.
> It knows the b in the type "'Branch" is of kind "BTree Nat"...

Try compiling with `-fprint-explicit-kinds -fprint-explicit-foralls`. Once you become accustomed to the more verbose output, it might be very helpful.

> 
> Then chimp's head hurts....
> 
> I may have forgotten what datakinds actually does...its doing more than I'm expecting...
> 
> Let me know if its horribly wrong, and I'll try and reread the exercise....(I'm doing this in between doing my proper job...which aint Haskell).

Everything so far is perfectly correct. Keep fighting the good fight. You'll be glad you did, in the end. :)

Richard