# Functions

## Polymorphism

This mostly discusses polymorphism in statically, as opposed to dynamically, typed languages.

Same operation being applied to othewise different types.

Example add operation working on both integers and strings.

### Parametric Polymorphism

Parameterised data types such as Lists

### Subtyping

Subtyping is a issue in type theory because an element of a type belongs only to that type. Therefore polymorphism based on subtyping may also be an issue.

A way to get some of this capability without the theoretical issues around subtyping might be to use the 'interface'/'typeclass' concept.

Structural types

### Polytypism

• polytypism
• data type genericity - use of type variables.

## Parametricity

Given a function signature what can we know about that functions implementation?

In many cases there will so many ways of translating the input types to the output type that we can't say much at all. Typically such implementations might deconstruct the parameters, do some processing on them and construct the output type.

If type variables have been used in the parameters then we know less about them. Strangely this often allows us to infer more about the implementation because there are less possibilities (a sort of contravarience of information?).

Usually if we have a function signature like a->b->c then we usually infer quantifiers: forall a and b then there exists c. However if a given type variable occurs more than once then there is a sort of dependant sum type.

A lower case identifier in the signature is a type variable, this is a form of polymorphism sometimes called genericity.

Sometimes, given a function signature there is really no choice about the implementation of the function. The following examples use a lower case identifier therefore we don't know anything about the type, so we can't call any functions on it, and the following implementations are forced:

Function Signature Implementation
id: a -> a id x = x
impossible: a -> b none - since we don't know anything about a and b we can't know about any functions between them.
first: a->b->a first x y = x
apply: a -> (a->b) -> b apply x f = f x
forall a. a->a
where a is a higher order type.
f x = \x -> x

Some function signatures will have more freedom, for example:

`List a -> List a`

We can rearrange elements of the list but we can't change the elements. There are two structures here that are somehow orthogonal.

What about parameters of a signature that have a certain 'interface'/'typeclass'? Can we still constrain the signature enough to say something about the implementation?

What if we require our implementation to be unique/canonical, that is, even if there are options for the implementation we are not allowed to make arbitrary choices. The choice must be special in some way.

When sets of sets are infinite is it always possible to have am automatic choice? (see axiom of choice).

[ref 1]

Advanced Topics in Programming Languages Series: Parametric Polymorphism and the Girard-Reynolds Isomorphism. This talk is based on a series of papers by Philip Wadler, a principal designer of the Haskell programming language. Featured are a number of double-barreled names in computer science:

• Hindley-Milner (Strong typing without having to type the types)
• Curry-Howard (Isomorphism between types and theorems, terms and proofs)
• Girard-Reynolds (Isomorphism between types and terms in the presence of parametricity)

For Djinn code see here.

Parametricity

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

 Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to this site, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

This site may have errors. Don't use for critical systems.