Introduction

The term polymorphism is very inaccurate. Here the various polymorphism aspects I want to explain:

Alas those categories interlace a lot:


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: |&| 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

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)

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
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

Special Case 2

(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:

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:

Closing the world and "strict" & "permissive"

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:

Simplication

The function calls are separated in two categories: permissive and strict.

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:

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:

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 $