dependent types, singleton types....
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<mailto: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.
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" <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
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
<image001.png>
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
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 <eir@cis.upenn.edu<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" <nicholls.mark@vimn.com<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
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<mailto:mik@vimn.com> T: +44 (0)203 580 2223 <image001.png> 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<mailto: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.
On Apr 29, 2015, at 8:54 AM, "Nicholls, Mark" <nicholls.mark@vimn.com> 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
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 <eir@cis.upenn.edu> wrote:
On Apr 29, 2015, at 8:54 AM, "Nicholls, Mark" <nicholls.mark@vimn.com> 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
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" <nicholls.mark@vimn.com> 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.
See below. On Apr 30, 2015, at 9:34 AM, "Nicholls, Mark" <nicholls.mark@vimn.com> 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" <nicholls.mark@vimn.com> 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.
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" <nicholls.mark@vimn.com> 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" <nicholls.mark@vimn.com> 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.
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.
See below. On Apr 30, 2015, at 1:02 PM, "Nicholls, Mark" <nicholls.mark@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
participants (3)
-
Carl Eyeinsky -
Nicholls, Mark -
Richard Eisenberg