[Haskell-cafe] Re: Type equality proof

Ashley Yakeley ashley at semantic.org
Wed Mar 18 12:12:05 EDT 2009

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:


Ashley Yakeley

More information about the Haskell-Cafe mailing list