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
