The specific case you are asking about can be solved nicely using GADTs and polymorphic
variants. See calls to M.add at the bottom of this code:
type whole = [ `Integer ]
type general = [ whole | `Float ]
type _ num =
| I : int -> [> whole ] num
| F : float -> general num
module M :
sig
val add : ([< general ] as 'a) num -> 'a num -> 'a num
val to_int : whole num -> int
val to_float : general num -> float
end =
struct
let add : type a. a num -> a num -> a num = fun a b ->
match a, b with
| I n, I m -> I (n + m)
| F n, I m -> F (n +. float_of_int m)
(* Can't allow the typechecker to see an I pattern first. *)
| _, F m ->
match a with
| I n -> F (float_of_int n +. m)
| F n -> F (n +. m)
let to_int : whole num -> int = fun (I n) -> n
let to_float = function
| I n -> float_of_int n
| F n -> n
end
(* Usage. *)
let () =
M.add (I 1) (I 2) |> M.to_int |> Printf.printf "%i\n";
M.add (I 1) (F 2.) |> M.to_float |> Printf.printf "%f\n";
M.add (F 1.) (I 2) |> M.to_float |> Printf.printf "%f\n";
M.add (F 1.) (F 2.) |> M.to_float |> Printf.printf "%f\n"
That prints
3
3.000000
3.000000
3.000000
You cannot change any of the above to_floats to to_int: it is statically
known that only adding two Is results in an I. However, you can change the
to_int to to_float (and adjust the printf). These operations readily compose and propagate the type information.
The foolery with the nested match expression is a hack I will ask on the
mailing list about. I've never seen this done before.
General type functions
AFAIK the only way to evaluate a general type function in current OCaml requires
the user to provide a witness, i.e. some extra type and value information. This
can be done in many ways, such as wrapping the arguments in extra constructors
(see answer by @mookid), using first-class modules (also discussed in next
section), providing a small list of abstract values to choose from (which
implement the real operation, and the wrapper dispatches to those values). The
example below uses a second GADT to encode a finite relation:
type _ num =
| I : int -> int num
| F : float -> float num
(* Witnesses. *)
type (_, _, _) promotion =
| II : (int, int, int) promotion
| IF : (int, float, float) promotion
| FI : (float, int, float) promotion
| FF : (float, float, float) promotion
module M :
sig
val add : ('a, 'b, 'c) promotion -> 'a num -> 'b num -> 'c num
end =
struct
let add (type a) (type b) (type c)
(p : (a, b, c) promotion) (a : a num) (b : b num) : c num =
match p, a, b with
| II, I n, I m -> I (n + m)
| IF, I n, F m -> F (float_of_int n +. m)
| FI, F n, I m -> F (n +. float_of_int m)
| FF, F n, F m -> F (n +. m)
end
(* Usage. *)
let () =
M.add II (I 1) (I 2) |> fun (I n) -> n |> Printf.printf "%i\n";
M.add IF (I 1) (F 2.) |> fun (F n) -> n |> Printf.printf "%f\n"
Here, the type function is ('a, 'b, 'c) promotion, where 'a, 'b are
arguments, and 'c is the result. Unfortunately, you have to pass add an
instance of promotion for 'c to be ground, i.e. something like this won't
(AFAIK) work:
type 'p result = 'c
constraint 'p = (_, _, 'c) promotion
val add : 'a num -> 'b num -> ('a, 'b, _) promotion result num
Despite the fact that 'c is completely determined by 'a and 'b, due to the GADT; the compiler still sees that as basically just
val add : 'a num -> 'b num -> 'c num
Witnesses don't really buy you much over just having four functions, except that
the set of operations (add, multiply, etc.), and the argument/result type
combinations, can been made mostly orthogonal to each other; the typing can be
nicer and things can be slightly easier to use and implement.
EDIT It's actually possible to drop the I and F constructors, i.e.
val add : ('a, 'b, 'c) promotion -> 'a -> 'b -> `c
This makes the usage much simpler:
M.add IF 1 2. |> Printf.printf "%f\n"
However, in both cases, this is not as composable as the GADT+polymorphic variants solution, since the witness is never inferred.
Future OCaml: modular implicits
If your witness is a first-class module, the compiler can choose it for you
automatically with modular implicits. You can try this code in the
4.02.1+modular-implicits-ber switch. The first example just wraps the GADT witnesses from the previous example in modules, to get the compiler to choose them for you:
module type PROMOTION =
sig
type a
type b
type c
val promotion : (a, b, c) promotion
end
implicit module Promote_int_int =
struct
type a = int
type b = int
type c = int
let promotion = II
end
implicit module Promote_int_float =
struct
type a = int
type b = float
type c = float
let promotion = IF
end
(* Two more like the above. *)
module M' :
sig
val add : {P : PROMOTION} -> P.a num -> P.b num -> P.c num
end =
struct
let add {P : PROMOTION} = M.add P.promotion
end
(* Usage. *)
let () =
M'.add (I 1) (I 2) |> fun (I n) -> n |> Printf.printf "%i\n";
M'.add (I 1) (F 2.) |> fun (F n) -> n |> Printf.printf "%f\n"
With modular implicits, you can also simply add untagged floats and ints. This example corresponds to dispatching to a function "witness":
module type PROMOTING_ADD =
sig
type a
type b
type c
val add : a -> b -> c
end
implicit module Add_int_int =
struct
type a = int
type b = int
type c = int
let add a b = a + b
end
implicit module Add_int_float =
struct
type a = int
type b = float
type c = float
let add a b = (float_of_int a) +. b
end
(* Two more. *)
module M'' :
sig
val add : {P : PROMOTING_ADD} -> P.a -> P.b -> P.c
end =
struct
let add {P : PROMOTING_ADD} = P.add
end
(* Usage. *)
let () =
M''.add 1 2 |> Printf.printf "%i\n";
M''.add 1 2. |> Printf.printf "%f\n"
'a t,'b t? what is "'aand'bints"? – Monarchal