On Tue, Mar 31, 2015 at 12:13 PM, Keean Schupke <[email protected]> wrote:
> You are right, but I would state it more like, the arrows cannot be plain HM
> arrows if the equations are all true.
As long as we agree that equations 1 and 2, and "arrows are plain HM
arrows" cannot all be true at once. :)
> Lets assume I was mistaken when I said they are HM arrows, and focus on the
> implications of the equations.
So combining intersections with what Shap was saying about (a->b->c)
and (a->(b->c)) being different _might_ work. It seems like a step in
the right direction at least, as far as semantics are concerned. This
way a type of the form
a1 -> a2 -> ... an -> rtn
_can_ be interpreted as requiring the function to be callable with n
arguments. So then intersections can combine the constraints.
However, I agree with Shap that attaching this hidden meaning to
HM-looking arrows is not good. For a while we would've written the
above type as
a1 -> a2 -> ... an => rtn
This is mixed arrow notation. The "=>" is a call arrow, and says we
can call the function with the number of arguments up to that point.
The nice thing is we can say something like (a=>b->c=>d) to require
that 1-calls and 3-calls are allowed, instead of intersecting (a->b)
with (a->b->c->d). But now we are talking about moving to different
syntax.
None of the above comments address the need for some kind of variable
to handle choose_one correctly. You're probably going to need that
too. Shap originally proposed a shallow arity variable. I proposed a
deep arity variable and argued that shallow arity wouldn't work. At
some point Shap abandoned shallow arity for some reason I don't know.
(I never recognized a point where I convinced him to.) To handle
apply2, Shap came up with the mixed arrow notation with call arrows.
Although I didn't realize it at first, each abstract arrow in the
notation has a "callvar", which is used to handle choose_one. Finally,
I convinced Shap that something like ('a->'b) in mixed arrow notation
doesn't make much sense, so we're considering various hybrid notations
between my afns and mixed arrow.
> On 31 March 2015 at 17:05, Matt Oliveri <[email protected]> wrote:
>>
>> On Tue, Mar 31, 2015 at 11:44 AM, Keean Schupke <[email protected]> wrote:
>> > Clarification, so:
>> >
>> > 1. (a -> b -> c -> d) U (a b c => d) = (a b c => d)
>> >
>> > 2. (a -> b) U (a b c => d) = _|_
>> >
>> > 3. (a -> b) U (a -> b -> c -> d) = (a =>b -> c -> d)
>>
>> (x U y) is notation for "unify x with y"? If so, then sorry, but I
>> think you're mistaken. Those equations cannot all be true if the
>> arrows are HM arrows. See my previous email.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
