[mercury-users] Maths and contexts.

[Julien Fischer]

On Sat, 21 Apr 2012, Paul Bone wrote:

> 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.

Yes, hence Mark's point about it still requiring runtime checks,
specifically a check for when two different "some [C] C" are
semantically identical.  If you don't mind living with the additional
restriction that all uses of given context must originate from a single
call then you can do away with the runtime checks entirely.

I would expect that doing some calculation with respect to a single
context is the most common use case and that the additional restriction
is not too onerous in practice.

Julien.

--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------