I realise this is longer than it need be as I am thinking this through as I write it. You could skip straight to the conclusion underlined as "Abstract Arities" if you don't want the thinking out-loud :-)
f x y = x + y -- inferred type f :: fn 'a 'a -> 'a f x = \y . x + y -- inferred type f :: fn 'a -> fn 'a -> 'a These are types with concrete arities. Imported functions, and foreign functions get explicit concrete type signatures: import 'C' f :: fn 'a 'a -> 'a We can infer the arity of an application: (f 1) 2 -- inferred type f :: fn 'a -> fn 'a -> a (f 1 2) -- inferred type f :: fn 'a 'a -> 'a Again each of these is a concrete type we infer. So far we have everything concrete, and can only apply functions that exactly match arities, so we should agree on everything so far? Now we would like to be able to call functions with some flexibility, but we have to consider that we do not want silent allocations. We cannot allow curried application of a non-curried function as that would require allocations, but it seems okay to allow non-curried use of a curried function. To achieve this all we need is a subtyping relationship defined on function types such that more curried is a subtype of less curried. for example: fn 'a 'a 'a -> 'a :< fn 'a 'a -> fn'a -> 'a fn 'a 'a 'a -> 'a :< fn 'a -> fn 'a 'a -> 'a fn 'a 'a -> fn'a -> 'a :< fn 'a -> fn 'a -> fn 'a -> a fn 'a -> fn 'a 'a -> 'a :< fn 'a -> fn 'a -> fn 'a -> a Such hierarchies can be automatically generated by the compiler. We are find to just let applications type check, and simply generate the correct number of applications when emitting the code for the function as we always have the concrete arities from the definition/import and the application. As an optimisation, if we have access to the function definition, we can generate 'uncurried' specialisations of function definitions to make calls more efficient. As we can always make 'uncurried' specialisations locally, and we always require type-signatures to export functions, we are safe to infer the most-curried version of all types for local use (still concrete) and just allow the export statement to create the necessary specialisation. So I would change the inferred type above to: g x y = x + y -- inferred type g :: fn 'a -> fn 'a -> 'a You could then export it as: export g :: fn 'a 'a -> 'a but locally you could use: ((g 1) 2) which would use a specilised definition of f by inserting a lambda in the definition (specialising it for the applied arity) with arity (1, 1) or (g 1 2) which would create an arity (2) specialised version. You could probably even allow multiple exports like: export g :: fn 'a 'a -> 'a export g :: fn 'a -> fn 'a -> 'a In which case you could just treat them as overloads. This does introduce intersection types at the top level (g :: fn 'a 'a -> 'a /\ fn 'a -> fn 'a -> 'a), but in general top level intersections do not introduce any of the problems that more general intersection types have). Abstract Arities -------------------- So there are no abstract-arities in this description, and if I think of an abstract arity like a type class: Arity 2 => fn 'a 'a -> 'a -- It seems an abstract arity is simply the argument count of the function for its least-curried application? It allows for more-curried applications of less-curried functions which is not allowed as it introduces allocations. It seems to me that a subtyping hierarchy more naturally fits, as we want a partial-order on function types, not an abstract arity which is unordered. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
