Why are mutually recursive type aliases with lists are cyclic?

Learning
1

I’m trying to define two mutually recursive types like this;

type transition = symbol * state
and state =
  | Nil
  | Cons of transition * state

which works fine, but then it leaves me wondering: Isn’t this logically the same as

type transition = symbol * state
and state = transition list

?

Why does the second case gets compiler error

The type abbreviation transition is cyclic:
         transition = symbol * state,
         symbol * state contains state,
         state = transition list,
         transition list contains transition

but the first one doesn’t?

2

I sure am not a type theorist, nor an expert in the OCaml type inference algorithm, but in the second case you have two type abbreviations (though if you expand state it looks like constructors and not an infinite recursion, sure sure) whereas in the first, you have manifestly that state is a constructor data-type. Maybe it’s as simple as that. You can’t provide a collection of type-abbreviations that are mutually-recursive, full stop.

3

By default, the OCaml compiler rejects recursive types. You can enable them by passing option -rectypes. The downside is that error messages might become much less readable, since the compiler can now infer recursive types, which tend to hide the root location of bugs.

4

In your first example, you are defining a new nominal type:

type transition = symbol * state
and state =
  | Nil
  | Cons of transition * state

In particular, if we expand the first type abbreviation, we get

type state =
  | Nil
  | Cons of (symbol * state) * state

And thus this is an usual definition of a recursive nominal type, where the recursion is guarded behind the constructors (aka iso-recursion). In other words, the type of Nil or
Cons (('a', Nil), Nil) is just state.

Contrarily, your second example only contains abbreviations for type expressions:

type transition = symbol * state
and state = transition list

and the recursive type expression appears clearly if we expand the first abbreviation:

type state = (symbol * state) list

Here it is the type expression which is recursive (aka equi-recursion): the type of
[('a', [])] seen as a state would be (symbol * 'state) list as 'state. This is only allowed with -rectypes or when the recursion goes through a polymorphic variants or objects:

type state = [ `Cons of symbol * state | `Nil ]

Moreover, beware that this definition of an automaton only works if the automaton digraph is acyclic, or if you define it whole-piece in a recursive value definition (which doesn’t scale well).

6 Likes