How to tie the knot for non-regular data type without falling to higher-kindness?

Learning
,
1

Let’s have an example of non-regular mutually recursive data types, for example

type 'a s = SS of 'a
and t = int s
and u = float s

And we want to create transformation functions for these three types. The transformation functions of two sorts: showing stuff

val show_s : ('a -> string) -> 'a s -> string
val show_t : t -> string
val show_u : u -> string

and mapping stuff (I actually want fmaps but I shrinked typed here for simplicity)

val map_s : ('a -> 'a) -> 'a s -> 'a s
val map_t : t -> t
val map_u : u -> u

And I want to write separate function for each type and tie these three functions to the knot using another function (I call it fix). I want this fix function to be the same for showing and fmaping. A already have the fix functions per transformation kind which have the same body but have different types.

Let me show that naive approach fails. These are the initial transformation for showing

let show0_s fa _s _t _u (SS a) = fa a
let show0_t     s _t _u        = s (sprintf "%d") s _t _u
let show0_u     s _t _u        = s (sprintf "%f") s _t _u

Let’s try to tie the knot

let fix1 (s0,t0,u0) =
  let rec s = fun fa -> s0 fa s0 t u
  and t = fun what -> t0 s0 t u what
  and u what = u0 s0 t u what
  in
  (s,t,u)

let (show_s,show_t,show_u) = fix1 (show0_s, show0_t, show0_u)
                                                      ^^^^^^^

Blah, blah, Type float is not compatible with type int

Let’s workaround this issue by introducing existential quantification. It works for showish functions. We start from initial implementations which abuse existential quantification

type  init2s =
  { s_init2: 'a . ('a -> string) ->
                  init2s ->  init2t ->  init2u ->
                  'a s -> string }
and  init2t =
  { t_init2: init2s ->  init2t ->  init2u -> t -> string }
and  init2u = 
  { u_init2: init2s ->  init2t ->  init2u -> u -> string }

let show2_s = { s_init2 = (fun fa _s _t _u (SS a) -> fa a) }
let show2_t = { t_init2 = (fun     s t u -> s.s_init2 (sprintf "%d") s t u) }
let show2_u = { u_init2 = (fun     s t u -> s.s_init2 (sprintf "%f") s t u) }

type 's wrap1s = { s_trf1: 'a . ('a -> 's) -> 'a s -> 's }
type 's wrap1t = { t_trf1:                       t -> 's }
type 's wrap1u = { u_trf1:                       u -> 's }


let fix2 (s0,t0,u0) =
  let rec s = { s_trf1 = fun fa subj -> s0.s_init2 fa s0 t0 u0 subj }
  and t = { t_trf1 = fun subj -> t0.t_init2 s0 t0 u0 subj }
  and u = { u_trf1 = fun subj -> u0.u_init2 s0 t0 u0 subj }
  in
  (s,t,u)

let () =
  let s,t,u = fix2 (show2_s,show2_t,show2_u) in
  let () = printf "%s\n%!" @@ s.s_trf1 (sprintf "%S") (SS "asdf") in
  let () = printf "%s\n%!" @@ s.s_trf1 (sprintf "%b") (SS true) in
  let () = printf "%s\n%!" @@ t.t_trf1 (SS 42) in
  let () = printf "%s\n%!" @@ u.u_trf1 (SS 3.1415) in
  ()

The problem is that approach doesn’t scale for fmap-like function. In the example above the result type is string with existenatial variable 'a but for fmap we need the result type to be parametrized by this existential 'a. And hence, if fix function is polymorphic by the type of functions’ results, the 'result type should be parametrizable by existential variable. I tried to use library Higher but the locally introduced type escapes the scope. The wrong piece of codeis below, but I doubt it will be helpful

open Higher
type ('syns,'syna,'synt,'synu) init3s =
  { s_init3: 'a . ('a -> ('a,'syna) app) ->
      ('syns,'syna,'synt,'synu) init3s ->
      ('syns,'syna,'synt,'synu) init3t ->
      ('syns,'syna,'synt,'synu) init3u ->
      'a s -> ('a,'syns) app }
