Re: [Caml-list] Late adding of type variable constraints

[Mikhail Mandrykin <mandrykin@ispras.ru>]

On Friday, September 04, 2015 07:58:26 PM Markus Mottl wrote:
> I see.  So it's not really a matter of soundness, but the type checker
> changes would presumably be overly intrusive and possibly cause issues
> with efficiency.  Ultimately, I wanted to be able to constrain type
> variables via a functor argument, which is also apparently not
> possible.
> 
> Maybe there are alternative solutions to what I'm trying to do, which
> is actually a quite neat type system challenge:
> 
> Imagine you have a datastructure that is parameterized over an unknown
> number of type variables.  Given such a datastructure, I want to be
> able to map all these type variables from one type to another while
> preserving the "skeleton" of that structure, but without limiting the
> skeleton constructors to a specific number of type variables.
 
Not sure if it's exactly what's desired, but I'd suggest Format-like 
implementation in spirit of the following:

(* The mapper "format" GADT, support for pairs, options, results and type 
variables *)
type ('c, 'r, 'i, 'o) mfmt =
(* 'c -- continuation,
    'r -- result of the form (('a -> 'b) -> ... -> ('y -> 'z) -> 'c),
    'i -- input type, o -- output type *)
  | T_v : ('c, ('e -> 'f) -> 'c, 'e, 'f) mfmt
  | Pair :
      ('r1, _ -> _ as 'r2, 'i1, 'o1) mfmt *
      ('c, _ -> _ as 'r1, 'i2, 'o2) mfmt ->
    ('c, 'r2, 'i1 * 'i2, 'o1 * 'o2) mfmt
  | Option : ('c, _ -> _ as 'r, 'i, 'o) mfmt -> ('c, 'r, 'i option, 'o option) 
mfmt
  | Result :
      ('r1, _ -> _ as 'r2, 'i1, 'o1) mfmt *
      ('c, _ -> _ as 'r1, 'i2, 'o2) mfmt ->
    ('c, 'r2, ('i1, 'i2) result, ('o1, 'o2) result) mfmt
  constraint 'r = 'x -> 'y

(* The CPS mapper generator, accepts continuation after mapper "format" *)
let rec map : type a y z d e x. (x -> e, (y -> z), a, d) mfmt -> ((a -> d) -> 
x -> e) -> (y -> z) =
  function
  | T_v -> fun c f -> c f
  | Pair (m1, m2) ->
    fun c -> map m1 @@ fun f1 -> map m2 @@ fun f2 ->c @@ fun (a, b) -> f1 a, 
f2 b
  | Option m ->
    fun c -> map m @@ fun f -> c (function Some a -> Some (f a) | None -> 
None)
  | Result (m1, m2) ->
    fun c -> map m1 @@ fun f1 -> map m2 @@ fun f2 -> c @@
      function
      | Ok a -> Ok (f1 a)
      | Error b -> Error (f2 b)

(* The final mapper generator *)
let map f = map f (fun x -> x)

(* Examples *)

 (* Mapper for the skeleton (('a, 'b) option, 'c option * 'd) result *)
let map_1 m1 m2 m3 m4 = map (Result (Pair (T_v, Option T_v), Pair (Option T_v, 
T_v))) m1 m2 m3 m4;;

let f = map_1 succ int_of_string string_of_int pred;;

f (Ok (5, Some "6"));;
(* Ok (6, Some 6) *)
f (Error (None, 0));;
(* Error (None, -1) *)

(* Mapper for skeleton ('a * ('c * 'e), 'g option * 'i option) result *)
let map_2 m1 m2 m3 m4 m5 = map (Result (Pair (T_v, Pair (T_v, T_v)), Pair 
(Option T_v, Option T_v))) m1 m2 m3 m4 m5;;

let f =
  map_2
    succ
    (fun (a, b) -> Some (int_of_string b, string_of_int a))
    float_of_int
    pred
    (function Ok a -> Some (Error a) | Error a -> Some (Ok a));;

f (Ok (1, ((6, "7"), 0)));;
(* Ok (2, (Some (7, "6"), 0.)) *)
f (Error (None, Some (Ok "5")));;
(* Error (None, Some (Some (Error "5"))) *)

With open extensible types it's possible to extend this approach to unlimited 
number of supported basic skeleton types, but the resulting usages would look 
somewhat messy, e.g.:

let map_1 m1 m2 m3 m4 =
  let open T_v in
  let module O = Option (T_v) in
  let module P1 = Pair (T_v) (O) in
  let module P2 = Pair (O) (T_v) in
  let module R = Result (P1) (P2) in
  R.map (R.Result (P1.Pair (T_v, O.Option T_v), P2.Pair (O.Option T_v, T_v))) 
m1 m2 m3 m4

-- 
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin@ispras.ru