Underdetermined recursion


Most type systems permit some flavour of recursive types, allowing the programmer to define, say, the type ListInt\n{ListInt} representing lists of integers. A ListInt\n{ListInt} consists of either the empty list, or a pair of an integer and a ListInt\n{ListInt}, giving the recursive equation: ListInt1+Int×ListInt \n{ListInt} \cong 1 + \n{Int} × \n{ListInt} There are two ways to interpret the symbol \cong above:

  • Isorecursive types: there is an explicitly defined datatype/class ListInt\n{ListInt}, and we must use its constructors/methods to convert between ListInt\n{ListInt} and 1+Int×ListInt1 + \n{Int} × \n{ListInt}. The symbol \cong is read as "is isomorphic to".

  • Equirecursive types: the types ListInt\n{ListInt} and 1+Int×ListInt1 + \n{Int} × \n{ListInt} are the same type, because ListInt\n{ListInt} is identified with the infinite expansion: 1+Int×(1+Int×(1+(Int×))) 1 + \n{Int} × (1 + \n{Int} × (1 + (\n{Int} × \dots))) The symbol \cong is read as "equals".

With equirecursive types, there can only be a single solution to a recursive equation. If I have another type AA satisfying A=1+Int×AA = 1 + \n{Int} × A, then the infinite expansions of ListInt\n{ListInt} and AA are equal, so A=ListIntA = \n{ListInt}. 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 FF and two types A,BA, B satisfying: A=F[A]B=F[B] \begin{aligned}A &= F[A] \ B &= F[B] \end{aligned} then type systems equirecursive types will assume that A=BA = B, since they have the same infinite expansion F[F[F[]]]F[F[F[\dots]]].

This is unsound for arbitrary type-level functions FF because there can be multiple solutions for X=F[X]X = F[X]. For instance: F[X]=XA=IntB=String \begin{aligned} F[X] &= X \ A &= \n{Int} \ B &= \n{String} \end{aligned}

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 =

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)