[Haskell-cafe] working my way through Data.Type.Equality...my head hurts...

[Nicholls, Mark]

Hmmm ok

And what is a singleton type!...I think this is a phrase I have chosen to ignore up to now.


> 
> 
> 
> Full code here…
> https://github.com/goldfirere/nyc-hug-oct2014/blob/master/Equality.hs
>  

...

That's a very good question. Apart from a reference in the ghc manual, I have been unable to find a reference for "~".

It doesn't exist in the Haskell 2010 Language Report, it didn’t exist in ghc 6.8.2 but made an appearance in 7.0.1. The documentation in the manual is rather sparse and doesn’t contain a reference:
https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf section 7.11. Folk on #ghc referred me to http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/. I can find papers that refer to ~ in F_C (aka FC?) but as far as I can tell not in the Haskell language itself.

Apparently:

They were introduced as part of the System Fc rewrite.

The Fc approach has the benefit of unifying a lot of the work on GADTs, functional dependencies, type and data families, etc. all behind the scenes.

Every once in a while, (~) constraints can leak into the surface language and it can be useful to be able to talk about them in the surface language of Haskell, because otherwise it isn't clear how to talk about F a ~ G b style constraints, which arise in practice when you work with type families.

I don't know if this is correct way to think about them but I think of ":~:" as internal equality and "~" as external equality and gcastWith allows you to use a proof using internal equality to discharge a proof of external equality.

For example suppose you have a type family

> type family (n :: Nat) :+ (m :: Nat) :: Nat where
>     Z   :+ m = m
>     S n :+ m = n :+ S m

and a proof

> plus_id_r :: SNat n -> ((n :+ Z) :~: n)

then you could use this with a definition of a vector

> data Vec a n where
>     Nil   :: Vec a Z
>     (:::) :: a -> Vec a n -> Vec a (S n)

to prove

> elim0 :: SNat n -> (Vec a (n :+ Z) -> Vec a n)
> elim0 n x = gcastWith (plus_id_r n) x

PS Nat and SNat are the usual natural numbers and singleton.


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe at haskell.org
http://www.haskell.org/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.