[bitc-dev] Function arity (again)
Sandro Magi
naasking at higherlogics.com
Sat Mar 27 23:42:11 PDT 2010
On 28/03/2010 1:23 AM, Jonathan S. Shapiro wrote:
> # let multiply x y = x * y;;
> val multiply: int -> int -> int = <fun> // correct, and expected
> # let multiply2 x = (fun y -> x * y);;
> val multiply2: int -> int -> int = <fun> // correct, but undesired
>
> The problem with this is that the information about arity has been
> lost. Given that correct use of native calling conventions actually
> relies on this knowledge, it's moderately awkward to have lost it. For
> the second type, I would have preferred to see:
>
> val multiply2: int -> (int -> int) = <fun> // correct, but undesired
>
> I fully understand that the two types are mathematically identical,
> but annotating which arrow distinguishes call from return nonetheless
> seems like a good and useful thing in a systems-oriented language, and
> seems fairly harmless to those accustomed to ML/Haskell. Would people
> coming from ML/Haskell find this impossibly strange?
Interesting idea, but:
1. how does this interact with partial application? ie. can you
partially apply both types, or only the second type?
2. what is the subsumption relationship between these two function
types, if any? ie. can you pass T->T->T where one expects T->(T->T) and
vice versa, or are they completely incompatible? If there is no
compatibility, which seems likely given your goals, that leads me to
ask: why not just go with the SML tupled form?
Curried form is preferred primarily because of the ease of partial
application. If you want to control or eliminate that, or anticipate
limited use of partial application, then tupled form should be the default.
You can then introduce a convenient syntax for partial application of
tupled form, so you're now explicit in partial application too. Sounds
like exactly what you're after.
> AVOIDING ALLOCATION
>
> When partial applications are permitted, there is still a strong
> desire to avoid performing them inadvertently. Unless an explicit
> application syntax is introduced to indicate that partial application
> is intended, I see no good way to deal with this. I can see two
> sensible ways to annotate this intent:
>
> 1. With a module-level annotation indicating that the module makes
> intentional use of currying
> 2. With an explicit application syntax, e.g.
> multiply . x
>
> Given the ability to write a lambda explicitly, I'm actually not very
> convinced that partial applications are critical, and they pose a real
> danger of unintended use. Input and suggestions?
Given BitC is so strongly typed, is it really that unlikely that the
programmer wouldn't know what types he's working with at a given point
in a program? When invoking a closure, you already don't know whether
that closure will perform allocation, so I don't see any additional
danger in not knowing whether it's allocating a closure record. When
you're not invoking a closure, it seems you already have full arity
information, so there's little danger in inadvertently allocating a
closure either. Perhaps you have a specific example of the danger you're
concerned with.
I'm not actually adverse to being explicit about partial application, so
that seems reasonable if the danger is real. However, you may run into
composition issues. Consider:
module type Partial =
sig
type 'a t
val lift: ('a -> 'b) -> ('a -> 'b) t
val apply: ('a -> 'b) t -> 'a -> 'b t
end;;
Now use lift and apply with a function 'a -> 'b -> 'c, and/or 'a -> ('b
-> 'c). What would happen with your two new function types? How does
apply know when it's performing a partial application and when it's
invoking the function? Or would the developer need to supply two
separate overloads for each case? The subsumption relationship between
these two arrow types should clarify how to write a Partial-like module,
and should hint at any expressiveness problems that result.
Sandro
More information about the bitc-dev
mailing list