dependent types, singleton types....

older
CFP: IEEE International Conference...

Nicholls, Mark

28 Apr 2015 28 Apr '15

10:45 a.m.

Can someone check my answer (no I'm not doing an assessment...I'm actually learning stuff out of interest!) working through https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dep... still there is a section about singleton types and the exercise is "Exercise: Define the binary tree type and implement its singleton type." Ok, I think I'm probably wrong....a binary tree is something like...

...

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

With DataKind My logic goes... Leaf is an uninhabited type, so I need a value isomorphic to it.... Easy?

...

data SBTree a where SLeaf :: SBTree Leaf

Things like Branch Integer Leaf (Branch String Leaf Leaf) Are uninhabited...so I need to add

...

SBranch :: (a :: *) -> (SBTree (b :: BTree *)) -> (SBTree (c :: BTree *)) -> SBTree (Branch a b c)

? It compiles...but....is it actually correct? Things like

...

y = SBranch (SS (SS SZ)) SLeaf SLeaf z = SBranch (SS (SS SZ)) (SBranch SZ SLeaf SLeaf) SLeaf

Seem to make sense ish. From: Nicholls, Mark Sent: 28 April 2015 9:33 AM To: Nicholls, Mark Subject: sds Hello, working through https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dep... but a bit stuck...with an error...

...

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

...

data Nat = Z | S Nat

...

data Vector a n where Nil :: Vector a Z (:-) :: a -> Vector a n -> Vector a (S n) infixr 5 :-

I assume init...is a bit like tail but take n - 1 elements from the front....but...

...

