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

[Nicholls, Mark]

This reminds me of the thing about the typewriter and the chimpanzees and Shakespeare (though I'm not claiming what follows is Shakespearean).

> {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances, GADTs, StandaloneDeriving #-}

yep

> data Nat = Z | S Nat

Sort of know whats happening here...

> data family Sing (a :: k)

This is just about believable (though its just copied from the article)

> data instance Sing (n :: Nat) where
>   SZ :: Sing 'Z
>   SS :: Sing n -> Sing ('S n)

shorthand

> type SNat (n :: Nat) = Sing n

Yep...this at least feels grounded

> data BTree a = Leaf | Branch a (BTree a) (BTree a)

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)

shorthand

> type SBTree (n :: BTree a) = Sing n

This works (good)

> y :: SBTree ('Branch ('S ('S 'Z)) 'Leaf 'Leaf)
> y = SBranch (SS (SS SZ)) SLeaf SLeaf

This works (good)!

> z :: SBTree ('Branch 'Z 'Leaf 'Leaf)
> z = SBranch SZ SLeaf SLeaf

Even this works (v good)

> f :: SBTree ('Branch 'Z 'Leaf 'Leaf) -> Integer
> f (SBranch SZ SLeaf SLeaf) = 1

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!

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"...

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).
CONFIDENTIALITY NOTICE

This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited.

While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data.

Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us.

MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe.  MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc.  Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.