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

[Nicholls, Mark]

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 at 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 at vimn.com T: 
> +44 (0)203 580 2223
> 
> 
> 
> 
> -----Original Message-----
> From: Richard Eisenberg [mailto:eir at cis.upenn.edu]
> Sent: 29 April 2015 2:43 PM
> To: Nicholls, Mark
> Cc: haskell-cafe at haskell.org
> Subject: Re: [Haskell-cafe] dependent types, singleton types....
> 
> On Apr 29, 2015, at 8:54 AM, "Nicholls, Mark" <nicholls.mark at 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.