In the definition of lambda cubes, type polymorphism is distinguished from type operators/constructors.
I have the nagging feeling that type polymorphism can be constructed through type operators using lazyness. This may be extremely convoluted but I always felt polymorphic types where just functioning "as if" waiting for a concrete type.
Here's an example...
(+1)::Num a => a -> a,
(+1) pi is
(+1) 1.1 is
This level of polymorphism above can be constructed through the use of a "universal delayed type constructor"
F and a type operator
G designed for
F :: X -> f -> a -> X a
I've tried to upper case type signatures to represent types and lower case for terms.
G :: a -> B
G ( _ ::Integral) = Integral
G ( _ ::Fractional) = Fractional
G ( _ ::Floating) = Floating
Note that G's implementation is partial, I've not actually said how
(+1)::Floating -> Floating is implemented differently from
(+1)::Integral -> Integral .
F G (+1) achieves the same as
(+1) with polymorphism above. This is a simple example, I may need to go a second level (i.e. operators on type operators) to simulate polymorphic type operators.
So, is true that polymorphism can be simulated by type operators? I'm probably wrong but I don't understand why. Can anyone help?
My question was ill-posed. I didn't have the concept quite formed in my mind. It actually was triggered by Pierce's comment
when a polymorphic function meets a type argument, the type is actually substituted into the body of the function.Based on that, polymorphic functions felt very close to type operators: type operators work on types, polymorphic functions crystalize into proper functions when given a type. I felt that polymorphic types could be replaced by some kind of (recursive) type operator that "fetched" the proper type. I forgot however that polymorphic types have kind $*$ whilst type operators have kind $* \rightarrow *$. So that's at least one difference.