Title: Theory / Unimportant / CS / Programming / oCaml / Manual{ / 05 Polymorphism and its limitations;
Tags: hasNotNewEffectReturnsMeaning type
On every note of this deck, unless a note says otherwise:
Page: http://caml.inria.fr/pub/docs/manual-ocaml/polymorphism.html#sec51

Typ: '_a
Meaning: A polymorphic type which lose polymorphism on first use
Page: http://caml.inria.fr/pub/docs/manual-ocaml/polymorphism.html#sec51
Language: ocaml
Chapter: 5
Section: 1
Name: A weak polymorphic type

Name: Value restriction
Definition: The rules stating that weak polymorphism should be used instead of polymorphism
Chapter: 5
Section: 1.2

Name: Relaxed value restriction
Definition: The rules stating that polymorphism should be used instead of weak polymorphism when some safety condition holds
Chapter: 5
Section: 1.2
Context: OCaml

Definition: x is a subtype of y
Chapter: 5
Section: 1.4
Variables: \(x,y\) types
Context: oCaml
Notation: x:>y
Extra: checked

Name: A constructor covariant in \(i\)-th position
Definition: A constructor C such that if x:> y, with x in i-th position, then
C foo_1 ... foo_i-1 x foo_i+1 ... foo_n :> C foo_1 ... foo_i-1 y foo_i+1 ... foo_n
Chapter: 5
Section: 1.4

Name: A constructor contravariant in \(i\)-th position
Definition: A constructor C such that if x:> y, with x in i-th position, then
C foo_1 ... foo_i-1 y foo_i+1 ... foo_n :> C foo_1 ... foo_i-1 x foo_i+1 ... foo_n
Chapter: 5
Section: 1.4

Name: A constructor invariant in \(i\)-th position
Definition: A constructor C which is neither contravariant nor covariant in \(i\)-th position
Chapter: 5
Section: 1.4

Typ: +'a
Meaning: A polymorphic type 'a which is covariant
Page: http://caml.inria.fr/pub/docs/manual-ocaml/polymorphism.html#sec51
Language: ocaml
Chapter: 5
Section: 1.5

Typ: 'a. t
Meaning: A type t, with 'a polymorphic, universally quantified on each call, such that 'a can not by unified with anything
Page: http://caml.inria.fr/pub/docs/manual-ocaml/polymorphism.html#sec51
Language: ocaml
Chapter: 5
Section: 1.5
Example: let rec depth: 'a. 'a nested -> int = function
| List _ -> 1
| Nested n -> 1 + depth n;;

Question: How to code
let average f x y = (f x + f y) / 2;;
such that f can be len ?
Answer: Introduce f inside a structure, so that it can have universal type quantifier
type 'a nested_reduction = { f:'elt. 'elt nested -> 'a };;
Put len in this structure
let boxed_len = { f = len };;
call average with this structure
let average nsm x y = (nsm.f x + nsm.f y) / 2 ;;
Page: http://caml.inria.fr/pub/docs/manual-ocaml/polymorphism.html#sec51
Chapter: 5
Section: 3
Variables: type 'a nested = List of 'a list | Nested of 'a list nested;;
let len, of type 'a. 'a nested -> int, which returns the number of element in the nested list.
Answer2: Introduce f inside an object, so that it can have universal type quantifier
let obj_len = object method f:'a. 'a nested -> 'b = len end;;
call average with this object
let average (obj:<f:'a. 'a nested -> _ > ) x y = (obj#f x + obj#f y) / 2 ;;