6
$\begingroup$

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:

postulate 
  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.

$\endgroup$
  • 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 May 4 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 May 4 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 May 7 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 May 7 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$ – Łukasz Lew May 7 at 20:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.