# Type definition contains a cycle? **URL:** \ **Category:** Learning\ **Tags:** type-system\ **Created:** [July 24, 2021, 8:01pm UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192 "2021-07-24T20:01:30Z")\ **Posts on this page:** 14\ **Page:** 1
**Author:** ![drorlb](https://avatars.discourse-cdn.com/v4/letter/d/ea666f/32.png) [@drorlb](https://discuss.ocaml.org/u/drorlb)\ **Post date:** [July 24, 2021, 8:01pm UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/1 "2021-07-24T20:01:30Z")
I’ve been trying to write a simple tree data structure, and cannot quite understand what exactly constitutes a cyclic type definition: This code works: module KMap = Map.Make(K) type 'a dir = 'a entry KMap.t and 'a entry = | Leaf of 'a | Tree of 'a dir and 'a t = 'a dir While replacing the definition of 'a entry with and 'a entry = ('a, 'a dir) Either.t results in “The definition of dir contains a cycle”. This is quite mystifying, since the (working) definition of entry is indeed isomorphic to ('a, 'a dir) Either.t ---
**Author:** ![yawaramin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yawaramin/32/3384_2.png) [@yawaramin](https://discuss.ocaml.org/u/yawaramin)\ **Post date:** [July 25, 2021, 2:27am UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/2 "2021-07-25T02:27:34Z")
It is considered a cyclical type definition when both the recursively-defined types are ‘type abbreviations’ (i.e. type aliases) as opposed to _new_ created types. Here’s a simple example: ```auto # type t = u and u = t;; Error: The definition of t contains a cycle: u ``` And when we make them _new_ types as opposed to _abbreviations:_ ```auto # type t = U of u and u = T of t;; type t = U of u and u = T of t ``` ---
**Author:** ![ifazk](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ifazk/32/836_2.png) [@ifazk](https://discuss.ocaml.org/u/ifazk)\ **Post date:** [July 25, 2021, 2:59am UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/3 "2021-07-25T02:59:19Z")
I don’t see a good reason for this to produce an error - looks like a bug in the type checker to me. I tried out a more minimal example, and got the same error. ```ocaml # module IntMap = Map.Make(Int);; # type 'a dir = 'a entry IntMap.t and 'a entry = ('a, 'a dir) Either.t;; Error: The definition of dir contains a cycle: 'a entry ``` ---
**Author:** ![Chet\_Murthy](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/chet_murthy/32/1501_2.png) [@Chet\_Murthy](https://discuss.ocaml.org/u/Chet_Murthy)\ **Post date:** [July 25, 2021, 3:11am UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/4 "2021-07-25T03:11:25Z")
Per Yawar, that’s a cycle, too, yes? The constraint makes sense: you expand all type-abbreviations, and if you end up with an infinite expansion or an expansion that doesn’t terminate, you raise an error. In the example, we might want for `'a dir` to not get expanded: but abbreviations are not supposed to be special: at least, that’s how I’ve always thought they were to be treated. ---
**Author:** ![ifazk](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ifazk/32/836_2.png) [@ifazk](https://discuss.ocaml.org/u/ifazk)\ **Post date:** [July 25, 2021, 3:34am UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/5 "2021-07-25T03:34:27Z")
Okay, I think I understand why the type checker disallows this after reading [this](https://caml.inria.fr/pub/docs/oreilly-book/html/book-ora208.html). Consider an even more minimal example… ```ocaml # type 'a entry = ('a, 'a entry IntMap.t) Either.t;; Error: The type abbreviation entry is cyclic ``` This is cyclic, as in self referential, but it’s not a cycle of abbreviations. As the OP states, this is isomorphic to the allowed type definition ```ocaml # type 'a entry = Left of 'a | Right of 'a entry IntMap.t;; type 'a entry = Left of 'a | Right of 'a entry IntMap.t ``` But the type checker treats `IntMap.t` and `Either.t` as abstract, it doesn’t know if it’s a type of variants, or if it is a product type… What if we had: ```ocaml type 'a IntMap.t = 'a * 'a type ('a,'b) Either.t = 'a * 'b ``` Then `'a entry` would be isomorphic to: ```ocaml type 'a entry = 'a * ('a entry * 'a entry) ``` The linked article describes why type abbrevations of the above kind are problematic. Since the type checker doesn’t know if `IntMap.t` and `Either.t` types are variants or products (or some other kind of type), it conservatively complains about types being cyclic. ---
**Author:** ![ifazk](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ifazk/32/836_2.png) [@ifazk](https://discuss.ocaml.org/u/ifazk)\ **Post date:** [July 25, 2021, 4:08am UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/6 "2021-07-25T04:08:48Z")
I’m not convinced that “infinite expansion” line of reasoning is works well. Expanding `'a dir` or `'a entry` does not seem problematic for me, it’s the not expanding `Either.t` that’s the problem. ---
**Author:** ![drorlb](https://avatars.discourse-cdn.com/v4/letter/d/ea666f/32.png) [@drorlb](https://discuss.ocaml.org/u/drorlb)\ **Post date:** [July 25, 2021, 4:46am UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/7 "2021-07-25T04:46:19Z")
OK then, but why would the type checker treat Either.t as abstract? the module signature exposes the usual _variant_ definition, so it’s definitely not `('a, 'b) either = 'a * 'b` (which would make the entire definition cyclic, unfounded, and doubleplusungood). Back to the abbreviation vs. definition issue, it amounts to beta-expansion at the (non-abstract) type level. I would have expected referential transparency here. ---
**Author:** ![yawaramin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yawaramin/32/3384_2.png) [@yawaramin](https://discuss.ocaml.org/u/yawaramin)\ **Post date:** [July 25, 2021, 5:05am UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/8 "2021-07-25T05:05:36Z")
From a couple of sources, it seems allowing these recursive type abbreviations can lead to accepting ill-formed values: [https://caml.inria.fr/pub/docs/oreilly-book/html/book-ora209.html](https://caml.inria.fr/pub/docs/oreilly-book/html/book-ora209.html) > If this mode may be useful in some cases, it tends to accept the typing of too many values, giving them types that are not easy to read. [https://ocaml.org/api/Lazy.html#TYPEt](https://ocaml.org/api/Lazy.html#TYPEt) > Note: if the program is compiled with the `-rectypes` option, ill-founded recursive definitions of the form `let rec x = lazy x` or `let rec x = lazy(lazy(...(lazy x)))` are accepted by the type-checker and lead, when forced, to ill-formed values that trigger infinite loops in the garbage collector and other parts of the run-time system. Without the `-rectypes` option, such ill-founded recursive definitions are rejected by the type-checker. ---
**Author:** ![ifazk](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ifazk/32/836_2.png) [@ifazk](https://discuss.ocaml.org/u/ifazk)\ **Post date:** [July 25, 2021, 5:40am UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/9 "2021-07-25T05:40:42Z")
> [@drorlb](#): > > amounts to beta-expansion at the (non-abstract) type level But that’s it though, OCaml does not do a lot of computation at the type level. You’ll have to ask the language designers and implementers for their own reasoning, but from my limited experience with implementing type checkers I would find it very weird to do beta-expansion (or delta-expansion) at the type level for a language like OCaml. It’s not trying to be a fully dependently typed language, so there won’t be a lot of benefit from complicating the type checker and wrecking error messages. ---
**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\ **Post date:** [July 26, 2021, 3:23pm UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/10 "2021-07-26T15:23:02Z")
@yawaramin is right: Ocaml makes the distinction between type abbreviations ```ocaml type 'a abbr = int * 'a ``` which create short-hand for type expressions, and are thus subject to the same restriction as ordinary type expressions and type definitions ```ocaml type 'a def = A of 'a ``` which creates new types. The two are fundamentally different in term of equalities: a type abbreviation introduces a new equality between two type expressions (`'a abbr`= `int * 'a`) whereas a type definition introduces a new unique entity with no (known) equality with previously defined types. Consequently, type abbreviations cannot create invalid type expressions. For instance, ```ocaml type 'a t = 'a t list ``` is only valid when regular recursive type expressions have been allowed with the `-rectypes` option. Moreover, non-regular recursive type expressions, for instance ```ocaml type 'a nr = 'a list nr list ``` are never allowed in OCaml ( (which corresponds to a type graph of infinite size even in presence of sharing) and yields this error message: > Error: This recursive type is not regular. > The type constructor nr is defined as > type 'a nr > but it is used as > 'a list nr. > All uses need to match the definition for the recursive type to be regular. For more information, you might be interested in looking at the difference between iso-recursive and equi-recursive types. ---
**Author:** ![garrigue](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/garrigue/32/2644_2.png) [@garrigue](https://discuss.ocaml.org/u/garrigue)\ **Post date:** [July 27, 2021, 3:17pm UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/11 "2021-07-27T15:17:30Z")
While the type checker does not expand `Either.t`, it does not treat it as abstract either. As mentioned by others, it knows that `Either.t` constructs a value, and as a result your type definition is allowed in `-rectypes` modes, which is of course sound (i.e., `-rectypes` is not unsafe). So why is your definition refused by default? This is mainly because allowing it makes type inference less useful at detecting mistakes. Here is an example using `-rectypes`: ```ocaml # let rec append l1 l2 = match l1 with [] -> l2 | a::l -> a :: append a l2;; val append : ('a list as 'a) -> 'a list -> 'a list = ``` About 20 years ago OCaml used to have `-rectypes` as default for some time, but it was eventually decided the confusion caused by accepting such definitions was not worth the added expressive power. Note that the trade-off is different for polymorphic variants and objects. There, recursion is allowed as long as it goes through either a polymorphic variant or object type. ```ocaml # let rec append l1 l2 = match l1 with `Nil -> l2 | `Cons (a,l) -> `Cons (a, append l l2);; val append : ([< `Cons of 'b * 'a | `Nil] as 'a) -> ([> `Cons of 'b * 'c] as 'c) -> 'c = ``` So you could actually write your code by defining `Either.t` as: ```ocaml type ('a,'b) either = [`Left of 'a | `Right of 'b] ``` Note that inferring such equi-recursive types (as mentioned by @octhacron) also comes with some restrictions on the form of recursion allowed (only regular types are allowed, which is weaker than for explicit type definitions). But this is another story (while there does exist a stronger algorithm, it is extremely complex). ---
**Author:** ![jpetkau](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/jpetkau/32/4219_2.png) [@jpetkau](https://discuss.ocaml.org/u/jpetkau)\ **Post date:** [February 9, 2023, 10:52pm UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/12 "2023-02-09T22:52:25Z")
Sorry to revive an old discussion here, not sure where else to post. This seems like a flaw (even a bug) in OCaml. All of the examples for why recursive types lead to confusion have to do with _inferred_ types of functions or data structures. None of them are examples of where a _type alias_ like `type 'a entry = ('a, 'a entry IntMap.t) Either.t` above can cause trouble. But if you enable `-rectypes` to allow the non-problematic cases, you have to also enable all the bad cases from the examples. Are there any examples of where _in a type alias_, allowing recursive types can cause a problem? Motivation: I wanted to create a type like ``` type 'e gast = Int | Sum of ('e * 'e) | ... type ast = ast gast ``` Which is equivalent to defining `ast` as `type ast = Int | Sum of (ast * ast) | ...` but also allows stuff like: ``` type mapper = ('a gast -> 'b) gast fun map_ast : ('a, 'b) mapper -> 'a gast -> 'b gast type 'a with_span = WithSpan of (int, int, 'a) type spanned_ast = spanned_ast gast with_span etc. ``` ---
**Author:** ![garrigue](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/garrigue/32/2644_2.png) [@garrigue](https://discuss.ocaml.org/u/garrigue)\ **Post date:** [February 10, 2023, 12:37am UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/13 "2023-02-10T00:37:44Z")
The problem is that you are introducing a distinction that does not exist. Namely, a type alias is just an alias, strictly equivalent to the type where this alias has been fully expanded. So for it to be valid, the version without alias should be valid too. I understand what you want, and I think many people would like to have that, including me. But this more or less amounts to introducing AI into the type checker, to let it decide which cycles are intentional and which are not. A workaround here is to make ast a one-constructor polymorphic variant type: ```plaintext type ast = [`Fix of ast gast] ``` Another common situation is that you may want to add extra information in ast nodes, and use an object type. Of course, if you don’t care about the node being structural, you can also use a record type (which may be more comfortable actually). ---
**Author:** ![Gopiandcode](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/gopiandcode/32/5346_2.png) [@Gopiandcode](https://discuss.ocaml.org/u/Gopiandcode)\ **Post date:** [February 10, 2023, 3:46am UTC](https://discuss.ocaml.org/t/type-definition-contains-a-cycle/8192/14 "2023-02-10T03:46:38Z")
> [@garrigue](#): > > ```auto > type ast = [`Fix of ast gast] > > ``` In these cases, what I like to do is use a single constructor type with unboxed: ```auto type t = Mk of t shape [@@unboxed] ``` This way, the memory representation of `t` should be the same as the idiomatic original definition, but you can also write functions parametric over nodes: ```auto val pp_shape: (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a shape -> unit val compare_shape: ('a -> 'a -> int) -> 'a shape -> 'a shape -> int val op: 'a shape -> op val children: 'a shape -> 'a list val map_children: 'a shape -> ('a -> 'b) -> 'b shape val make : op -> 'a list -> 'a shape ``` I use this in [ego](https://github.com/verse-lab/ego) to allow users to supply modules with relatively arbitrary term structures while still allowing building generic components on top of them ([ego/lib/language.ml at master · verse-lab/ego · GitHub](https://github.com/verse-lab/ego/blob/master/lib/language.ml#L17))