On Tue, Dec 23, 2008 at 00:59:15 +0000, Ganesh Sittampalam wrote: > Just to give a (very brief!) overview of the point of IsEq: the type > witnesses stuff is designed so that the type system generally knows when > two patch contexts are the same, because they are represented by the same > type witness. Sometimes, this information (namely the equality of two > contexts) has to be propagated around the darcs code to help the type > system out, and the way we do this is with IsEq, which amounts to evidence > that two type witnesses with different names are actually the same. The > point about it is the declaration: > > data EqCheck a b where > IsEq :: EqCheck a a > NotEq :: EqCheck a b > > so if we have some value of type EqCheck a b in our hands, and we inspect > it and it turns out that it is 'IsEq', then we have a proof that a = b.
I've posted a link on this to the wiki, thanks! http://wiki.darcs.net/index.html/DarcsInternals -- Eric Kow <http://www.nltg.brighton.ac.uk/home/Eric.Kow> PGP Key ID: 08AC04F9
signature.asc
Description: Digital signature
_______________________________________________ darcs-users mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-users
