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
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
