[Haskell-cafe] Re: Type equality proof

[Ashley Yakeley]

Martijn van Steenbergen wrote:
> Ashley Yakeley wrote:
>> 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
> 
> Ah, nice! It seems most we came up with is already in there. Even Any 
> which I use in my project but didn't think of putting in the package is 
> there. No use anymore for a new package now, I guess. On the other hand, 
> I can't find the comm, trans, coerce, subst and resp. Would it be an 
> idea to add those to your package?

Well, trans is the same as (.), if you import Control.Category. But by 
and large you don't need those functions. You just match MkEqualType 
where you need it. Since matchWitness returns (Maybe (EqualType a b)), 
you can do this easily with "do" notation. For instance:

do
   MkEqualType <- matchWitness a1 b1
   MkEqualType <- matchWitness a2 b2
   return MkEqualType

Current code is in darcs here:
http://code.haskell.org/witness/
http://code.haskell.org/open-witness/

They now target base 4.0.

Also, my paper that explains it:
http://semantic.org/stuff/Open-Witnesses.pdf

-- 
Ashley Yakeley