I would like to write catamorphism in OCaml for any endofunctor (in terms of types) as a functor (in terms of OCaml):
module type Functor = sig
type 'a t
(* ... *)
end
module Make(F : Functor) = struct
type fix_t = 'a F.t as 'a
(* ... *)
end
But this code produces an error: "The type variable 'a occurs inside 'a F.t".
I know that there is "-rectypes" flag for OCaml compiler, and following type definition is accepted in place of fix_t: type fix_list = 'a list as 'a.
So I think that an error produced by unknown type t, but it looks strange for me, that type checker distinguish between known and unknown types here.
Even with -rectypes, recursive types must be contractive: all recursive variables must occur as arguments of builtin or datatype type constructors. Without this constraint, equations of the form
type 'a id = 'a
type t = 'a id as 'a
could be accepted and would allow multiple incomparable solutions (for instance t=int or t=float).
Thus, it is simpler to avoid -rectypes, and use an explicit constructor for guarding recursion:
type fix = Fix of fix t [@@unboxed]