On Sat, Mar 7, 2009 at 7:20 PM, Jonathan S. Shapiro <[email protected]> wrote:
> On Sat, Mar 7, 2009 at 5:16 PM, Gelf Mrogen <[email protected]> wrote:
>> It seems that if you're going to curry effectful functions,
>> the equivalence would be:
>>
>> (impure fn 'a 'b -> 'c)) == (pure fn 'a -> (impure fn 'b -> 'c))
>
> Basically, if the application is permitted to be impure, then any step
> is permitted to be impure. If the application must be pure, then all
> steps must be pure.
The equivalence Gelf proposed is true. Here is a Curry-Howard proof:
(fun f -> fun a -> fun b -> f a b) : (impure fn 'a 'b -> 'c) ->
(pure fn 'a -> (impure fn 'b -> 'c))
(fun f -> fun a b -> (f a) b) : (pure fn 'a -> (impure fn 'b ->
'c)) (impure fn 'a 'b -> 'c)
Here's a possible scheme for recovering multiparameter functions in
the implementation given a fully curried front end. I started writing
it for the previous discussion, but it also interacts with effects, so
it also applies here. This is somewhat more aggressive than the
schemes used by ocaml and haskell, in the sense that it biases towards
making more functions multiparameter and requires wrappers in some
cases where they aren't.
1. Run type inference as if everything were curried.
2. After type inference, bake in arities for all types based on signatures.
3. Make wrappers whenever this doesn't match.
If a function ends up with the signature (forall a. a -> a -> a), that
function would take two arguments. If a function has the signature
(forall a. (a -> a -> a) -> a -> a -> a), it's first argument would be
a function that takes two arguments. If you needed to pass a function
that takes one argument and returns a one argument function to a
function that takes two arguments, you'd have to make a wrapper.
This is the only scheme for curry-elimination I could think of that
handles separate compilation. Haskell resolves this by exporting two
version of every function, one with a fast multiargument calling
convention and one with a slow single curried convention, but this is
probably undesirable for BitC. It is also compatible with the normal
C convention, since the default is maximum arity.
Disadvantages include:
1. The mapping from source type to runtime type is not invariant under
parameterization. E.g., the following two functions would be compiled
differently:
let f a b = a b
let f (a : c -> d -> e) b = a b
By itself this might not be too bad, since BitC is already using
polyinstantiation. Note that these two functions would have unrelated
types in a noncurried world where (a : c d -> e).
2. With effects, this scheme doesn't compute the most general type,
since by Gelf's equivalence multiparameter functions only have effects
when fully applied.
These disadvantages are probably bad enough to kill currying, but
that's up to others.
Incidentally, by the symmetry of your type inference algorithm, saying that
a b -> c
a -> b -> c
are the same means that the language would immediately become fully
curried. I.e., I don't think there's any way to allow passing more
parameters to functions without also allowing passing less in a
Hindley Milner-style type system, due to the lack of subtyping. If we
lose full currying, we have to always pass exactly the right number of
parameters.
Geoffrey
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