init' :: Vector a ('S n) -> Vector a n init' (x :- Nil) = Nil init' (x :- xs@(_ :- _)) = x :- (init' xs)

...

zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n zipWithSame f Nil Nil = Nil zipWithSame f (x :- xs) (y :- xs@(_ :- _)) = Nil

Mark Nicholls | Senior Technical Director, Programmes & Development - Viacom International Media Networks A: 17-29 Hawley Crescent London NW1 8TT | e: Nicholls.Mark@vimn.commailto:mik@vimn.com T: +44 (0)203 580 2223 [Description: cid:image001.png@01CD488D.9204D030] 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.

Attachments:

attachment.html (text/html — 13.1 KB)
image001.png (image/png — 21.6 KB)

Show replies by date

Richard Eisenberg

29 Apr 29 Apr

7:43 a.m.

Hello Mark, Your suspicion that your singleton tree type is wrong is well-founded. The problem is that, in my opinion, that exercise is mentioned too early in the tutorial. To properly implement a singleton type for a parameterized type, like a binary tree, you will need `data family Sing (a :: k)`, as explained just a little bit further down in the post. You'll need to rewrite your definition for singleton numbers and booleans to work with `Sing` as well. Your code except the definition for SBranch is all correct. The problem with your definition is that you don't get the right information when pattern-matching. For example, say you have x with type `SBTree a`. If you successfully pattern match against `SBranch SZ SLeaf SLeaf`, you would want to learn `a ~ Branch Z Leaf Leaf`. But that's not what you'll get in your implementation: you'll get a type error saying that we don't know that `a0` is an `SNat`, where `a ~ Branch a0 Leaf Leaf`, or something like that. The type-level information is simply encoded in the wrong place for this to work out. Write back and I'll give you the full answer if this isn't enough to get you moving in the right direction! Richard On Apr 28, 2015, at 10:45 AM, "Nicholls, Mark" wrote:

...

Can someone check my answer (no I’m not doing an assessment…I’m actually learning stuff out of interest!)

working through

https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dep...

still there is a section about singleton types and the exercise is

“Exercise: Define the binary tree type and implement its singleton type.”

Ok, I think I’m probably wrong….a binary tree is something like…

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

With DataKind

My logic goes… Leaf is an uninhabited type, so I need a value isomorphic to it….

Easy?

...
data SBTree a where SLeaf :: SBTree Leaf

Things like Branch Integer Leaf (Branch String Leaf Leaf) Are uninhabited…so I need to add

...
SBranch :: (a :: *) -> (SBTree (b :: BTree *)) -> (SBTree (c :: BTree *)) -> SBTree (Branch a b c)

?

It compiles…but….is it actually correct? Things like

...
y = SBranch (SS (SS SZ)) SLeaf SLeaf z = SBranch (SS (SS SZ)) (SBranch SZ SLeaf SLeaf) SLeaf

Seem to make sense ish.

From: Nicholls, Mark Sent: 28 April 2015 9:33 AM To: Nicholls, Mark Subject: sds

Hello,

working through

https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dep...

but a bit stuck...with an error...

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

...
data Nat = Z | S Nat

...
data Vector a n where Nil :: Vector a Z (:-) :: a -> Vector a n -> Vector a (S n) infixr 5 :-

I assume init...is a bit like tail but take n - 1 elements from the front....but...

...
init' :: Vector a ('S n) -> Vector a n init' (x :- Nil) = Nil init' (x :- xs@(_ :- _)) = x :- (init' xs)

...
zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n zipWithSame f Nil Nil = Nil zipWithSame f (x :- xs) (y :- xs@(_ :- _)) = Nil

Mark Nicholls | Senior Technical Director, Programmes & Development - Viacom International Media Networks A: 17-29 Hawley Crescent London NW1 8TT | e: Nicholls.Mark@vimn.com T: +44 (0)203 580 2223

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.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

Nicholls, Mark

8:54 a.m.

Accchhhh Thats another level of pain, i'm not a big haskeller so i'll have to wrestle with it to get all the knobs and dials working, leave it with me for the moment and i'll start wrestling with cabal Excuse the spelling, sent from a phone with itty bitty keys, it like trying to sow a button on a shirt with a sausage. On 29 Apr 2015, at 12:43, Richard Eisenberg mailto:eir@cis.upenn.edu> wrote: Hello Mark, Your suspicion that your singleton tree type is wrong is well-founded. The problem is that, in my opinion, that exercise is mentioned too early in the tutorial. To properly implement a singleton type for a parameterized type, like a binary tree, you will need `data family Sing (a :: k)`, as explained just a little bit further down in the post. You'll need to rewrite your definition for singleton numbers and booleans to work with `Sing` as well. Your code except the definition for SBranch is all correct. The problem with your definition is that you don't get the right information when pattern-matching. For example, say you have x with type `SBTree a`. If you successfully pattern match against `SBranch SZ SLeaf SLeaf`, you would want to learn `a ~ Branch Z Leaf Leaf`. But that's not what you'll get in your implementation: you'll get a type error saying that we don't know that `a0` is an `SNat`, where `a ~ Branch a0 Leaf Leaf`, or something like that. The type-level information is simply encoded in the wrong place for this to work out. Write back and I'll give you the full answer if this isn't enough to get you moving in the right direction! Richard On Apr 28, 2015, at 10:45 AM, "Nicholls, Mark" mailto:nicholls.mark@vimn.com> wrote: Can someone check my answer (no I’m not doing an assessment…I’m actually learning stuff out of interest!) working through https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dep... still there is a section about singleton types and the exercise is “Exercise: Define the binary tree type and implement its singleton type.” Ok, I think I’m probably wrong….a binary tree is something like…

...

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

With DataKind My logic goes… Leaf is an uninhabited type, so I need a value isomorphic to it…. Easy?

...

data SBTree a where SLeaf :: SBTree Leaf

Things like Branch Integer Leaf (Branch String Leaf Leaf) Are uninhabited…so I need to add

...

SBranch :: (a :: *) -> (SBTree (b :: BTree *)) -> (SBTree (c :: BTree *)) -> SBTree (Branch a b c)

? It compiles…but….is it actually correct? Things like

...

y = SBranch (SS (SS SZ)) SLeaf SLeaf z = SBranch (SS (SS SZ)) (SBranch SZ SLeaf SLeaf) SLeaf

...

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

...

data Nat = Z | S Nat

...

data Vector a n where Nil :: Vector a Z (:-) :: a -> Vector a n -> Vector a (S n) infixr 5 :-

I assume init...is a bit like tail but take n - 1 elements from the front....but...

...

init' :: Vector a ('S n) -> Vector a n init' (x :- Nil) = Nil init' (x :- xs@(_ :- _)) = x :- (init' xs)

...

zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n zipWithSame f Nil Nil = Nil zipWithSame f (x :- xs) (y :- xs@(_ :- _)) = Nil

Mark Nicholls | Senior Technical Director, Programmes & Development - Viacom International Media Networks A: 17-29 Hawley Crescent London NW1 8TT | e: Nicholls.Mark@vimn.commailto:mik@vimn.com T: +44 (0)203 580 2223 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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.orgmailto:Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe 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.

Richard Eisenberg

9:42 a.m.

On Apr 29, 2015, at 8:54 AM, "Nicholls, Mark" wrote:

...

Accchhhh

Thats another level of pain

It is, unfortunately.

...

, i'm not a big haskeller so i'll have to wrestle with it to get all the knobs and dials working, leave it with me for the moment and i'll start wrestling with cabal

You won't need cabal and such. Just say `data family Sing (a :: k)` in your file and you'll have the definition. There's really nothing more to it than that! Richard

Carl Eyeinsky

2:54 p.m.

As Richard said, you don't need much of cabal for dependent types. BUT, a scenario that has worked for me is: install ghc and cabal-install from your package manager, update cabal-install via cabal ("cabal install cabal-install"), and install all else in a sandbox. Works predictably if something fails as you can just wipe the sandbox. Here is something to refer to if one wishes to go deeper :) http://www.vex.net/~trebla/haskell/sicp.xhtml On Wed, Apr 29, 2015 at 4:42 PM, Richard Eisenberg wrote:

...

On Apr 29, 2015, at 8:54 AM, "Nicholls, Mark" wrote:

...
Accchhhh

Thats another level of pain

It is, unfortunately.

...
, i'm not a big haskeller so i'll have to wrestle with it to get all the knobs and dials working, leave it with me for the moment and i'll start wrestling with cabal

You won't need cabal and such. Just say `data family Sing (a :: k)` in your file and you'll have the definition. There's really nothing more to it than that!

Richard _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

-- Carl Eyeinsky

Nicholls, Mark

30 Apr 30 Apr

9:34 a.m.

See questions below...

...

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

...

data Nat = Z | S Nat

...

data SNat n where SZ :: SNat 'Z SS :: SNat n -> SNat ('S n)

