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?


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.

  • $\begingroup$ Note that you can use Markdown here. $\endgroup$ – Raphael Apr 28 '15 at 10:44
  • $\begingroup$ 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. $\endgroup$ – cody Apr 29 '15 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.