On 24 February 2015 at 21:11, Jonathan S. Shapiro <[email protected]> wrote:
> On Mon, Feb 23, 2015 at 2:11 PM, Keean Schupke <[email protected]> wrote: > >> On 23 February 2015 at 21:40, Jonathan S. Shapiro <[email protected]> >> wrote: >> >>> >>> fn 3 'a->'b->'c->'d >>> >>> and the number is not redundant. >>> >> >> If you write it like that (with all the arrows) its not redundant, but if >> you use argument grouping: >> >> fn 'a 'b 'c -> 'd >> >> You can express the same information without the number. >> > > I agree. But as we established in the choose_one example, we need a > syntactic position in the 'fn' construct for the arity type variable (the > one that has Nat kind). I want to stick to a consistent syntax for > arity-abstract and arity-concrete functions to avoid confusion while we are > discussing all of this. > > >> There are two types involved in any function, the type it is defined >> with, and the type where you attempt to use it. >> >> So for example: >> >> f x = \y . x + y >> >> f 1 2 >> >> we can infer the concrete type f :: fn 1 'a -> (fn 1 'a -> 'a) from the >> definition >> >> we can infer the concrete type f :: fn 2 'a -> 'a -> 'a from the call >> > > I do not agree. I have disagreed several times, and I have asked several > times that you explain this. What syntactic elements in your example of > application justify inferring that the arity of f is 2 rather than 1? I > certainly see that it is bounded by 2, but I don't agree that it is > necessarily 2. > > >> and we know that you can apply a more-curried function where a >> less-curried one is expected, so with the order on types we know: >> >> fn 1 'a -> (fn 1 'a -> 'a) is acceptable where fn 2 'a -> 'a -> 'a is >> expected, and we can make it work by removing lambdas form the definition, >> or adding applications to the call site, which represents moving from one >> type to the other, but in opposite directions. >> > > Another way to say this, which does not appeal to sub-typing, is that we > can infer your application f 1 2 to have the type > > ('arity <= 2) => fn 'arity 'a -> 'a -. 'a > > shap > This is probably saying the same thing... but it ignores deeper arities. The other side is the definition defines the lower bound on arity so you might have: ((1, 1) <= 'arity <= (2)) => fn 'arity 'a -> 'a -> 'a And then you are kind of doing the same thing, but with a more complex type system... Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
