Recursive type generativity

• ? Derek argues against equi-recursive types,
  • instead rec(A, x.e) is just a forward declaration for checking $x:rec(A)⊢e:A$ , the canonical forms of rec(A) are just variables
  • “backpatching”
• qualifier ($\uparrow ,\downarrow$) meanings are yet to be understood
  • typing rules come with an effect result (deciding a set of variables who are marked as non-writable)
  • basically there for marking whether an abstract type variable in a recursive module body has been decided or not
  • potentially, we give another account with a different elaboration?
• The system formalize data type definitions as a separate syntax
  • also, this separate syntax is used in checking whether there is a cyclic transparent dependency
• an erasable operational semantics, with a type stores bookkeeping the recursive instantiation information
• [ ]