Most type systems permit some flavour of recursive types, allowing the programmer to define, say, the type representing lists of integers. A consists of either the empty list, or a pair of an integer and a , giving the recursive equation: There are two ways to interpret the symbol above:
Isorecursive types: there is an explicitly defined datatype/class , and we must use its constructors/methods to convert between and . The symbol is read as "is isomorphic to".
Equirecursive types: the types and are the same type, because is identified with the infinite expansion: The symbol is read as "equals".
With equirecursive types, there can only be a single solution to a recursive equation. If I have another type satisfying , then the infinite expansions of and are equal, so . With isorecursive types, on the other hand, there can be two different datatypes/classes with the same pattern of recursion, which the type system does not necessarily consider equal.
The assumption that recursive type equations have only a single solution can lead to unsoundness when combined with higher-kinded types. If it is possible to abstract over a type constructor and two types satisfying: then type systems equirecursive types will assume that , since they have the same infinite expansion .
This is unsound for arbitrary type-level functions because there can be multiple solutions for . For instance:
This problem has arisen in OCaml1:
(* Counterexample by Stephen Dolan *) type (_, _) eq = Eq : ('a, 'a) eq let cast : type a b . (a, b) eq -> a -> b = fun Eq x -> x module Fix (F : sig type 'a f end) = struct type 'a fix = ('a, 'a F.f) eq let uniq (type a) (type b) (Eq : a fix) (Eq : b fix) : (a, b) eq = Eq end module FixId = Fix (struct type 'a f = 'a end) let bad : (int, string) eq = FixId.uniq Eq Eq let _ = Printf.printf "Oh dear: %s" (cast bad 42)