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?