[mercury-users] Maths and contexts.

[Julien Fischer]

On Sat, 21 Apr 2012, Paul Bone wrote:

> On Sat, Apr 21, 2012 at 02:20:55PM +1000, Julien Fischer wrote:
>>
>> 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.
>
> I don't understand where the runtime checks come from.  I thought that if I
> have two different some [C] dec(C). such as.
>
> X :: some [c] dec(C)
> Y :: some [C] dec(C)
>
> then this is as good as.
>
> X :: dec(A)
> Y :: dec(B)
>
> and therefore I can't call.
>
> Z = add(X, Y)
>
> because A and B can't be unified in the call to add.  (the call
> is not type correct).  And therefore cannot be compiled.

That's all true.  The runtime checks are only necessary in the case
where you wish to be able to do calcuations using numbers associated
with contexts created at two or more different call sites but that are
otherwise identical.  If you don't want to allow that then the runtime
checks aren't necessary (so far as I can see), you just won't be able to
mix numbers associated with identical contexts that originate from
different calls to make_context.

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