[Haskell-cafe] Re: Type equality proof

Martijn van Steenbergen wrote:

Olá café,

With the recent generic programming work and influences from type-dependent languages such as Agda, the following data type seems to come up often:

...

data (a :=: a') where Refl :: a :=: a

Everyone who needs it writes their own version; I'd like to compile a package with this data type and related utilities, if such a package doesn't exist already (I couldn't find one). Below is what I have so far; I'd much appreciate it if you added your ideas of what else the package should contain.

Have a look at these: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/witness http://hackage.haskell.org/cgi-bin/hackage-scripts/package/open-witness -- Ashley Yakeley