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
