is identity the only polymorphic function without typeclasses?
Tue, 4 Mar 2003 16:14:06 -0600
> 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
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
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
from the list of expressions we have created, or introducing the new type
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
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
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
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
nt1: no new type constraint
nt2: no new type constraint
nt3: no new type constraint (Th new function is a constant function without
* 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.