Attempting to create 'recursion schemes' in ocaml

Learning
,
1

Hey All,

I’ve taught myself enough OCaml to be dangerous and so of course that means I’m trying to port some interesting haskell ideas. I recently learned about recursion schemes (I’ve been using the series from https://blog.sumtypeofway.com/archive.html as a guide), and am running in to some weird issues when going from hard coded types to a module functor.

I’ve managed to get most of the recursion schemes working when dealing with a known type like this example:

module Expr = struct
  module Open = struct
    type 'a t =
      | Unit
      | Var of { id: string }
      | Fn of { arg: string; body: 'a }
      | App of { fn: 'a; arg: 'a }

    let map f = function
      | Unit | Var _ as t -> t
      | Fn { arg; body } -> Fn { arg; body = f body }
      | App { fn; arg } -> App { fn = f fn; arg = f arg }

    (* fold *)
    let rec cata (f : 'a t -> 'a) (x: 'b t) = map (cata f) x |> f

    (* unfold *)
    let rec ana (f : 'a -> 'a t) x = f x |> map (ana f)
  end

  type t = t Open.t

  let map : (t -> t) -> t -> t = Open.map

  (* use cata to calculate the depth of the tree without thinking about recursion *)
  let depth : t -> int = Open.cata (function
    | Unit | Var _ -> 1
    | Fn { body; _ } -> body + 1
    | App { fn; arg } -> fn + arg + 1
  )
end

This works fantastically and I’ve had no trouble extending it to some of the other schemes (para, apo, histo, futu, etc). I am having trouble turning this in to a reusable module functor though.

(* I resisted calling this 'functor' *)
module type Mappable = sig
  type 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end

module Recursive = struct
  module M (M: Mappable) = struct
    type 'a t = 'a M.t
    
    let rec cata (f : 'a t -> 'a) (x: 'b t) = M.map (cata f) x |> f
  end
end

When compiling this, I get a type error on x:

Error: This expression has type 'b t = 'b M.t
       but an expression was expected of type 'b t M.t
       Type 'b is not compatible with type 'b t = 'b M.t 
       The type variable 'b occurs inside 'b t

I have tried tweaking the type signature and such but can’t seem to get it working. Does anyone know what I’m doing wrong here? I wouldn’t be surprised if I have a really dumb mistake - this stuff is pretty mind bending.

Thanks for any help!

1 Like
2

It can be done by guarding the recursion with

module M (M: Mappable) = struct
  type 'a t = W of 'a t M.t [@@unboxed]
  let rec cata f (W x) = f(M.map (cata f) x)
end

And this works even without -rectypes.

With rectypes enabled, we just need to have one layer of injective wrapper (because recursive type equations are only allowed on data type constructors and not abstract types):

module M (M: Mappable) = struct
    type 'a w = W of 'a M.t [@@unboxed]
    let rec cata f (W x) = f(M.map (cata f) x)
  end
1 Like
3

I’m trying to understand what is going on here. If I think about it correctly, the introduction of a dummy unary constructor ‘W’ (in type 'a t = W of 'a t M.t in @octachron answer) allows for the creation of a fresh type, similar to haskell “newtype” keyword (I never worked with Haskell but I assume this is what it does). Is it correct ? If so, this makes me wonder if a “newtype” keyword would be useful in ocaml. Also, why using “unboxed” ? Until now I thought this was mostly a matter of getting a better runtime representation (Here I guess there is no need to allocate any space for a tag), does it have any other purpose here ? Thanks in advance

4

The [@@unboxed] attribute is just a personal idiosyncrasy to signal that the data type only matters at the type level. This unary constructor is here to introduce a new type constructor with better properties than the abstracted 'a t. The original issue here is that one cannot add recursive equations to an abstract types even with -rectypes. The definition of type 'a t makes it an ordinary (isorecursive) type and thus both fixes the issue and remove the need for -rectypes.

With -rectypes another option is to introduce a dummy identity types to carry the equation:

type 'a id = Id of 'a
module Recursive = struct
  module M (M: Mappable) = struct
    type 'a t = 'a M.t
    let rec cata (f : 'a id t -> 'a) (Id x) = M.map (cata f) x |> f
  end
end

(Also it is a bad sign that you are using -rectypes because this is not a feature supported by Haskell, something may have gone wrong with your translation.)

1 Like