Extensional polymorphism

– theory and applications –

Jun FURUSE

INRIA Rocquencourt Projet Cristal

⇒

Extensional polymorphism

Ad-hoc parametric (non parametric) polymorphism extension framework over ML.

• Polymorphic primitives with type dependent semantics – Polymorphic overloaded arithmetic operators (+), (-), … – Primitives for dynamic values, persistent data storage, … – Meta-programming tools: print, eval

• User definition of overloaded values

– Pattern match based definition and semantics

       generic plus = case
       | int → int → int ⇒ plus_int
       | float → float → float ⇒ plus_float
       ;;

⇒

Motivation: Overloading in ML (SML)

SML has overloaded arithmetic operators (+),(-), etc. • Predefined (not user definable)

• Not really polymorphic. The definition:

       let double x = x + x

– is rejected in SML’90

– has a type int → int in SML’97, using the default type of (+),

     int → int → int.

⇒

Motivation: Overloading in Haskell

Haskell type classes support:

• User definition of overloaded values

• Extension by class instances Problems:

• Some typing restrictions – Multi type class parameters

– Overlap instances

are not allowed, or restricted.

• Open extension scheme does not match with ML semantics – Type classes must be global

– Mutual recursive module dependency

⇒

Motivation: Overloading in ML (O’Caml)

O’Caml has … none!

• Each arithmetic type has its own set of operators.

• We have 10 arithmetic types!

  int, int32, int64, nativeint, float, Complex.t,
   nat, big int, ratio, num

We need overloading!!

⇒

Extensional polymorphism

Generic values, our ad-hoc polymorphic values support:

• Polymorphic primitives with type dependent semantics – Polymorphic overloaded arithmetic operators (+), (-), …

– Primitives for dynamic values, persistent data storage, …

• User definition of overloaded values – Pattern match based definition and semantics

– No typing restrictions of overloaded instances

– Recursions on types are easily defined

• Simple design

– Two-layer typing: new typing extension is modular both in theory and implementation.

⇒

Generic primitives

Example: value printer as a generic primitive:

val print : ∀δ.δ → unit

Type dependent semantics as a primitive:

print : τ → unit ⇝ gen(print,τ)

Compilation with type application and abstraction like system F:

print 1 ⇒ print �int� 1
let print twice = λx.print x; print x
     ⇒ let print twice = Λδ.λx.print δ x; print δ x
print twice (1,3.14) ⇒ print twice �int*float� (1,3.14)

⇒

Generic primitives – typing and compilation

Ad-hoc polymorphism is quantified by dynamic type variables δ, δ′, … to be distinguished from regular parametric polymorphism:

let id = λx.x
val id : ∀α.α → α  val print : ∀δ.δ → δ

Type application and abstraction are attached only to ad-hoc polymorphism:

let id = λx.x ⇒ let id = λx.x
id (1,3.14) ⇒ id (1,3.14)
let print twice = λx.print x; print x
     ⇒ let print twice = Λδ.λx.print δ x; print δ x
print twice (1,3.14) ⇒ print twice �int*float� (1,3.14)

Classical ML programs can be executed efficiently without any overhead.

⇒

Application of generic primitives

Primitive functions for dynamic values can be defined as generic primitives:

val dynamic : ∀δ.δ → dyn
let dynamic_comp = fun t x → (x,t)
gen(dynamic,τ) ≡ dynamic comp τ
val coerce : ∀δ.dyn → δ
let coerce_comp = fun t (v,t') → if t ≤ t' then v
                                 else raise Coercion_failure
gen(coerce,τ) ≡ coerce comp τ

(We need more careful type checking for encapsulation of polymorphic values.)

⇒ Coherence problem of generic primitives – dyn-unification

Generic primitive instances with more than one possible types may have incompatible semantics depending on types – coherence problem:

val print : ∀δ.δ → unit      val read : ∀δ.unit → δ
print (read ())
print (read () : int)
print (read () : float)
print (read () : δ)

} incompatible semantics!

Solution: free dynamic type variables are forced to be unified with some closed type: dyn, since so that use of the free variables can be virtually postponed at run time:

1                                (1,int)
3.14 ⟹ (read () : dyn) ⟹ (3.14,float)
"1"                              ("1",string)

⇒

User defined generics

Definition by type cases, a list of type indexed expressions:

generic plus = case
| int → int → int ⇒ plus_int
| float → float → float ⇒ plus_float
in ...
plus 1 2  ⇝ 3
plus 1.2 3.4 ⇝ 4.6

⇒

Type case selection semantics by pattern match

