# Can polymorphism be simulated by lazy type operators?

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...

Take (+1)::Num a => a -> a, (+1) pi is Floating whilst (+1) 1.1 is Fractional.

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 (+1). Where,

F :: X -> f -> a -> X a

I've tried to upper case type signatures to represent types and lower case for terms.

And where, 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 .

Therefore, 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?

[EDIT]

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.

• Note that you can use Markdown here. Apr 28, 2015 at 10:44
• Note that in logical frameworks, you can encode $\Pi$-types as a constructor: $\texttt{Π}$, which is applied to a function: $\Pi x:A.\ B = \texttt{Π}(\lambda x:A.\ B)$. Unfortunately, you still need dependent types at the framework level.
– cody
Apr 29, 2015 at 18:07

It's not entirely clear to me how your idea is supposed to work, but everything you're doing can just simply be done with a bit of more high-powered type theory. That is, if we allow quantification over types then we can talk about polymorphism. Let's go from easy examples to the ones you're talking about.

A function such as $$f \, x = (x,x)$$ is polymorphic in the type of $x$: if $x$ has type $A$ then $f$ has type $A \to A \times A$. We can express this sort of dependency by intrducing an extra argument so that $f$ has type $\prod_{A : \mathsf{Type}} A \to A \times A$ and is defined by $$f \, A \, x = (x, x).$$

Your example is like this, except a bit more complicated. To keep examples simple, let me instead used a simplified class (the whole Num is a bit large)

class Cow a where
one :: a
plus :: a -> a -> a


and consider a functio dependent on Cow:

plusOne :: Cow a => a -> a
plusOne x = plus x one


We can express plusOne as before, except that now it takes three extra parameters: a type $A$, an element of $A$, and a function $A \to A \to A$. So its type would be $$\prod_{A : \mathsf{Type}} A \to (A \to A \to A) \to A \to A$$ and it would be defined by $$\mathtt{plusOne} \; A \; \mathtt{one} \; \mathtt{plus} \; x = \mathtt{plus} \; x \; \mathtt{one}.$$ This is a general trick: polymorphism can always be replaced by passing around extra arguments, but the price you pay is that you will have dependent types and there might be many extra arguments.