What is the exact difference between Fix and Self on the Calculus of Constructions?

Question

The Self Types for Dependently Typed Lambda Encodings paper (by Peng Fu and Aaron Stump) proposes self types, which are, supposedly, sufficient to encode the induction principle and Scott-encoded datatypes on the Calculus of Constructions, without making the system inconsistent or introducing paradoxes.

The notation of that paper is too heavy for me to fully understand how to implement it.

What is, precisely, the main difference of Fix and Self? Or, in other words: in what points a naively implemented Fix should be restricted, so that it leaves no inconsistencies on the core calculus?

Answer 1

This is what I have understood after browsing the paper.

A Fix type satisfies the typing equivalence (assuming equirecursive types)

G |- M : Fix x. t   <=>     G |- M : t{Fix x. t / x}

i.e. you can unfold the type over itself. Note how the term M does not play any role here. If using isorecursive types, M would get some isomorphism applied (e.g. a Haskell's newtype constructor), but it is not that important.

Instead, Self types satisfy the following

G |- M : Self x. t   <=>     G |- M : t{M / x}

Now, x is not a type variable, but a term variable. The term gets "moved" inside the type. This is not a recursive type at all.