[Haskell-cafe] Re: Type equality proof

[Ashley Yakeley]

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