Case selection priority like pattern matching allows overlapped instance definitions:

generic find_int = case
| ∀δ.(int* δ) → int ⇒ fun (x,y) → x
| ∀δ.(δ *int) → int ⇒ fun (x,y) → y
;;
find_int (1, 3.14) ⇝ 1
find_int (3.14, 2) ⇝ 2

The first match is selected when there are more than one:

find_int (1, 2)  ⇝ 1

⇒

User defined generics – recursion over types

Recursive generic binding easily defines complex recursive overloaded values:

generic rec flat = case (* super list flattening *)
| ∀δδ′.δ list list → δ′ list ⇒
     fun x → flat (List.flatten x)
| ∀δ.δ list → δ list ⇒ fun x → x

(Multiple parameters δ and δ′ can be used without any problem.) It flattens lists:

# flat [[1]; [2;3]];;
- : int list = [1; 2; 3]

From any depth to one!

# flat [[[[1]; [2;3]]; [[4;5;6]]]; []];;
- : int list = [1; 2; 3; 4; 5; 6]

⇒

User defined generics – other examples

Tautology checker

generic rec taut = case
| bool → bool ⇒ fun x → x
| ∀δ.(bool → δ) → bool ⇒
      fun form → taut (form true) && taut (form false)
;;
# taut (fun p → not p or p);; (* checks ∀P. ¬P ∨ P *)
- : bool = true

⇒

User defined generics – other examples

Function with variable length of arguments

generic rec vprint = case
| unit ⇒ ()
| ∀δδ′.δ → δ′ ⇒ fun x → print x; vprint
;;
# vprint 1 3.14 "hello";;
1 3.14 hello
- : unit = ()

⇒

Typing and compilation: big picture

untyped source fully type annotated program E ⊧ e_{t} : τ ⟹ r semantics with types

normal ; typing ; Γ ⊢ e_{t} : τ

constraint annotated program

generic ; constraint ; typing ; Γ, V ⊩ e_{t} : τ

type dispatch compilation

E ⊧ e ⟹ r untyped semantics

flow compilation No type dispatching

⇒ Type checking of generics – two typing layers

Normal typing layer: Γ ⊢ e_{t} : τ • Regular ML typing with minimal extension (= dynamic variables)

• User defined generics have type schemes as anti-unifiers of type cases:

generic plus = case
| int → int → int ⇒ plus int
| float → float → float ⇒ plus float
;;
val plus : ∀δ.δ → δ → δ

• Types may be too general.

plus "hello" "world" well-typed, but lacks semantics • but are good approximation to provide principal typings.

⇒

Type checking of generics – two typing layers

Generic constraint typing layer: Γ, V ⊩ e_{t} : τ • For detecting illegal uses of user generics without semantics

• User generics are assigned with generic constraints:

plus :  [ int → int → int | float → float → float ]

Generic constraints constraint type instantiations of too general type schemes obtaind in the normal layer.

val plus : ∀δ.δ → δ → δ
plus : int → int → int  ok
plus : float → float → float  ok
plus : string → string → string  type error

⇒

Type checking of generics – generic constraints

Generic constraint represents the set of valid instance types.

generic plus = case
| int → int → int ⇒ plus int
| float → float → float ⇒ plus float
;;
K_{plus} = [ int → int → int | float → float → float ]

Intuitively, it is a list of type patterns.

         int → int → int <: K_{plus}

   float → float → float <: K_{plus}
string → string → string ≮: K_{plus}

⇒

Internal use of other generics also adds constraints:

let double x = plus x x;;

K_{double} = [ ∀δ.δ → δ { δ → δ → δ <: K_{plus}} ]

      int → int <: K_{double}
  float → float <: K_{double}
string → string ≮: K_{double}

⇒

Recursive use of generics produce recursive constraints

generic rec flat = case
| ∀δδ′. δ list list → δ′ list ⇒
    fun x → (flat : δ list → δ′ list) (List.flatten x)
| ∀δ.δ list → δ list ⇒ fun x → x
;;
K_{flat} =
   μκ.[ ∀δδ′. δ list list → δ′ list { δ list → δ′ list <: κ }
      | ∀δ.δ list → δ list ]
int list list list → int list <: K_{flat}
int list list list → int list list <: K_{flat}
int list list list → int list list list <: K_{flat}
...

⇒

Type inference of user generics – coherence

Instance of user generics may have more than one typing:

flat [[[1]]] : int list
flat [[[1]]] : int list list
flat [[[1]]] : int list list list

