"ocaml_beginners"::[] OCaml & subtyping polymorphism

Hello all,

I should like to know more about subtyping polymorphism and OCaml ( if I'm not the only
OCaml programmer in the world that worries about the incompleteness of that feature
in OCaml). The typical case is when you have two types, one of which
is a "large" subtype of the other (e.g. 'a equitable_partition and 'a
partition, increasing_mapping and mapping, or even positive_int and int, etc).
You are stuck between two ugly alternatives :

1) If you implement those types as one and the same, say

type increasing_mapping =mapping;;

the typechecker will not warn you when you mistake one type for the other. Even if you
put "assert" checks (that will consume computation time instead of "doing things right";
from the beginning, during the typechecking phase), errors will show up only at runtime,
debugging will be more laborious, and you will have less trust in a piece of code that
compiles correctly.

2) If you separate the two types with a constructor, say

type increasing_mapping=IncreasingMappingConstructor of mapping;;

then type security will come at the following price : your code will be filled with
conversions between the two types, and the interpreter will waste time
removing and putting back the constructor.

Last (this is a question for Jon Harrop I guess) : does F# allow for
a better treatment of that problem ? I read in http://research.microsoft.com/fsharp/
language-compare.aspx that F# has "nominal subtyping constraints". What is this ?

TIA,

Ewan

Messages in this topic (1) Reply (via web post) | Start a new topic

.

Shalom, roparzhhemon.

r> The typical case is when you have two types, one of which
r> is a "large" subtype of the other (e.g. 'a
r> equitable_partition and 'a partition, increasing_mapping
r> and mapping, or even positive_int and int, etc).

There are better alternatives than these two.
I don't know what are "'a partition" and "'a mapping",
but for positive_int it's possible to define module with
signature like that:

module Pos : sig
type positive_int = 'z;
value of_int : int -> positive_int;
value add : positive_int -> positive_int -> positive_int;
value sub : positive_int -> positive_int -> positive_int;
... more operations ...
value to_int : positive_int -> int;
end;
(it's even possible to make modules like IntOps and
PosIntOps and open them before structure items that
require
either only usual integer operators +,-,*,/ or only
positive_int operators).

There is another variant, that uses phantom types,
polymorphic variants and subtyping. Compile with
"-pp camlp4r"

====================================================
type any = [= `Pos | `Neg ]
;

type pos = [= `Pos ]
;

exception Range
;

module Int
:
sig

type t +'k = 'z
;

value pos_of_int : int -> t pos
;

value any_of_int : int -> t any
;

value int_of_t : t 'a -> int
;

value pp2p_int_op : (int -> int -> int)
-> t pos -> t pos -> t pos
;

value aa2a_int_op : (int -> int -> int)
-> t any -> t any -> t any
;

end
=
struct

type t +'k = int
;

value pos_of_int x =
if (x < 0)
then
raise Range
else
x
;

value any_of_int x = x
;

value int_of_t x = x
;

value pp2p_int_op op =
fun x y ->
pos_of_int (op x y)
;

value aa2a_int_op op =
fun x y ->
any_of_int (op x y)
;

end
;

open Int
;

value sub_pos = pp2p_int_op -
;

value sub_any = aa2a_int_op -
;

value a = any_of_int 10
;

value p = pos_of_int 15
;

(* now you will see the use of subtyping with
explicit coercion (because there are no implicit
coercions in OCaml).
Value "p&quot; coerced from type "t pos" to type "t any"
and then used in function "sub_any", which has
signature
"value sub_any : t any -> t any -> t any;"
*)

value a_minus_p = sub_any a (p :> t any)
;

value p_minus_a = sub_any (p :> t any) a
;

value () =
Printf.printf "a-p = %i, p-a = %in"
(int_of_t a_minus_p) (int_of_t p_minus_a)

(* outputs: a-p = -5, p-a = 5 *)
;

(* another test: *)

value p2 = pos_of_int (max_int - 5)
;

value add_pos = pp2p_int_op +
;

value () =
try do
{ Printf.printf
"incredible! result=%in"
(int_of_t (add_pos p p2))
(* 15 + max_int - 5 > max_int *)
}
with
[ Range ->
print_string "nice. out of range error.n&quot;
]
;

(* uncommenting this line:
value () = add_pos p a
;
causes error:
This expression has type any Int.t but is here
used with type pos Int.t
Type any = [ `Neg | `Pos ] is not compatible
with type pos = [ `Pos ]
*)

====================================================

So, there do exists subtyping in OCaml.

--
WBR,
dmitry mailto: gds-mlsts%40moldavcable.com">gds-mlstsmoldavcable.com

Messages in this topic (0) Reply (via web post) | Start a new topic

.