The time you grouped (a->b->c), you utilized the arrow type constructor to build a function type, it is no different that using a polymorphic list. I think I am not happy with the dual semantics of this arrow thingie. I have to ponder on this some more, I guess.
Thanks for the response. Greatly appreciated.
I'm not a student of type theory, but what follows is my own attempt to rigorously (per my definitions) formalize an answer. Lets forget about the undefined, bottom, error, or whatever cases and look at the following. Lets think about this inductively. First off, lets start off with something of type a. (here we don't mean that something of type forall a . a, which is a whole different type, we just mean we have something with a specific type, we just don't care what it is.) Now, with the arrow constructor we can build two new types of functions. a - > a (of which the only useful function I can see is id or a constant function which constrains the type of the 1st argument.) b -> a (which is basically a constant function.) we can continue to build new functions by either adding an existing type variable from the list of expressions we have created, or introducing the new type variable c. so now we have U: a -> a -> a V: a -> b -> a W: b -> a -> a X: b -> b -> a Y: c -> a -> a Z: c -> b -> a Analyzing the functions (U..Z) we find: U: could be any any thing similar to asTypeOf (selecting either the first or second arguments, constraining them to a single type,) or a constant valued function. V: choose first argument or constant W: choose second argument or constant. X: constant f (But could this be a very odd but perhaps minorly useful method to constrain types of certain values in some type system?) Lets call this a constant asTypeOf function Y: whoops! this is isomprophic to W Z: constant f Now, if we go on creating 3,4,...,N parameter, etc. functions, could we find anything other than functions which could not described described as some combination of the following? (Assume i is integer and z_i is just a specific argumetn number). 1: selecting asTypeOf function (with type constraint a on arguments (y_1,y_2, ...), type constraint b on arguments (z_1,z_2, ....), type constraint c ....) I am considering id as one of these, since it selects its first (and only) argument. 2: constant asTypeOf function with type constraints similar to that of case 1. 3: constant function without type constraints. This is where induction can get confusing, because we need to deal with 6 cases. existing type var on cases 1,2, and 3, and new type var on cases 1,2,and 3. I will denote the cases et1,et2,et3 and nt1,nt2,nt3 respectively. et1: just (possibly*) adds a new type constraint to new function et2: just (possibly*) adds a new type constraint to new function et3: now we have a constraint on the type, so the new function is a case 2 function. nt1: no new type constraint nt2: no new type constraint nt3: no new type constraint (Th new function is a constant function without type constraints). * I say possibly here because in the case where you selected a type var amongst the set of type vars which are already declared in your list of created functions, and add it to a function which does not have that type var, it would be the same as adding a new type var. If this is confusing, just consider cases W and Y a from few paragraphs above (where meantion, "whoops, this is isomorphic...") and maybe you'll understand what I'm trying to say. So it looks like you only get those three cases if you go by my partitioning of the kinds of functions. Jay Cox