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

[Mikhail Mandrykin <mandrykin@ispras.ru>]

On Wednesday, September 09, 2015 10:00:34 AM Markus Mottl wrote:

> In my case I also need to define a type ('a t) such that I can pass it
> on in a functor.  The functor body needs to know that invariants are
> maintained after each mapping: the skeleton, as captured by t, and
> that the same constraints hold for type parameter 'a across mappings.
> Only then can the functor body easily map back and forth between
> various encodings of the type parameters while maintaining the
> skeleton.
> 

Probably the defunctionalization encoding used in the paper on Lightweight 
Higher-Kinded Polymorphism in OCaml 
(https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf) can help in some way. The corresponding library and examples 
are available at https://github.com/ocamllabs/higher.

The implementation used in the library doesn't perfectly fit the case, because 
the suggested encoding puts the type `t' capturing the type skeleton on an 
unknown depth inside the list of type constructor applications.  I tried the 
following slight variation on the initial encoding:

type ('p, 'f) app = App of 'p * 'f
type nil
type ('a, 'b) typ = .. (* To be used as `('a, M.t) typ' for different `M.t's 
*)

(* Slight change made to pull `M.t' (see below) from the inside of the 
parameter list *)

(* A couple of helper functors similar to the ones in the library *)

module Newtype1 (T : sig type 'a t end) =
struct
  type 'a s = 'a T.t
  type t
  type (_, _) typ += Mk : 'a T.t -> (('a, nil) app, t) typ
  let inj v = Mk v
  let prj (Mk v) = v
end

module Newtype2 (T : sig type ('a, 'b) t end) =
struct
  type ('a, 'b) s = ('a, 'b) T.t
  type t
  type (_, _) typ += Mk : ('a, 'b) T.t -> (('a, ('b, nil) app) app, t) typ
  let inj v = Mk v
  let prj (Mk v) = v
end

(* The common signature for all the skeletons regardless of the number of type 
parameters *)
module type S =
sig
  type t
  type ('a, 'b) mapper = ('a, t) typ -> ('b, t) typ
  
  type task = (* This is just an example of how the mappers can be used *)
      Task :
        ('a, t) typ *
        ('a, 'b) mapper * ('b, 'c) mapper * ('c, 'a) mapper *
        (('a, t) typ -> string) -> task
end

(* The skeleton is captured by M.t .*)
(* The passed type is "('a, M.t) typ" *)
module Performer (M : S) =
struct
  let perform =
    function
    | M.Task  (v, m1, m2, m3, s) ->
      let s = v |> m1 |> m2 |> m3 |> s in
      prerr_endline s
end

(* Example skeleton definitions *)

module Pair =
struct
  include Newtype2 (struct type ('a, 'b) t = 'a * 'b end)
  type ('a, 'b) mapper = ('a, t) typ -> ('b, t) typ
  type task =
      Task : ('a, t) typ * ('a, 'b) mapper * ('b, 'c) mapper * ('c, 'a) mapper 
* (('a, t) typ -> string) -> task
end

module Singleton =
struct
  include Newtype1 (struct type 'a t = 'a end)
  type ('a, 'b) mapper = ('a, t) typ -> ('b, t) typ
  type task =
      Task : ('a, t) typ * ('a, 'b) mapper * ('b, 'c) mapper * ('c, 'a) mapper 
* (('a, t) typ -> string) -> task
end

(* Example usages *)

let mappers =
  (fun (x, y) -> int_of_string x, int_of_string y),
  (fun (x, y) -> float_of_int x, float_of_int y),
  (fun (x, y) -> string_of_float x, string_of_float y)

let pair_tasks =
  let open Pair in
  let m1, m2, m3 = mappers in
  let wrap m x = x |> prj |> m |> inj in
  let m1, m2, m3 = wrap m1, wrap m2, wrap m3 in
  [|Task (inj ("1", "2"), m1, m2, m3, fun x -> let a, b = prj x in a ^ ", " ^ 
b);
    Task (inj (1, 2), m2, m3, m1, fun x -> let a, b = prj x in string_of_int a 
^ ", " ^ string_of_int b)|]

let mappers = int_of_string, float_of_int, string_of_float

let singleton_tasks =
  let open Singleton in
  let m1, m2, m3 = mappers in
  let wrap m x = x |> prj |> m |> inj in
  let m1, m2, m3 = wrap m1, wrap m2, wrap m3 in
  [|Task (inj (1), m2, m3, m1, fun x -> "Just " ^ string_of_int @@ prj x);
    Task (inj ("1"), m1, m2, m3, fun x -> "Just " ^ prj x)|]

module Pair_performer = Performer (Pair)
module Single_performer = Performer (Singleton)

let () = Pair_performer.perform pair_tasks.(0)
(* "1", "2" --> 1, 2 --> 1., 2. --> "1.", "2." --> "1., 2."*)
(* Stderr: 1., 2. *)
let () = Single_performer.perform singleton_tasks.(1)
(* "1" --> 1 --> 1. --> "1." --> "Just 1." *)
(* Stderr: Just 1.*)

let () = Pair_performer.perform pair_task.(1)
(* 1, 2 -> 1., 2. --> "1.", "2." --> Failure: int_of_string *)

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