Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
367 lines (268 sloc) 11.1 KB

Polymorphic Variants

There are three different kinds of varints [< … ], […], [> …]. They are subtly different in terms of unification and coercion. First, let’s consider the cases coercion happens, there are nine cases together

Coercion

Co-Domain is closed variant type

The output is as follows:

let f x = (x : [`a] :> [<`a|`b]);;
val f : [ `a ] -> [ `a ] = <fun>

let f x = (x : [>`a] :> [<`a|`b]);;
val f : ([< `a | `b > `a ] as 'a) -> 'a = <fun>

let f x = (x : [<`a] :> [< `a|`b]);;
val f : ([< `a ] as 'a) -> 'a = <fun>

When the codomain of type coercion is a closed variant type , the coercion does not have effect on domain, it may add more constraint to the typing relation, but the input and output always share the same type.

Here [< `a | `b > `a ] reads a subset of `a or `b with the constraint > `a (this is called possible tags)

Co-domain is exact variant type

let f x = (x : [`a] :> [ `a|`b]);;
val f : [ `a ] -> [ `a | `b ] = <fun>

let f x = (x : [<`a] :> [ `a|`b]);;
val f : [< `a ] -> [ `a | `b ] = <fun>

let f x = (x : [> `a] :> [ `a|`b]);;
val f : [ `a | `b ] -> [ `a | `b ] = <fun>  

There’s no surprise here.

Co-domain is open variant type

