A the risk of spoiling the illusion that I might have said something
clever, what I was suggesting is:

- you need to be able to infer the arity of all functions from the type
signature.

- you have some fixed arity functions (imports from other modules or
foreign functions). These need to have arity explicitly in the type.

- you can allow generalising the arities of these, or allow specific
other-arity aliases, but this should only be permitted by explicit request
as it may allocate.

- For functions defined in the same module you can specialise the
definitions to match the way the functions are applied, so it is safe to
permit generalising over arity for local functions.

That's more or less what I had in mind, but with a few tweeks as mechanisms
have become clearer.

Keean.
On 17 Feb 2015 08:00, "Jonathan S. Shapiro" <[email protected]> wrote:

On Mon, Feb 16, 2015 at 12:54 PM, Geoffrey Irving <[email protected]> wrote:

> On Mon, Feb 16, 2015 at 12:49 PM, Jonathan S. Shapiro <[email protected]>
> wrote:
> >   def perverse f a b = f a b
> >
> > we cannot determine whether f has type fn 'a -> (fn 'b -> 'c) or
> > alternatively has type fn 'a 'b -> 'c
>
> I believe that in Matt's proposal, we do know the arity of f in this
> case: it's 2.  f is applied to two arguments, so it must have type fn
> a b -> c.
>

Yes, it was Matt's proposal that we infer the arity based on the number of
arguments present. I also advocated that at one point, though elsewhere I
noted that we could use the constraint solver.

But I now think that is the wrong approach, and it further turns out that
all my noise about static definitions was wrong. We *do* need to be able to
determine arity given type, but we do *not* need to worry about the cases
whose arity we cannot statically determine. If we instead leave the arity
of those generic, then we can specialize over arity at parameters in the
same way that we specialize over other aspects of type.

I think I owe Keean an apology!

The really silly part about this is that I was even talking about allowing
arity to be captured by a Nat kind that could be generalized. It turns out
that won't quite work, because of the requirement for an AST re-write, but
I'm fairly sure that what I'm thinking about now *will* work.

Keean: is this more or less along the lines of what you were trying to say
originally? If so, I missed it because I got distracted by the initial part
of the discussion when you were saying that arity should not be part of
type. Well, that, or I just plain missed it.


shap

_______________________________________________
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

Reply via email to