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

[Dominic Steinitz]

Nicholls, Mark <nicholls.mark <at> vimn.com> writes:

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