On Wed, Apr 1, 2015 at 10:40 AM, Keean Schupke <[email protected]> wrote:
> Going back to this, we should get:
>
> > def keean f a b c d tst {
> > if tst
> > f a b
> > else
> > f a b c d
> > }
>
> keean : (a -?r1-> b -y-> c -?r2-> d -y-> j) -n-> a -n-> b -n-> c -n-> d
> -n-> Bool -y-> c -?r2-> d -y-> j
>
> I see now why '?r' needs to be a kind of variable, because we want to
> maintain the 'link' between arrows, so that whatever ?r2 gets bound to (n
> or y) is forced to be the same as all uses of ?r2 be the same.
>
Exactly. And now that you have agreed on this point, I think that we are
all in agreement about the technical issues here, and we are left to
consider different choices of concrete surface syntax.
> The slightly worrying thing is now arrows have 'identity' in the same way
> a type-variables are distinct.
>
I don't perceive this as a "worrying thing", because we have already
committed to this by adopting effect types. Those put exactly the same kind
of variable on the arrow.
> I guess really -?r-> is a type variable of kind * -> *, compared with a
> normal type variable that has kind '*'. Does that make sense?
>
I don't think so. I think the type variable is ?r, and the arrow type is
now a ternary constructor rather than a binary constructor. But I haven't
looked at how this is modeled in type systems that incorporate effects. If
there is a way of capturing this that is already being used in the
literature and seems vaguely sane, I'd rather not invent a new one.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
