What is the exact difference between Fix and Self on calculus constructs?

Question

Type Types for Dependent Typed Lambda Codes (Peng Fu and Aaron Pamp) offer self types that are supposedly sufficient to encode the induction principle and copied data types onto Construct Calculus without making the system inconsistent or introducing paradoxes.

The designation of this article is too heavy for me to fully understand how to implement it.

What is the main difference between Fix and Self? Or, in other words: at what points is it necessary to limit the naively implemented Fix so that it does not leave inconsistencies in the main calculus?

Answer 1

This is what I understood after watching the article.

A type

A Fixsatisfies typing equivalence (assuming equirecursive types)

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

i.e. you can expand the type above you. Please note that the term Mdoes not play any role here. If you use isorecursive types, you Mwill use some isomorphism (for example, the Haskell constructor newtype), but this is not so important.

Instead, Self types satisfy the following

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

Now xit is not a type variable, but a term variable. The term "moves" within a type. This is not a recursive type.