Usual pattern matching priority rule leads to the default typing selection rule.

generic rec flat = case
 | ∀δδ′.δ list list → δ′ list ⇒ fun x → flat (List.flatten x)

 | ∀δ.δ list → δ list ⇒ fun x → x

 | ∀δ.δ list → δ list ⇒ fun x → x | ∀δδ′.δ list list → δ′ list ⇒ fun x → flat (List.flatten x)

# flat [[[1]]];;
- :  int list = [1] int list list list = [[[1]]]

Other typings can be selected by giving type information explicitly:

# (flat [[[1]]] : int list list);;
- : int list list = [[1]]

⇒

Compilation of user generics – type passing

Classical compilation by type passing:

generic rec flat = case
| ∀δδ′.δ list list → δ′ list ⇒
     flat (List.flatten x)
| ∀δ.δ list → δ list ⇒ fun x → x
in flat [[[1]]]
      ⇒  let rec flat = fun ty ty' →
              match ty, ty' with
              | �t list, t'� →
                  flat �t� �t'� (List.flatten x)
              | �t�, �t� → fun x → x
            in flat �int list list� �int� [[[1]]]

Type case selection is performed statically during typing: use it to compile!

⇒

Compilation of user generics – generic flow passing

Dispatching generic flows, witness of successful type case selections obtained from generic constraint typing.

generic plus = case
| int → int → int ⇒ plus_int
| float → float → float ⇒ plus_float
in
plus 1 2
;;

        ⇒  let plus =

                  let tcs = [| plus_int; plus_float |] in
                  fun pos → tcs.(pos)
                in
                plus 0 (* flow to access plus_int *) 1 2
                ;;

⇒

Generic flows are integer graphs, corresponding to the graph of generic calls.

generic rec flat = case
| ∀δδ′.δ list list → δ′ list ⇒
     flat (List.flatten x)
| ∀δ.δ list → δ list ⇒ fun x → x
;;
 ⇒ type flow = int*flow array (* integer graph *)
    let rec flat =
      let tcs =
        [| fun subs → fun x → flat subs.(0) (List.flatten x);
           fun subs → fun x → x |]
      in
      fun (p,subs) → tm.(p) subs
    ;;

⇒

Generic flows are integer graphs, following the tree structure of generic calls.

let rec flat =
  let tcs =
    [| fun subs → fun x → flat subs.(0) (List.flatten x);
       fun subs → fun x → x |]
  in
  fun (p,subs) → tm.(p) subs
;;
flat [[[1]]] : int list ⇒ flat (0 → 0 → 1) [[[1]]]
                         ⇝ flat (0 → 1) [[1]]
                         ⇝ flat (1) [1]
                         ⇝ [1]

⇒

Generic flow passing supersedes type passing:

• Type case selection is performed in constant time, regardless of type pattern complexity.

• Upward compatible and better type case selection semantics with static

backtracking, precomputed at static typing time.

generic rec flat = case
| ∀δδ′.δ list list → δ′ list ⇒
     flat (List.flatten x)
| ∀δ.δ list → δ list ⇒ fun x → x
;;
flat : int list list → int list list

– Run time type pattern matching cannot give semantics

– Flow passing can select the second case

⇒

Other topics...

• Primitives for type safe data exchange between arbitrary ML programs – Data type identification using encrypted check-sums of type definitions.

• Incremental generic definition by inclusion:

generic rec plus' = case
| include plus

| δ * δ′ → δ * δ′ → δ * δ′ ⇒

      fun (x,y) (z,w) → (plus' x z, plus' y w)

Open recursion within closed extension:

generic plus'' = case
| include plus'
| string → string → string ⇒ String.concat

Internal recursive calls in plus' are automatically redirected to plus'':

plus'' ("hello ",1) ("world,2) ⇝ ("hello world", 3)

⇒

Future work

• Refinement of type inference:

– ex. functional dependencies of Haskell type class

• Open extension ? (maybe with Haskell like typing restrictions)

• Implementation:

– Prototype has been developed.

– Coexistence with other type extensions: (O’Caml’s classes, polymorphic variants, etc...)

⇒

Conclusion

Extensional polymorphism… • is non-parametric polymorphism extension over ML

• supports type passing based ad-hoc polymorphic generic primitives, including almighty ML value printer, dynamic values, etc.

• provides user definition of overloaded values – pattern matching based definitions allow nice semantics and typing – independent typing system for generics simplifies both theory and

implementation

– new generic flow compilation performs powerful case selection

• new type-value computation methodology: ex. taut, flat, vprint etc.

⇒