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:

References

The only reference i've found talking about things alike Strict is weak binary operations vs strong binary operations in chapter 24 of Types and Programming Languages

More on polymorphism, overloading


Pixel
This document is licensed under GFDL (GNU Free Documentation License).

Release: $Id: polymorphism.html,v 1.21 2002/09/07 20:15:27 pixel_ Exp $