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

[Jan Stolarek]

> the 1st link is a bit challenging...
You may want to read 3rd chapter of Okasaki's "Purely Functional Data Structures" - it describes 
weight-biased lefitsh heaps without any type-level magic.

> the 2nd I can probably cope with for the moment, though I may be asking questions.
As you probably noticed this is based on paper "Why Dependent Types Matter", so you should 
probably read the paper and follow the code.

> If you have any beginner level tutorial, then that’s even better..
I personally learned all these things in Agda. It's a bit easier because it's a fully-fledged 
dependently-typed language and things are just easier to write. Only then I moved to Haskell. 

Janek

> I can 
> just about cope with associated types, type families and GADT...some of the
> other extensions I suspect disbelief for.
>
> > What does “~” mean…(it’s something that comes out in error messages
> > when my types are all messed up)….
>
> It means GHC knows that two types are equal.
>
> > and then there’s a “=>” going on…in the middle of a signature….I know
> > “=>” in the context of “Num a => a -> a -> a”
>
> Yeah, that looks scary. You use gcastWith when you need a value of type a
> but you have a value of type b with a proof that a and b are equal (here a
> proof is a value of a :~: b). I have a practical example, though perhaps
> it's not the simplest one:
>
> https://github.com/jstolarek/dep-typed-wbl-heaps-hs/blob/master/src/TwoPass
>Merge/RankProof.hs#L361
>
> This code is thought as an intermediate level tutorial - you might want to
> give it a try. Another example I have is here (I use the name subst, but
> it's identical to gcastWith):
>
> https://github.com/jstolarek/why-dependent-types-matter/blob/master/WhyDepe
>ndentTypesMatter.hs#L220
>
> HTH
>
> Janek
>
> 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.