Introduction
The term polymorphism is very inaccurate. Here the various
polymorphism aspects I want to explain:
- inclusion polymorphism (subtyping, data inheritance)
- interface inheritance (mix-in, type classes)
- ad'hoc overloading (compile-time ad'hoc overloading, free overloading)
- parametric polymorphism
Alas those categories interlace a lot:
- Statically typed languages introduce the "closed world" vs "open world"
restriction. In a closed world we know every instance of a function, whereas
in a open world we must allow the programmer to add new instance without
changing the local meaning.
Dynamically typed languages usually do not bother with such limitations
allowing free overloading, blurring the differences between ad'hoc overloading
and interface inheritance.
- "ad'hoc overloading" is the closed world polymorphism. It is used in
C++/Java to allow multi form constructors... It fits quite well in
explicitly-typed languages, alas the simple & efficient implementation
introduces traps.
- Object-Oriented languages freely mix data and interface inheritance. The
term specialisation is used in both kind of inheritance to call this
overloading.
OO dynamic languages (like Python) mix all kind of polymorphism...
- Parametric and inheritance polymorphism are orthogonal.
- Parametric polymorphism in ML often use polymorphic functions like
equality or comparison which really is interface inheritance
- Interface inheritance without genericity is poor
The full power of parametric polymorphism plus interface inheritance is shown
in haskell's type classes.
Data subtyping
merd offers powerful data subtyping: both extensible variants and records.
Polymorphic Variants
Just like OCaml, merd uses polymorphic variants offering extensibility and
flexibility. But for usability a complex contructor
being declared in a variant can not be used with different applied values.
type foo = [ `Foo of foo | `Bar ]
let _ = `Foo(0)
is allowed in OCaml, whereas merd would refuse it since 0 is not of
type foo.
The | operator is used to combine types, just like OCaml. It
introduces a subtyping relation.
|&| operator
|&| is used to combine value just like a set:
- 0 |&| "" is both 0 and ""
- X(0) |&| Y(1) is both X(0) and Y(1)
- Int |&| String is the type containing the product of Int
and String. 0 |&| "" is an example of such a value.
|&| introduces a subtyping relation which is the inverse of |.
Function call and subtyping
The default calling convention is:
y = f(x) where f !! A -> B implies x !< A and y !> B
- f !! A -> B means the type of f is A -> B
- x !< A means the type of x is a subtype of A
- y !> B means the type of y is a supertype of B
Specialization on datatypes
The generalisation of subtyping to datatypes allow specialization on
datatypes. I don't know if this can be useful:
fact(0) = 1
fact(n) = n * fact(n-1)
introduces two functions: fact_0 !! 0 -> 1 and fact_n !! Num -> Num.
This is quite different from the classical version:
fact(n) = if n == 0 then 1 else n * fact(n-1)
Implementing specialization on datatypes seems quite hard, at least
without being dead slow (especially for numbers).
Interface inheritance
Abstract types are treated like any values with a few special rules.
class is sugar around abstract types:
Eq = class
::== := o,o -> Bool
::!= := o,o -> Bool
Ordered = Eq |&| class
::<=> := o,o -> -1|0|1
is rewritten in
Eq = Builtin::Abstract("Eq")
::== !! Builtin::Open_function(o,o -> o !< Builtin::Abstract("Eq") ; Bool)
::=! !! Builtin::Open_function(o,o -> o !< Builtin::Abstract("Eq") ; Bool)
Ordered = Eq |&| Builtin::Abstract("Ordered")
::<=> !! Builtin::Open_function(o,o -> o !< Ordered ; -1|0|1)
- Builtin::Abstract("Eq") is pretty-printed &Eq, but it
should (must?) not be used directly.
- Builtin::Open_function is a special constructor indicating that
the function is open.
- there is no subtyping relation between &Eq and &Ordered,
the subtyping relation is between Eq and Ordered which are
simple variables. This permits structural equivalence for abstract types.
TODO: instance declaration
Instance
Normally, a !< c and b !< c implies a|b !< c.
Alas this is not true for the real-world - abstract-world subtype, at least
not in any case:
Let
i !! 1 | "foo"
one := 1->1 ; e->e #=> one !! x -> (x !> 1) ; x
- to_string !! &Serializable -> String
i.to_string is ok (gives "1" or "foo")
- (+ 1) !! a -> (1 !< a !< &Addable) ; a
i.(+ 1) is NOT ok (what is "foo" + 1)
- e -> e.one.times(2) !! a -> (1 !< a !< &Addable) ; a
i.one.times(2) is ok (gives 2 or "foofoo")
This shows that the constraints are not precise enough.
TODO: explain the &Strict solution
Ad'hoc overloading
Special Case 1
(1) void move(Boo);
(2) void move(Foo, int, int);
(3) void move(Bar, int, int);
merd version
(1) move !! Boo -> ()
(2) move !! Foo, Int, Int -> ()
(3) move !! Bar, Int, Int -> ()
(2,3) move !! Foo|Bar, Int, Int -> ()
merd keeps the resulting type in the form:
move !!
Boo -> () &&
Foo, Int, Int -> () &&
Bar, Int, Int -> ()
inference
Inference can take advantage of the equivalence: (2) and
(3) <=> (2,3). This tries to make ad'hoc
overloading less ad'hoc, factorizing the differences.
move(o,x,y) => o !< Foo|Bar ; x !< Int ; y !< Int
move(o) => o !< Boo
(1) Foo move(Foo, int, int);
(2) Bar move(Bar, int, int);
(!subtyping spoilage! more on it later)
merd version (#1)
(1) move !! Foo, Int, Int -> Foo
(2) move !! Bar, Int, Int -> Bar
(approx 1,2) move !! Foo|Bar, Int, Int -> Foo|Bar
inference (#1)
If we already have a constraint on "o", it can help choosing the good
overloaded function:
o !< Foo ; o' = move(o,x,y) => o' !> Foo
Otherwise, there is no best solution here:
- Keeping all the constraints on types is complicated: it implies keeping
exclusive disjunctions of constraints. To simplify type unification, this
solution is discarded in merd.
- Use the (approx 1,2) rule
o' = move(o,x,y) => o !< Foo|Bar, o' !> Foo|Bar
This is not a good solution as we are loosing precision (the type link between
"o" and "o'" is lost)
- Use a default type: in some case, it can be useful to prefer a
type over another.
o' = move(o,x,y) => o !< Foo ; o' !> Foo
- Make it an error, asking for more type information
merd version (#2)
A better solution, not semantically equivalent, but better approaching the
idea of the example:
(1) move !! x, Int, Int -> x !< Foo ; x
(2) move !! x, Int, Int -> x !< Bar ; x
(1,2) move !! x, Int, Int -> x !< Foo|Bar ; x
This version has the advantage of preserving subtyping.
inference (#2)
o' = move(o,x,y) => o !< Foo|Bar ; o' !> o
Special Case 2
(1) Boo move(Foo);
(2) Far move(Bar);
merd version
(1) move !! Foo -> Boo
(2) move !! Bar -> Far
(approx 1,2) move !! Foo|Bar -> Boo|Far
inference
Once again, no good solution. A solution would to type infere 2 times for each
possibility. It would enable:
f =
None -> None
Some(x) -> Some(move(x))
to be typechecked as (None|Some(Foo) -> None|Some(Boo)) |&| (None|Some(Bar) -> None|Some(Far))
General case
(1) void move(Foo, Bar);
(2) void move(Boo, Far);
merd version
(1) move !! Foo, Bar -> ()
(2) move !! Boo, Far -> ()
inference
If we already have a constraint on "o", it can help choosing the good
overloaded function:
o !< Foo ; move(o,o') => o' !< Bar
Otherwise, once again there is no best solution here:
- Approximating "move" with "Foo|Boo, Bar|Far -> ()" is wrong, as it
would allow ill-typed solutions (eg: "Foo, Far -> ()")
- Use a default type
- Make it an error, asking for more type information
Introduction
l1 = [ 1, "foo" ].map(to_string)
l2 = [ 1, "foo" ].map(+ 1)
l3 = [ 1, "foo" ].map((1 -> 1) ; (x -> x + x))
l1 and l3 should be legal, whereas l2 should not.
we have:
[ 1, "foo" ] !! List(1 | "foo")
to_string !! Serializable -> String
+ 1 !! o -> (1 !< o !< Addable) ; o
(1 -> 1) ; (x -> x + x) !! o -> (1 !< o !< Addable) ; o
Int !< Serializable
String !< Serializable
Int !< Addable
String !< Addable
argh! l2 and l3 are typed exactly the same :-(
Abstract types and subtyping
merd tries to hide the gap between real
world and abstract world. This is done by having the subtyping relation
working across physical/abstract worlds. eg:
Serializable Addable
/ \ / \
/ \ / \
Int String Int String
| | | |
1 "foo" 1 "foo"
aka:
1 !< Int !< Serializable
"foo" !< String !< Serializable
Alas, things do not work *that* nicely.
Using the relation A !< C and B !< C => A|B !< C
we should have
Int|String !< Addable (since Int !< Addable and String !< Addable)
which we don't want to be true, otherwise we must allow 1 + "foo"
On the other hand, there are case where we do want Int|String to work:
Int|String !< Serializable
which allow "l1"
Why does Int|String !< Serializable holds (l1)
whereas Int|String !< Addable sometimes does (l3), sometimes doesn't (l2)
Closing the world
In fact, when closing the world x !< Serializable,
x = Int|String is not a good solution, but
x in { Int, String } is.
x -> x.to_string
implies union(x where x !< Serializable)
which gives union { Int, String }
which is Int | String
x -> x+1
implies union(x where 1 !< x !< Addable)
which gives union(Int)
which is Int
y -> y.((1 -> 1) ; (x -> x + x))
implies y !> 1 and y !< union(x where x !< Addable)
which gives 1 !< y !< Int | String
This is simple when the world is closed during type inference. But this is too
restrictive.
If we want to keep open-world types:
- we can enrich the type system to keep abstract types constraint as shown
above
- we can simplify the constraint, loosing some precisions
Simplication
The function calls are separated in two categories: permissive and strict.
- with permissive functions, closing the world allow to take the union of the
solutions. "to_string" is a permissive function
- with strict functions, you must choose one and only one solution when
closing the world
To mark the difference, the type of strict functions is modified:
::+ !! o,o -> (o !< Addable |&| &Strict) ; o
(instead of ::+ !! o,o -> (o !< Addable) ; o
the &Strict is a magic tag indicating that closing the world must be done
strictly.
Let's have a look at the examples:
- l1
to_string !! Serializable -> String
type is unchanged, the constraint
"Int | String !< Serializable" is verified
=> l1 accepted
- l2
+ 1 !! o -> (1 !< o !< Addable |&| &Strict) ; o
the constraint
1 !< o ; Int | String !< o ; o !< Addable |&| &Strict
is rejected, since nor "o !! Int" nor "o !! String" works
=> l2 rejected
- l3
(1 -> 1) ; (x -> x + x) !! o -> (1 !< o !< Addable |&| &Strict) ; o
the type is the same as l2
=> l3 rejected
The &Strict allows to accept l1 and reject l2, but can't make the difference
between l2 and l3. This is the cost for keeping the type system "simple".
Telling wether a function is strict or permissive
It's quite simple: if a type variable occurs more than once on the left or the
right of "->", it must be strict.
In fact, there's no function strict/permissive, there's only variable type
which are strict/permissive.
Examples:
to_string := Serializable -> String
::&&& := Default_val,o -> (o !< Default_val) ; o
::||| := o,o -> (o !< Default_val) ; o
::+= := Inout(o),o -> (o !< Addable) ; ()
times := o, Uint -> (o !< Addable) ; o
becomes
to_string := Serializable -> String
::&&& := Default_val,o -> (o !< Default_val) ; o
::||| := o,o -> (o !< Default_val |&| &Strict) ; o
::+= := Inout(o),o -> (o !< Addable |&| &Strict) ; ()
times := o, Uint -> (o !< Addable) ; o
note that &&& is permissive, whereas ||| is strict.
Alternative simplification
A even simpler simplification is to seperate the abstract types in the
strict/permissive categories. An abstract type is permissive if all its
functions are permissive, otherwise it is strict.
This solution is of course less precise: this would make the "times" function
strict.
The advantage is that there's no need for the &Strict trick. When closing the
world, you just see if the abstract type is permissive or not.
Comparison with other languages
Well, I don't know any languages that have enough expressivity to have such
problems:
- ruby, python, perl
are not statically typed
- ocaml, java, C++, eiffel
do not have multi-methods
- haskell
do not have subtyping on physical types
only has intersection types on type classes
More on polymorphism, overloading
Pixel
This document is licensed under GFDL (GNU Free Documentation License).
Release: $Id: polymorphism.html,v 1.19 2002/05/17 15:22:56 pixel_ Exp $