Why don't type synonyms permit recursion in Haskell?

Question

Can anyone explain why these both compile happily :

data A a b = A { a :: a, b :: b }
newtype B a = B (A a (B a))
newtype C = C (A Int C)

But I cannot create a similarly recursively defined types via type synonyms?

type B a = A a (B a)
type C = A Int C

Although obviously data B a = A { a :: a, b :: B a } works just fine.

Is there any way to avoid dealing with that extra constructor X everywhere I want the type recursive? I'm mostly passing in accessor functions that pick out the b anyways, so I'm mostly okay, but if an easy circumvention mechanism exists I'd like to know about it.

Any pragmas I should be using to improve performance with the specialized data type C? Just specialize stuff?

Any clever trick for copying between A a b and A c d defining only the a -> b and c -> d mapping without copying over the record twice? I'm afraid that A's fields will change in future. Template Haskell perhaps?

Answer 1

This has to do with Equi-recursive types versus iso-recursive types. Haskell implements recursive types using iso-recursive types, which require the programmer to tell the type-checker when type recursion is happening. The way you mark it is with a specific constructor, which a simple type-synonym doesn't allow you to have.

Equi-recursive types allow the compiler to infer where recursion is happening, but it leads to a much more complicated type-checker and in some seemingly simple cases the problem is undecidable.

If you'd like a good discussion of equi vs. iso recursive types, check out Benjamin Pierce's excellent Types and Programming Languages

Short answer: because type synonyms don't introduce constructors, and haskell needs constructors to explicitly mark recursion at the type-level, you can't use recursive type synonyms.

Answer 2

I will answer your first question and second questions.

The type of B is the infinite type (A a (A a (A a (A a (...)))))

The "type inference engine" could be designed to infer and handle infinite types. Unfortunately many errors (typographical or logical) by the programmer create code that fails to have the desired finite type and accidentally & unexpectedly has an infinite type. Right now the compiler rejects such code, which is nearly always what the programmer wants. Changing it to allow infinite types would create much more difficult to understand errors at compile time (at least as bad as C++ templates) and in rare cases you might make it compile and perform incorrectly at runtime.

Is there any way to avoid dealing with that extra constructor X everywhere I want the type recursive?

No. Haskell has chosen to allow recursive types only with explicit type constructors from data or newtype. These make the code more verbose but newtype should have little runtime penalty. It is a design decision.