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

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 `fmap`s 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 `show`ish 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?

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

``````

``````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

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

@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!

@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?

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
``````

I think that you are missing `-rectypes` compiler switch

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