and  ('syns,'syna,'synt,'synu) init3t =
  { t_init3: 'syn .
      ('syns,'syna,'synt,'synu) init3s ->
      ('syns,'syna,'synt,'synu) init3t ->
      ('syns,'syna,'synt,'synu) init3u ->
      t -> 'syn }
and  ('syns,'syna,'synt,'synu) init3u =
  { u_init3: 'syn .
      ('syns,'syna,'synt,'synu) init3s ->
      ('syns,'syna,'synt,'synu) init3t ->
      ('syns,'syna,'synt,'synu) init3u ->
      u -> 'synu }

let show3_s = { s_init3 = (fun fa _s _t _u (SS a) -> fa a) }
let show3_t = { t_init3 = (fun     s t u ->
    let module HS = Higher.Newtype1(struct type 'a t = 'a s end) in
    let module HA = Higher.Newtype1(struct type 'a t = string end) in
    HS.inj @@ s.s_init3 (fun n -> HA.inj @@ sprintf "%d" n ) s t u)
    (* HA.t escapes its scope     ^^^^^ *)
  }
let show3_u = { u_init3 = (fun     s t u -> s.s_init3 (sprintf "%f") s t u) }

I can’t make the code with Higher work. I thought about passing the first class module out together with the result of transformation but it seems extremely scary. I basically out of ideas. Do you know any other dirty hacks to work around higher kinded types which have appeared because of existentials? Maybe I can throw away existentials to hack non-regularity in some other manner?

2

I think the following meets the above requirements. Here’s the general fixed point operator that can be used for mutually-recursive functions over mutually-recursive types, both show and map:

module FixV(Sym: sig type 'a i end) =
struct
  type fn = { call: 'a. 'a Sym.i -> 'a }
  let fixv f = let rec g = { call = fun x -> (f g).call x } in g
end

Here fixv has essentially the following type:

βˆ€t.((βˆ€Ξ±.Ξ± t β†’ Ξ±) β†’ (βˆ€Ξ±.Ξ± t β†’ Ξ±)) β†’ (βˆ€Ξ±.Ξ± t β†’ Ξ±)

β€” that is, it’s a standard call-by-value fixed point operator with some extra polymorphism thrown in to make each function result type dependent on the function argument.

We can build a suitable argument for FixV using a helper functor Index whose argument S turns the types s, t, u, into the types of map and show:

module Index (S: sig type 'a result end) =
struct
  type 'a i =
    | S : ('a S.result -> 'a s S.result) i
    | T : t S.result i
    | U : u S.result i
end

So Index specializes FixV to your types s, t, u, and S further specializes Index for functions map, show, etc.

Here’s Show using FixV. There are four steps: first instantiate FixV with a suitable index; second, write the show functions individually (and non-recursively); third, pass these individual functions to fixv; fourth, project out each function from the result:

module Show =
struct
  module I = Index(struct type 'a result = 'a -> string end)
  include FixV(I)

  let show0_s {call} fa (SS a) = fa a
  let show0_t {call}           = call I.S (sprintf "%d")
  let show0_u {call}           = call I.S (sprintf "%f")

  let show = fixv @@ fun f ->
   { call = fun (type a) (sym : a I.i) : a -> match sym with
     | I.S -> show0_s f
     | I.T -> show0_t f
     | I.U -> show0_u f }

  let show_s x = show.call I.S x
  let show_t x = show.call I.T x
  let show_u x = show.call I.U x
end

Then your test code, adjusted to this interface, works as expected:

let () =
  let s,t,u = Show.(show_s, show_t, show_u) in
  let () = printf "%s\n%!" @@ s (sprintf "%S") (SS "asdf") in
  let () = printf "%s\n%!" @@ s (sprintf "%b") (SS true) in
  let () = printf "%s\n%!" @@ t (SS 42) in
  let () = printf "%s\n%!" @@ u (SS 3.1415) in
  ()

Finally, here’s Map, following the same pattern as Show, and using the same generic fixed point operator:

module Map =
struct
  module I = Index(struct type 'a result = 'a -> 'a end)
  include FixV(I)

  let map0_s {call} fa (SS a) = SS (fa a)
  let map0_t {call}           = call I.S (fun (x:int) -> x)
  let map0_u {call}           = call I.S (fun (x:float) -> x)

  let map = fixv @@ fun f ->
   { call = fun (type a) (sym : a I.i) : a -> match sym with
     | I.S -> map0_s f
     | I.T -> map0_t f
     | I.U -> map0_u f }

  let map_s x = map.call I.S x
  let map_t x = map.call I.T x
  let map_u x = map.call I.U x
end

(It might be possible to eliminate some of the functors using higher, but I think it’s often useful to see things working with the module system first.)

6 Likes
3

These types are not mutually recursive by themselves. Am I missing something?

4

@yawaramin This is simplified case. It can be derived for example from OCaml parse tree or other non-regular data type example.

@yallop this is very peculiar piece of code. I will try to understand the details and adapt for my needs. It seems that I am able to change it for other kinds of transformations. The next step is to see what changes when a number of type parameters changes (haven’t tried it yet). Many thanks!

5

@kakadu How did you get to the point where you were defining fix for the show0 functions? I can’t seem to get the show0 functions to type check on their own even before trying to create recursive versions by tying the knot.

─( 20:57:37 )─< command 0 >────────────────────────────────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # open Core;;
─( 20:57:38 )─< command 1 >────────────────────────────────────────────────────────────────────────────────────────────{ counter: 0 }─
utop #
type 'a s = SS of 'a
and t = int s
and u = float s
let show0_s fa _s _t _u (SS a) = fa a
let show0_t     s _t _u        = s (sprintf "%d") s _t _u
let show0_u     s _t _u        = s (sprintf "%f") s _t _u
;;
Error: This expression has type (int -> string) -> 'a -> 'b -> 'c -> 'd
       but an expression was expected of type 'a
       The type variable 'a occurs inside
       (int -> string) -> 'a -> 'b -> 'c -> 'd

Am I missing something?

6

I think this is @yallop’s solution using Higher if you’re curious:

open Higher

type 'a s = SS of 'a
and t = int s
and u = float s

type 'sym fixfn =  { call : 'a. ('a, 'sym) app -> 'a }
let fixv f =
  let rec g = { call = fun x -> (f g).call x } in g

type ('a, 'result) index =
  | S : (('a, 'result) app -> (('a s, 'result) app), 'result) index
  | T : ((t, 'result) app, 'result) index
  | U : ((u, 'result) app, 'result) index

module Show = struct
  open Format
  module R = Higher.Newtype1(struct type 'a t = 'a -> string end)
  module I = Higher.Newtype1(struct type 'a t = ('a, R.t) index end)

  let show0_s {call} fa = R.inj (fun (SS a) -> (R.prj fa) a)
  let show0_t {call} = call (I.inj S) (R.inj (sprintf "%d"))
  let show0_u {call} = call (I.inj S) (R.inj (sprintf "%f"))

  let show = fixv @@ fun (f : I.t fixfn) ->
   { call = fun (type a) (sym : (a, I.t) app) : a -> match I.prj sym with
     | S -> show0_s f
     | T -> show0_t f
     | U -> show0_u f }

  let show_s f x = R.prj (show.call (I.inj S) (R.inj f)) x
  let show_t x = R.prj (show.call (I.inj T)) x
  let show_u x = R.prj (show.call (I.inj U)) x
end

module Map = struct
  open Format
  module R = Higher.Newtype1(struct type 'a t = 'a -> 'a end)
  module I = Higher.Newtype1(struct type 'a t = ('a, R.t) index end)

  let map0_s {call} fa = R.inj (fun (SS a) -> SS ((R.prj fa) a))
  let map0_t {call} = call (I.inj S) (R.inj (fun (x:int) -> x))
  let map0_u {call} = call (I.inj S) (R.inj (fun (x:float) -> x))

  let map = fixv @@ fun (f : I.t fixfn) ->
   { call = fun (type a) (sym : (a, I.t) app) : a -> match I.prj sym with
     | S -> map0_s f
     | T -> map0_t f
     | U -> map0_u f }

  let map_s f x = R.prj (map.call (I.inj S) (R.inj f)) x
  let map_t x = R.prj (map.call (I.inj T)) x
  let map_u x = R.prj (map.call (I.inj U)) x
end
7

I think that you are missing -rectypes compiler switch

8

And here’s a version using Higher with the fixpoint combinator specialised to just these types:

open Higher

type 'a s = SS of 'a
and t = int s
and u = float s

type 'result fixfn =
  { call_s : 'a. ('a, 'result) app -> (('a s, 'result) app);
    call_t : unit -> (t, 'result) app;
    call_u : unit -> (u, 'result) app; }

let fixv f =
  let rec g =
    { call_s = (fun fn -> (f g).call_s fn);
      call_t = (fun () -> (f g).call_t ());
      call_u = (fun () -> (f g).call_u ()); }
  in
  g

module Show = struct
  open Format
  module R = Higher.Newtype1(struct type 'a t = 'a -> string end)

  let show = fixv @@ fun {call_s; _} ->
   { call_s =
       (fun (type a) (fa : (a, R.t) app) : (a s, R.t) app ->
          R.inj (fun (SS a) -> (R.prj fa) a));
     call_t =
       (fun () -> call_s (R.inj (sprintf "%d")));
     call_u =
       (fun () -> call_s (R.inj (sprintf "%f"))); }

  let show_s f x = R.prj (show.call_s (R.inj f)) x
  let show_t x = R.prj (show.call_t ()) x
  let show_u x = R.prj (show.call_u ()) x
end

module Map = struct
  open Format
  module R = Higher.Newtype1(struct type 'a t = 'a -> 'a end)

  let map = fixv @@ fun {call_s; _} ->
   { call_s =
       (fun (type a) (fa : (a, R.t) app) : (a s, R.t) app ->
          R.inj (fun (SS a) -> SS ((R.prj fa) a)));
     call_t =
       (fun () -> call_s (R.inj (fun (x : int) -> x)));
     call_u =
       (fun () -> call_s (R.inj (fun (x : float) -> x))); }

  let map_s f x = R.prj (map.call_s (R.inj f)) x
  let map_t x = R.prj (map.call_t ()) x
  let map_u x = R.prj (map.call_u ()) x
end
1 Like