CODEWITHSUNDEEP
haskellpolymorphismparametric-polymorphismtype-theoryadhoc-polymorphism
Conor Quinn
Conor Quinn

Reputation: 529

What is the full space of parametrically polymorphic functions (not ad hoc polymorphic) operations in programming languages?

On page 349 paragraph 5 of A Theory of Type Polymorphism in Programming, Milner says,

For us, the polymorphism present in a program is a natural outgrowth of the primitive polymorphic operators which appear to exist in every programming language; such operators are assignment, function application, pairing and tupling, and list-processing operators.

Does this description define the full set of parametrically polymorphic functions (When we extend list processing operators to mean operators on all recursive data types)? (+, *, ... need to be defined in an ad hoc style with different underlying implementations for each type they handle). Also, is there some kind of formal pattern that separates a parametrically polymorphic function from one that has to be defined with overloading (ad hoc)?

Upvotes: 1

Views: 106

Answers (1)

Daniel Wagner
Daniel Wagner

Reputation: 153172

Does this description define the full set of parametrically polymorphic functions?

Certainly not. Church teaches us that there is an infinitely rich collection of parametrically polymorphic functions. For example:

type Nat = forall a. (a -> a) -> a -> a

zero :: Nat
zero s z = z

succ :: Nat -> Nat
succ n s z = s (n s z)

one, two, three :: Nat
one = succ zero
two = succ one
three = succ two

All of zero, one, two, and three are parametrically polymorphic functions; and they are all distinct in that there are arguments we can apply them to that give different results for each. And this is just the Church encoding of one of the simplest recursive data types. The encodings of other data types also give rise to an incredibly complex family of parametrically polymorphic functions of other types... and there are parametrically polymorphic functions which do not correspond to the Church encoding of any data type.

Trying to write down a list of all parametrically polymorphic functions would be a hopeless task indeed, akin (by the Curry-Howard isomorphism) to writing down a list of all mathematical truths!

Also, is there some kind of formal pattern that separates a parametrically polymorphic function from one that has to be defined with overloading (ad hoc)?

Not really. The dictionary-passing implementation of typeclasses in GHC is a witness that any definition that relies on ad-hoc polymorphism can be converted to use parametric polymorphism instead in a systematic, mechanical way.

Upvotes: 0

Related Questions