...

--type family Plus (n :: Nat) (m :: Nat) :: Nat --type instance Plus Z m = m --type instance Plus (S n) m = S (Plus n m)

...

--infixl 6 :+

...

--type family (n :: Nat) :+ (m :: Nat) :: Nat --type instance Z :+ m = m --type instance (S n) :+ m = S (n :+ m)

...

--type family (n :: Nat) :* (m :: Nat) :: Nat --type instance Z :* m = Z --type instance (S n) :* m = (n :* m) :+ m

...

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

...

data SBTree a where SLeaf :: SBTree 'Leaf SBranch :: (a :: *) -> (SBTree (b :: BTree *)) -> (SBTree (c :: BTree *)) -> SBTree ('Branch a b c)

ok so this does work...

...

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

but this doesnt.

...

f :: SBTree a -> Integer f (SBranch SZ SLeaf SLeaf) = 1

but (for me) the important thing to work out is what's actually wrong....i.e. walk before I run and land on my face I struggle with Haskell errors. it says exerviceOnDependentTypes.lhs:42:14: Could not deduce (a1 ~ SNat t0) from the context (a ~ 'Branch a1 b c) bound by a pattern with constructor SBranch :: forall a (b :: BTree *) (c :: BTree *). a -> SBTree b -> SBTree c -> SBTree ('Branch a b c), in an equation for 'f' at exerviceOnDependentTypes.lhs:42:6-27 'a1' is a rigid type variable bound by a pattern with constructor SBranch :: forall a (b :: BTree *) (c :: BTree *). a -> SBTree b -> SBTree c -> SBTree ('Branch a b c), in an equation for 'f' at exerviceOnDependentTypes.lhs:42:6 In the pattern: SZ In the pattern: SBranch SZ SLeaf SLeaf In an equation for 'f': f (SBranch SZ SLeaf SLeaf) = 1 so its trying to work out what? "a" is valid in "SBTree a" in the context of the function definition "f (SBranch SZ SLeaf SLeaf) = 1" ? so "a" ~ "Branch a1 b c" from the defintion "SBranch :: (a :: *) -> (SBTree (b :: BTree *)) -> (SBTree (c :: BTree *)) -> SBTree ('Branch a b c)"? and it wants to deduce that "a1 ~ SNat t0"? why? Why does it care? (is this my OO type head getting in the way) Mark Nicholls | Senior Technical Director, Programmes & Development - Viacom International Media Networks A: 17-29 Hawley Crescent London NW1 8TT | e: Nicholls.Mark@vimn.com T: +44 (0)203 580 2223 -----Original Message----- From: Richard Eisenberg [mailto:eir@cis.upenn.edu] Sent: 29 April 2015 2:43 PM To: Nicholls, Mark Cc: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] dependent types, singleton types.... On Apr 29, 2015, at 8:54 AM, "Nicholls, Mark" wrote:

...

Accchhhh

Thats another level of pain

It is, unfortunately.

...

, i'm not a big haskeller so i'll have to wrestle with it to get all the knobs and dials working, leave it with me for the moment and i'll start wrestling with cabal

You won't need cabal and such. Just say `data family Sing (a :: k)` in your file and you'll have the definition. There's really nothing more to it than that! Richard 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.

Richard Eisenberg

11:41 a.m.

See below. On Apr 30, 2015, at 9:34 AM, "Nicholls, Mark" wrote:

...

but this doesnt.

...
f :: SBTree a -> Integer f (SBranch SZ SLeaf SLeaf) = 1

but (for me) the important thing to work out is what's actually wrong....i.e. walk before I run and land on my face I struggle with Haskell errors.

it says

exerviceOnDependentTypes.lhs:42:14: Could not deduce (a1 ~ SNat t0) from the context (a ~ 'Branch a1 b c) bound by a pattern with constructor SBranch :: forall a (b :: BTree *) (c :: BTree *). a -> SBTree b -> SBTree c -> SBTree ('Branch a b c), in an equation for 'f' at exerviceOnDependentTypes.lhs:42:6-27 'a1' is a rigid type variable bound by a pattern with constructor SBranch :: forall a (b :: BTree *) (c :: BTree *). a -> SBTree b -> SBTree c -> SBTree ('Branch a b c), in an equation for 'f' at exerviceOnDependentTypes.lhs:42:6 In the pattern: SZ In the pattern: SBranch SZ SLeaf SLeaf In an equation for 'f': f (SBranch SZ SLeaf SLeaf) = 1

so its trying to work out what? "a" is valid in "SBTree a" in the context of the function definition "f (SBranch SZ SLeaf SLeaf) = 1" ? so "a" ~ "Branch a1 b c" from the defintion "SBranch :: (a :: *) -> (SBTree (b :: BTree *)) -> (SBTree (c :: BTree *)) -> SBTree ('Branch a b c)"? and it wants to deduce that "a1 ~ SNat t0"? why?

GHC is trying to type-check the pattern `SBranch SZ SLeaf SLeaf` against the type `SBTree a`. Once GHC sees the constructor `SBranch`, it knows that `a ~ 'Branch a1 b c` for some `a1`, some `b`, and some `c`. Then, it tries to type-check the pattern `SZ` against the type `a1`. For this to type-check, GHC must be convinced that `a1 ~ SNat t0` for some `t0`. But there's no reason for GHC to believe this, so it reports an error. One may say "Well, GHC should just decide that `a1` must be `SNat t0` and get on with it." But, that is tantamount to arguing that `foo :: a -> a; foo True = False` should type-check, by saying that GHC should decide that `a` is `Bool`. It's the same thing in the `SBTree` case: we just don't know enough to assume that `a1` should be an `SNat`.

...

Why does it care? (is this my OO type head getting in the way)

This doesn't look, in particular, like a question from a recovering OO programmer. It's a good question to ask and a hard part to figure out. I hope this helps! Richard

...

Mark Nicholls | Senior Technical Director, Programmes & Development - Viacom International Media Networks A: 17-29 Hawley Crescent London NW1 8TT | e: Nicholls.Mark@vimn.com T: +44 (0)203 580 2223

-----Original Message----- From: Richard Eisenberg [mailto:eir@cis.upenn.edu] Sent: 29 April 2015 2:43 PM To: Nicholls, Mark Cc: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] dependent types, singleton types....

