Self types introduce two typing new rules (simplified):

$ \frac{\Gamma \; \vdash \; t : [t/x]T}{\Gamma \; \vdash \; t : \iota x. T}$ I-self and $ \frac{\Gamma \; \vdash \; t : \iota x. T}{\Gamma \; \vdash \; t : [t/x]T} $ E-self

The are related to Very dependent types, dependent intersection.

Their huge appeal is that they allow to prove induction for lambda encoded terms. They are implemented in Formality for that reason.

Is it possible to "hack" them into Agda (or Coq) so that one can play with them in a familiar environment? By "hack" I mean that it is fine to disable termination-checker, allow type-in-type, postulate stuff etc. (I'd be happy with source code modification too but that is likely beyond my skill set).

My first idea was to model the encoding after isorecursive types with $T$ as a higher order type and postulate constants 'Self', 'self' and 'unself':

$ \frac {\Gamma, T:\star \rightarrow \star \; \vdash \; t : (T t)} {\Gamma, T:\star \rightarrow \star \; \vdash \; \text{self}\, t : \text{Self} \, T}$ I-self and $ \frac {\Gamma, T:\star \rightarrow \star \; \vdash \; t : \text{Self} \, T} {\Gamma, T:\star \rightarrow \star \; \vdash \; \text{unself} \, t : T t} $ E-self

And intended evaluation rule ($\text{unself}\, (\text{self}\, t) \stackrel{\beta}{\rightarrow} t$).

Unfortunately this is not working in Agda for various reasons:

  Self : (T : Set -> Set) -> Set
  unself : (T : Set -> Set) -> (t : Self T) -> T t
  self : (T : Set -> Set) -> (t : T t) -> Self T

Perhaps the technique described in this mysterious issue in Agda can be of help.

Please advise.

  • 2
    $\begingroup$ I'm curious what do you think the type of T should be in the two rules I-self and E-self? It is certainly not Set -> Set, more something like T ? -> Set but then you can't fill the question mark. I have a feeling that this isn't going to be possible in an intrinsically typed language such as Agda or Coq, perhaps Cedille (github.com/cedille) will get you further. $\endgroup$
    – Jesper
    Commented May 4, 2020 at 7:38
  • 2
    $\begingroup$ Yes I would also be surprised if you can get this to work. It only works in a Curry-style system, because in the introduction rule you substitute the un-type-checked term in the type before you typecheck the term itself! $\endgroup$
    – Labbekak
    Commented May 4, 2020 at 16:55
  • $\begingroup$ You can see self types also as a "powerful" for pi types. Now on top of allowing the codomain to dependent on the argument, it can also depend on the function itself. So Pi A B, here B is not just A -> *, but Pi A B -> A -> *. $\endgroup$
    – Labbekak
    Commented May 7, 2020 at 17:41
  • $\begingroup$ So application: t1 t2 : B t1 t2 if t1 : Pi A B and t2 : A. Maybe that approach might help? $\endgroup$
    – Labbekak
    Commented May 7, 2020 at 18:09
  • $\begingroup$ Are you suggesting to use Agda's build in '->' dependent product or define a new type constructor Pi. The latter approach if pushed far enough might (?) work, but it will amount to formalizing a whole language as data in Agda. I'm interested in the former more but I can't seem to get it to work. $\endgroup$ Commented May 7, 2020 at 20:49


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.