I still like writing the call arrow as a multi (variable) argument infix
constructor, and leaving out the function arrows. Prolog notation does not
have this problem as you could have:
call(arrow(a, arrow(b, c)), d)
Which has clear meaning, but the prefix notation is hard to read.
so you have:
a -> b -> c -> d
For arity abstract functions and
a b c => d
The arrows between a b and c seem unnecedsary, but could be included for
concrete arity. Nesting needs disambiguation, so some form of bracketing is
necessary. If () are already in use then something like:
{a b c}-> d
Would work, but some brackets would seem to be needed (and familiar bracket
symbols are more readable than letters or other symbols). You could add the
other arrows back:
{a -> b -> c} -> d
But in general all this is superficial notation, the underlying structure
remains the same.
Keean.
On 21 Mar 2015 16:43, "Matt Oliveri" <[email protected]> wrote:
> On Sat, Mar 21, 2015 at 12:20 PM, Jonathan S. Shapiro <[email protected]>
> wrote:
> > On Fri, Mar 20, 2015 at 1:23 PM, Matt Oliveri <[email protected]> wrote:
> >> Right, basically we would need some restrictions to prevent ('a-n->B)
> >> from arising, where B is a concrete, non-function type. Because that
> >> type is nonsense. To me this is a symptom of bad type syntax.
> >
> > Perhaps. But if so, then I think that the bad type syntax lies in the
> > multi-arrow function type notation. The source of the problem is that the
> > "length" of the type (the number of arrows) is indeterminate until the
> final
> > rightmost type variable is specialized.
>
> Well that's bad for your notation, since individual "-n->"s aren't
> meaningful (in the usual sense of having elements). Maybe that's what
> you're saying. Nestable function types and type variables are not a
> problem for any other type system I know of. You never really care
> what the total number of arguments a function can accept is. I
> might've said you do earlier, but I was wrong. That was before I
> realized afns need to be nestable.
>
> In other words if by "multi-arrow", you mean nesting function types,
> then no, there's nothing wrong with that.
>
> >> > But another way to look at it might be that 'a -n-> 'b tells us that
> 'b
> >> > *must* be a [multi-]arrow type that eventually includes a constituent
> =>
> >> > arrow somewhere. That is: the existence of a -n-> arrow is
> effectively a
> >> > constraint requiring that some return must occur somewhere to the
> right
> >> > of that same arrow.
> >>
> >> I suppose that perspective is workable, but I really don't like it.
> >> What's so bad about afns, which avoid this issue entirely, that you'd
> >> rather invent a new kind of constraint?
> >
> > I haven't considered afn's at all yet. At this point, I'm trying to wrap
> my
> > head around the issues. I'm planning to look at afns, but I find that I
> > internalize things best when I think about one alternative at a time.
>
> Well OK, but remember I think the current issue is an artifact of
> mixed arrow notation. So if you were to switch to afns now, rather
> than later, then I think there'd be fewer issues to wrap your head
> around.
>
> Here's a way to think about afns which is superficially similar to mixed
> arrows:
> - A call arrow is syntactically required to appear after any
> call-abstract arrows.
>
> So ('a->'b=>'c) is syntactically valid.
> ('a->'b->'c) is not. There's no call arrow after those call-abstract
> arrows.
>
> - Call-abstract arrows are not really type constructors. Groups are.
>
> You cannot parenthesize ('a->'b=>'c) as ('a->('b=>'c)). Informally,
> it's because this is saying "->" is a type constructor, and I'm
> proposing that it isn't. Technically, it's because we've made ('b=>'c)
> a subexpression (and it is a valid type) but then the outer function
> type is missing a call arrow. ('a->'b=>'c) has 3 direct
> subexpressions: 'a, 'b, and 'c. ('a->('b=>'c)) has two, and neither of
> them are the return type of the whole group, so no good. So I'm
> calling type expressions like ('a->'b=>'c) "groups", but of course
> they're just afns in disguise.
>
> ('a->'b=>'c->'d=>'e) would fully parenthesize as
> ('a->'b=>('c->'d=>'e)). Every group has exactly one call arrow.
>
> Because I've changed the notation to parse "group-wise", there's
> nothing so weird about requiring the call arrow. It's just part of the
> syntax for any group. Valid types can still be combined freely.
> Informally, requiring the call arrow is sensible because any
> application involves at least one call, one of which will be the last
> step in the application.
>
> A group has elements which are arity-abstract functions (yeah I know
> there are no canonical arity-abstract functions) which can be applied
> to arguments. Emphasis on "can be applied". We have enough information
> to check an application. We also infer a whole group from an
> application.
>
> - Groups have an appropriate number of callvars.
>
> Just like before, there's an implicit fresh callvar for each
> call-abstract arrow in a group that doesn't have an explicit callvar.
> This is unlike afns, where the whole afn has a single deep arity
> variable. But the two ways of parameterizing the type are
> interchangeable--like in the example in the table--provided we work
> group-wise.
>
> - Callvars unify the same way as before.
>
> 'a=>'b->'c=>'r
> and
> 'x->'y=>'z=>'s
>
> unify to get
> 'a=>'b=>'c=>'r
> provided 'a and 'x unify, etc.
>
> This is weirder now, since those things all have different structure.
> But I believe it still makes semantic sense.
>
> - We can instantiate however we like.
>
> We can (somewhat abusively) write a "-n->" simply as a space. This can
> look funny, like in
> 'a 'b->'c=>'r
> But whether the remaining callvar becomes y or n, we get
> 'a 'b=>'c=>'r
> or
> 'a 'b 'c=>'r
> both of which are valid arity-concrete types. But note that they have
> different structure, since only a call arrow causes the group to be
> split.
>
> - It (probably) works.
>
> Because there's a systematic translation to cfn/afn notation, and that
> system probably works.
>
> Hope you like it.
> _______________________________________________
> bitc-dev mailing list
> [email protected]
> http://www.coyotos.org/mailman/listinfo/bitc-dev
>
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