On Apr 29, 2015, at 8:54 AM, "Nicholls, Mark" wrote:

...
Accchhhh

Thats another level of pain

It is, unfortunately.

...
, i'm not a big haskeller so i'll have to wrestle with it to get all the knobs and dials working, leave it with me for the moment and i'll start wrestling with cabal

You won't need cabal and such. Just say `data family Sing (a :: k)` in your file and you'll have the definition. There's really nothing more to it than that!

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

Nicholls, Mark

12:24 p.m.

Hmmm it does..... My oo compiler would say...cannot match True against "a".... or something like.....at some point you go so far out on a (mental) limb...it just snaps. Let me try to fix it all. See below. On Apr 30, 2015, at 9:34 AM, "Nicholls, Mark" wrote:

...

but this doesnt.

...
f :: SBTree a -> Integer f (SBranch SZ SLeaf SLeaf) = 1

but (for me) the important thing to work out is what's actually wrong....i.e. walk before I run and land on my face I struggle with Haskell errors.

it says

exerviceOnDependentTypes.lhs:42:14: Could not deduce (a1 ~ SNat t0) from the context (a ~ 'Branch a1 b c) bound by a pattern with constructor SBranch :: forall a (b :: BTree *) (c :: BTree *). a -> SBTree b -> SBTree c -> SBTree ('Branch a b c), in an equation for 'f' at exerviceOnDependentTypes.lhs:42:6-27 'a1' is a rigid type variable bound by a pattern with constructor SBranch :: forall a (b :: BTree *) (c :: BTree *). a -> SBTree b -> SBTree c -> SBTree ('Branch a b c), in an equation for 'f' at exerviceOnDependentTypes.lhs:42:6 In the pattern: SZ In the pattern: SBranch SZ SLeaf SLeaf In an equation for 'f': f (SBranch SZ SLeaf SLeaf) = 1

so its trying to work out what? "a" is valid in "SBTree a" in the context of the function definition "f (SBranch SZ SLeaf SLeaf) = 1" ? so "a" ~ "Branch a1 b c" from the defintion "SBranch :: (a :: *) -> (SBTree (b :: BTree *)) -> (SBTree (c :: BTree *)) -> SBTree ('Branch a b c)"? and it wants to deduce that "a1 ~ SNat t0"? why?

...

Why does it care? (is this my OO type head getting in the way)

This doesn't look, in particular, like a question from a recovering OO programmer. It's a good question to ask and a hard part to figure out. I hope this helps! Richard

...

Mark Nicholls | Senior Technical Director, Programmes & Development - Viacom International Media Networks A: 17-29 Hawley Crescent London NW1 8TT | e: Nicholls.Mark@vimn.com T: +44 (0)203 580 2223

-----Original Message----- From: Richard Eisenberg [mailto:eir@cis.upenn.edu] Sent: 29 April 2015 2:43 PM To: Nicholls, Mark Cc: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] dependent types, singleton types....

On Apr 29, 2015, at 8:54 AM, "Nicholls, Mark" wrote:

...
Accchhhh

Thats another level of pain

It is, unfortunately.

...
, i'm not a big haskeller so i'll have to wrestle with it to get all the knobs and dials working, leave it with me for the moment and i'll start wrestling with cabal

You won't need cabal and such. Just say `data family Sing (a :: k)` in your file and you'll have the definition. There's really nothing more to it than that!

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

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.

Nicholls, Mark

1:02 p.m.

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.

Richard Eisenberg

1:42 p.m.

See below. On Apr 30, 2015, at 1:02 PM, "Nicholls, Mark" 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

3676

Age (days ago)

3678

Last active (days ago)

List overview

Download

9 comments

3 participants

participants (3)

Carl Eyeinsky
Nicholls, Mark
Richard Eisenberg