[mercury-users] Maths and contexts.

[Paul Bone]

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.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 490 bytes
Desc: Digital signature
URL: <http://lists.mercurylang.org/archives/users/attachments/20120421/c889fda6/attachment.sig>