[mercury-users] Maths and contexts.
pbone at csse.unimelb.edu.au
Sat Apr 21 09:22:51 AEST 2012
On Sat, Apr 21, 2012 at 01:56:25AM +1000, Mark Brown wrote:
> Julien said it gives you compile-time checking, not that it eliminates
> run-time checking. You'll still need run-time checks if two contexts
> don't originate from the same call to make_context.
AIUI the existential types cannot be unified.
some [C] in C = some [C] in C <-> A = B.
Therefor, add(dec(C), dec(C)) = dec(C). cannot be called with two different
existentially quantified types.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 490 bytes
Desc: Digital signature
More information about the users