# How to tie the knot for non-regular data type without falling to higher-kindness?
**URL:** https://discuss.ocaml.org/t/how-to-tie-the-knot-for-non-regular-data-type-without-falling-to-higher-kindness/3240
**Category:** Learning
**Tags:** higher-kinds, existentials
**Created:** [January 28, 2019, 3:12pm UTC](https://discuss.ocaml.org/t/how-to-tie-the-knot-for-non-regular-data-type-without-falling-to-higher-kindness/3240 "2019-01-28T15:12:56Z")
**Posts on this page:** 8
**Page:** 1
### Author:  [@Kakadu](https://discuss.ocaml.org/u/Kakadu)
#### Post date: [January 28, 2019, 3:12pm UTC](https://discuss.ocaml.org/t/how-to-tie-the-knot-for-non-regular-data-type-without-falling-to-higher-kindness/3240/1 "2019-01-28T15:12:56Z")
Let’s have an example of non-regular mutually recursive data types, for example
```ocaml
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
```ocaml
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)
```ocaml
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
```ocaml
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
```ocaml
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
```ocaml
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) }
```
```ocaml
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](https://github.com/ocamllabs/higher) but the locally introduced type escapes the scope. The wrong piece of codeis below, but I doubt it will be helpful
```ocaml
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?
---
### Author:  [@yallop](https://discuss.ocaml.org/u/yallop)
#### Post date: [January 28, 2019, 8:03pm UTC](https://discuss.ocaml.org/t/how-to-tie-the-knot-for-non-regular-data-type-without-falling-to-higher-kindness/3240/2 "2019-01-28T20:03:27Z")
> [@Kakadu](#):
>
> > 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.
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`:
```auto
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:
```auto
∀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`:
```auto
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:
```auto
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:
```auto
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:
```auto
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.)
---
### Author:  [@yawaramin](https://discuss.ocaml.org/u/yawaramin)
#### Post date: [January 29, 2019, 8:04pm UTC](https://discuss.ocaml.org/t/how-to-tie-the-knot-for-non-regular-data-type-without-falling-to-higher-kindness/3240/3 "2019-01-29T20:04:04Z")
> [@Kakadu](#):
>
> ````auto
> type 'a s = SS of 'a
> and t = int s
> and u = float s```
>
> ````
These types are not mutually recursive by themselves. Am I missing something?
---
### Author:  [@Kakadu](https://discuss.ocaml.org/u/Kakadu)
#### Post date: [January 29, 2019, 8:08pm UTC](https://discuss.ocaml.org/t/how-to-tie-the-knot-for-non-regular-data-type-without-falling-to-higher-kindness/3240/4 "2019-01-29T20:08:17Z")
@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!
---
### Author:  [@ddickstein](https://discuss.ocaml.org/u/ddickstein)
#### Post date: [February 25, 2019, 2:00am UTC](https://discuss.ocaml.org/t/how-to-tie-the-knot-for-non-regular-data-type-without-falling-to-higher-kindness/3240/5 "2019-02-25T02:00:14Z")
@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?
---
### Author:  [@lpw25](https://discuss.ocaml.org/u/lpw25)
#### Post date: [February 25, 2019, 8:24am UTC](https://discuss.ocaml.org/t/how-to-tie-the-knot-for-non-regular-data-type-without-falling-to-higher-kindness/3240/6 "2019-02-25T08:24:42Z")
I think this is @yallop’s solution using `Higher` if you’re curious:
```ocaml
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
```
---
### Author:  [@Kakadu](https://discuss.ocaml.org/u/Kakadu)
#### Post date: [February 25, 2019, 10:37am UTC](https://discuss.ocaml.org/t/how-to-tie-the-knot-for-non-regular-data-type-without-falling-to-higher-kindness/3240/7 "2019-02-25T10:37:59Z")
I think that you are missing `-rectypes` compiler switch
---
### Author:  [@lpw25](https://discuss.ocaml.org/u/lpw25)
#### Post date: [February 25, 2019, 10:44am UTC](https://discuss.ocaml.org/t/how-to-tie-the-knot-for-non-regular-data-type-without-falling-to-higher-kindness/3240/8 "2019-02-25T10:44:09Z")
And here’s a version using `Higher` with the fixpoint combinator specialised to just these types:
```ocaml
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
```