On Tue, Mar 3, 2015 at 9:22 AM, Jonathan S. Shapiro <[email protected]> wrote:
> On Mon, Mar 2, 2015 at 1:45 PM, Matt Oliveri <[email protected]> wrote:
>> So adding back the "fn" is not entirely trivial. If you wanted
>> fn 'a->'b->'c->'d->'e->'r
>> to be shorthand for
>> fn 'a->(fn 'b->(fn 'c->(fn 'd->(fn 'e->'r))))
>> which, without arity abstraction, you would, then you have to
>> "ungroup" the function type...
>
> In the absence of an arity marker it's just a syntax manipulation.
Agree. I was just saying that it's not syntax manipulation handled
automatically by the parser. (I also defined "ungroup" by example.)
>> >> > that is: the conventional arity notation is a convenience shorthand
>> >> > for the fully nested one.
>> >>
>> >> What is the "conventional arity notation"?
>> >> Is that "fn 'a->'b->'c->'d->'e->'r"?
>> >> Or "fn 'arity 'a->'b->'c->'d->'e->'r"?
>> >> Or something else?
>> >
>> > I'm very sorry. The word "arity" in that sentence should have read
>> > "arrow".
>> > So:
>> >
>> > The conventional _arrow_ notation is a convenience shorthand for the
>> > fully nested one. Does that make the proposition clearer?
>>
>> Yes. But that kind of thing is below the radar for this discussion.
>
> Well, no, apparently it isn't. The confusion in the present discussion
> drives us all the way back to basics to sort things out.
So far, I don't see any evidence that I'm confused about how things in
your proposal parse. Right here we are bickering about the clearest
way of talking about lambda calculus functions, including parsing, is
all I see.
>> The parser sees them as nested. They are nested. The type system
>> doesn't need to address curried functions, as I explained above.
>
> Matt: that's your *assumption*. But in the presence of arities (which I was
> about to re-introduce), it is not at all clear that what you say is still
> the right interpretation.
I was only talking about conventional arrow notation, which doesn't
have arity. I agree that when we add arities (or just "fn"), it's no
longer true. (And I already said so.)
>> >> > So another way to look at this would be to write
>> >> > it as:
>> >> >
>> >> > f :: ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r
>> >>
>> >> Now you're getting weird. From your previous email, I thought the
>> >> point of ('arity < 5) is to prevent partial applications.
>> >
>> > Not at all! The ('arity < 5) notation means simply that there are 4
>> > arguments present, and therefore (a) the *first* concrete application
>> > may
>> > not consume more than 4 arguments nor less than 1, and (b) it's return
>> > type
>> > must be something that might account for the *rest* of the arguments (if
>> > any
>> > remain).
>>
>> But that _does_ prevent partial applications, in this case! If 'r gets
>> instantiated before 'arity, we might forget the upper bound if we
>> hadn't made it explicit. At least that's the case if you allow
>> ungrouping.
>
> Misplaced referent. If you are referring to the arity notation, that does
> NOT prevent partial applications, because it says that the application may
> consume 1, 2, 3, or 4 arguments. There is no assurance of arity agreement
> inherent in this notation.
I don't think that's an accurate criticism, but criticizing your
criticism is not a good way to explain what I meant. And since what I
meant is limited to a certain understanding of how your system works,
which may not be what you meant, let's just work our way back to this
elsewhere.
>> >> > with the intended interpretation that f is some [composition of]
>> >> > functions
>> >> > such that f takes at least four arguments, and may take more
>> >> > depending on
>> >> > how r unifies. Following the arity-free convenience syntax intuition
>> >> > above, this can be viewed as a shorthand for:
>> >> >
>> >> > f :: fn 1 'a -> fn 1 'b -> fn 1 'c -> fn 1 'd -> 'r
>> >>
>> >> Whoa, I didn't know that. I thought that type was arity-concrete (up
>> >> until you get an 'r, which may be an arity-abstract function).
>> >
>> > It is. What I'm writing here is how this would expand to a curry-style
>> > application, where all arities are concrete and all arities are 1.
>>
>> But
>> ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r
>> could concretize to
>> fn 4 int->int->int->int->bool
>> for example, and that's an incompatible concrete arity with
>> fn 1 int -> fn 1 int -> fn 1 int -> fn 1 int -> bool
>> assuming they are, in fact arity-concrete.
>
> If we are talking about the nArgs approach, then the mental model is that we
> are starting from the curried version and then using further rewrites to
> work our way up to the fn 4 version starting from the fn 1 -> fn 1 ...
> version. The idea in this notation is to follow the optimizer rewriting
> model.
>
> Yes, the two concrete arities you give are incompatible, in the sense that
> they do not unify.
Ooohhh! Well shoot, that's the mental model I don't like as much.
While I can't be sure, I think I'm closer to understanding things in
terms of instantiation, not rewriting. I don't know if that's a good
way to actually implement it, but it seems fine for working at the AST
level to design the type system.
>> So you cannot say
>> ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r
>> is shorthand for
>> fn 1 'a -> fn 1 'b -> fn 1 'c -> fn 1 'd -> 'r
>> because then they'd have to be equivalent types, but only the former
>> has the concrete-arity-4 instance.
>
> No, Matt. I switched notation here intentionally in order to use a
> completely different approach. I'm saying that:
>
> ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r
>
> is [definitionally] shorthand for
>
> fn 1 'a -> fn 1 'b -> fn 1 'c -> fn 1 'd -> 'r
>
> and that what we are then going to do is combine arities as we further
> specialize the CONCRETE function type in order to do optimizer-style
> combinings to arrive at higher arity.
OK, but you really didn't make it clear that you had just made a HUGE
change to what it was you were trying to explain.
>> > We have used several different notations. In our current notation, I
>> > would write an arity-concrete function having arity 2 as:
>> >
>> > fn 2 'a->'b->'c
>> >
>> > which is what I wrote above.
>>
>> Viewing that syntax as an arity-concrete function type seems at odds
>> with viewing "fn 'arity 'a->'b->'c->'d->'r" as shorthand. You _need_
>> to keep the argument types grouped, because you don't _know_ if it's
>> curried or not.
>
> The "2" tells me the concrete arity, so how is it that I don't know what it
> is?
To clearify, you _need_ to keep 'a, 'b, 'c, and 'd grouped under one
fn, because you don't _know_ if it will concretize to a curried
function type or not. But that's not true if you can rewrite concrete
function types, which I didn't realize you were doing.
>> > It seems to me that we haven't come to a common understanding of whether
>> > fns of any sort are nestable, and that's where we need to start.
>>
>> No, my latest thinking is that they should always be nestable.
>>
>> We need to address whether they can be ungrouped freely, like you seem
>> to be doing with
>> ('nargs >= 4) => fn 'nargs 'a->'b->'c-'d->'r
>> as shorthand for
>> fn 1 'a -> fn 1 'b -> fn 1 'c -> fn 1 'd -> 'r
>>
>> To me, that's nonsense, and the nonsense is especially clear in this
>> case, since only the latter function type has concrete arity. In fact,
>> it was because this seems so obviously nonsensical to me that I
>> assumed that "fn 1 'a -> ..." was not intended to be arity-concrete,
>> so I introduced "cfn" and "afn" to disambiguate. But it seems that's
>> not what you meant.
>
> Indeed. My intention with the 'nargs notation was to move immediately to
> concrete arity based on currying, and then explore optimizer-style rewrites.
Well, I basically said it already, but I really don't think you made
it clear that you were changing the type system to reflect that
alternative way of thinking. It caused a lot of the confusion in these
past few emails in this subthread.
I guess we'll discuss the merits of the rewrite model on the new thread.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