let f x = (x : [ `a] :> [> `a|`b]);;
val f : [ `a ] -> [> `a | `b ] = <fun>

let f x = (x : [> `a] :> [> `a|`b]);;
val f : ([> `a | `b ] as 'a) -> 'a = <fun>

let f x = (x : [< `a] :> [> `a|`b]);;
val f : [< `a ] -> [> `a | `b ] = <fun>

Width and depth subtyping

ocaml does has width and depth subtyping if /t1 :> t1'/ and /t2 :> t2'/ then /(t1,t2) :> (t1',t2')/

let f x = (x:[`A] * [`B] :> [`A|`C] * [`B | `D]);; 
val f : [ `A ] * [ `B ] -> [ `A | `C ] * [ `B | `D ] = <fun>


let f x = (x : [ `A | `B ] -> [ `C ] :> [ `A ] -> [ `C | `D ]);;
val f : ([ `A | `B ] -> [ `C ]) -> [ `A ] -> [ `C | `D ] = <fun>
    

Unification

There’s some uncertainity in closed variant and open variant. So unification will make sense here.

For example, the code below will give an error

let f (x: [` a  ]) : [`a | `b ] = x  (* failed*)   
let f (x: [` a  ]) : [< `a | `b ] = x ;;
val f : [ `a ] -> [ `a ] = <fun>

let f (x:[<`a|`b>`a `b]) :[`a |`b]= x ;;
(*just abbreviation *)  
val f : [ `a | `b ] -> [ `a | `b ] = <fun>
                                           

let f (x:[<`a|`b>`a ]) :[`a |`b]= x ;;
val f : [ `a | `b ] -> [ `a | `b ] = <fun>
(* the left reads at least allows tag `a *)                                           

let f (x:[<`a|`b>`b ]) :[`a |`b]= x ;;
val f : [ `a | `b ] -> [ `a | `b ] = <fun>
(* the left reads at least allows tag `b *)                                           

                                           
let f (x:[<`a|`b>`a `b `c ]) :[`a |`b]= x ;;
Characters 9-27:
  let f (x:[<`a|`b>`a `b `c ]) :[`a |`b]= x ;;
           ^^^^^^^^^^^^^^^^^^
Error: The present constructor c has no type

let f (x:[<`a|`b>`b  ]) :[`a ]= x ;;
Characters 32-33:
  let f (x:[<`a|`b>`b  ]) :[`a ]= x ;;
                                  ^
Error: This expression has type [< `a | `b > `b ]
       but an expression was expected of type [ `a ]
       The second variant type does not allow tag(s) `b
(* the left reads at least allows tag `b while
   the right does not have *)                                    

let f (x:[<`a|`b>`a  ]) :[`a ]= x ;;
val f : [ `a ] -> [ `a ] = <fun>

There’s some varity in closed variant, so the compiler will try to unify it.

Let’s take a concrete example:

let f x  =  (x: [> `a] :> [< `a | `b ]);;
val f : ([< `a | `b > `a ] as 'a) -> 'a = <fun>

The type of f reads that it can be either `a or `b with a constraint that at least allows tag `a, so if you tried f `a, f `b, both will work but the following code will break:

let x = (`b : [`b]);;
val x : [ `b ] = `b
# f x;;
Characters 2-3:
  f x;;
    ^
Error: This expression has type [ `b ] but an expression was expected of type
         [< `a | `b > `a ]
       The first variant type does not allow tag(s) `a

Example

The code below shows how to define type abbreviations to reduce type coercion:

type value = [`Scalar of float | `Vector of float * float ]
type scalar = [`Scalar of float]
type vector = [`Vector of float * float ]
type operation =
    [`Multiply of scalar * scalar
    | `DotProduct of vector * vector ]
type general_operation =
    [ `Multiply of value * value 
    | `DotProduct of value * value ]
let values x =
  match (x : operation :> general_operation)  with
  | `Multiply (a,b) ->  [a;b]
  | `DotProduct (a,b) -> [a;b]      

Problem

The type inference was not precise:

let f x = match x  with `a -> `b | x -> x ;;
val f : ([> `a | `b ] as 'a) -> 'a = <fun>

Here the `a will never appear as output, but we could not encode the invariant here.

use-case

If the variant type is exported in the interface and I feel that some cases could appear in other modules but it wouldn’t necessarily make sense to make them dependend on the module, I use polymorphic variants because they are not tied to the module namespace system

If the variant type is exported in the interface I find it sometimes too verbose to use regular variants when values of the variant type are given to functions of the module.

type base = [`String of string | `Int of int]
type t1 = [base | `Bool of bool | `List of t1 list]
type t2 = [base | `Other]

let simplify (x:t1):t2 = match x with
| #base as b -> b
| `Bool _ | `List _ -> `Other    

open recursion for term rewriting

type base = [`String of string | `Int of int]
type t1 = [base | `Bool of bool | `List of t1 list]
type t2 = [base | `Other]
            
let simplify (x:t1):t2 = match x with
  | #base as b -> b
  | `Bool _ | `List _ -> `Other    

Unfortunately Ocaml’s Hindley-Milner type inference is not strong enough to do this kind of thing without explicit typing, which requires careful factorisation of the types, which in turn makes proto-typing difficult. Additionally, explicit coercions are sometimes required.

The big downside of this technique is that for terms with multiple parameters, one soon ends up with a rather confusing combinatorial explosion of types, and in the end it is easier to give up on static enforcement and use a kitchen sink type with wildcards and exceptions (i.e. dynamic typing).

type abbreviation

type 'a number = 'a constraint 'a = [>`Integer of int | `Real of float]

It’s cool that ~’a~ can be extended dynamically

let zero : 'a number = `Zero;;
val zero : [> `Integer of int | `Real of float | `Zero ] number = `Zero
type 'a number = 'a constraint 'a = [< `Integer of int | `Real of float ]
let z:'a number  = `Real 3.0;;
val z : [< `Integer of int | `Real of float > `Real ] number = `Real 3.
type number = [ `Integer of int | `Real of float ]   

private row types

Private row types are type abbreviations where part of the structure of the type is left abstract.

type-equation   ::=      ...  
        ∣        = private typexpr

Concretely typexpr in the above should denote either an object type or a polymorphic variant type. If the private declaration is used in interface, the corresponding implementation may either provide a ground instance, or a refined private type.

type c = private <x:int; ..> 

This denotation does more than hiding the y method, it also makes the type c incompatible with any other closed object type.

Private row types are more flexible with respect to incremental refinement, this feature can be used in combination with functors. (* FIXME subtyping does not work here :-(, refinement works*)

module F(X : sig type c = private < x : int; .. > end) = struct
  let get_x (o : X.c) = o#x end
module G(X : sig type c = private < x : int; y : int; .. > end) = struct
  include F(X)
  let get_y (o : X.c) = o#y end;;

module F : functor (X : sig type c = private < x : int; .. > end) ->
    sig val get_x : X.c -> int end
module G : functor (X : sig type c = private < x : int; y : int; .. > end) ->
    sig val get_x : X.c -> int val get_y : X.c -> int end
   

combination with polymorphic variant

type t = [ `A of int | `B of bool ]
type u = private [< t > `A ]
type v = private [> t ]

With type u, it’s possible to create values of the form (`A n), but not (`B b), with type v, construction is restricted to `A,`B, and a default case is needed

Conculsion

For open union, it’s easy to reuse, but unsafe, for closed union, hard to use, since the type checker is conservative

Variance notation

If you don’t write the + and -, ocaml will infer them for you , but when you write abstract type in module type signatures, it makes sense. variance annotations allow you to expose the subtyping properties of your type in an interface, without exposing the representation.

type (+'a, +'b) t = 'a * 'b
type (-'a,+'b) t = 'a -> 'b 
module M : sig
  type (+'a,'+b) t
end = struct
  type ('a,'b) t = 'a * 'b 
end

ocaml did the check when you define it, so you can not define it arbitrarily

Variance notation helps polymorphism

module M : sig
  type +'a t
  val embed : 'a -> 'a t
end = struct
  type 'a t = 'a
  let embed x = x
end ;;
M.embed []  ;;
- : 'a list M.t = <abstr>

You can see that it’s no longer /'_a list/