<p><a href="https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf" rel="noreferrer">Self types</a> introduce two typing new rules (simplified):</p>

<p><span class="math-container">$
\frac{\Gamma \; \vdash \; t : [t/x]T}{\Gamma \; \vdash \; t : \iota x. T}$</span> I-self and 
<span class="math-container">$
\frac{\Gamma \; \vdash \; t : \iota x. T}{\Gamma \; \vdash \; t : [t/x]T}
$</span> E-self</p>

<p>The are related to <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.39.4169&amp;rep=rep1&amp;type=pdf" rel="noreferrer">Very dependent types</a>, <a href="https://ecommons.cornell.edu/bitstream/handle/1813/5799/2000-1809.pdf?sequence=1" rel="noreferrer">dependent intersection</a>.</p>

<p>Their huge appeal is that they allow to prove induction for lambda encoded terms. They are implemented in <a href="https://github.com/agda/agda/issues/1556" rel="noreferrer">Formality</a> for that reason. </p>

<p>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).</p>

<p>My first idea was to model the encoding after isorecursive types with <span class="math-container">$T$</span> as a higher order type and postulate constants 'Self', 'self' and 'unself':</p>

<p><span class="math-container">$
\frac
{\Gamma, T:\star \rightarrow \star \; \vdash \; t : (T t)}
{\Gamma, T:\star \rightarrow \star \; \vdash \; \text{self}\, t : \text{Self} \, T}$</span> I-self and 
<span class="math-container">$
\frac
{\Gamma, T:\star \rightarrow \star \; \vdash \; t : \text{Self} \, T}
{\Gamma, T:\star \rightarrow \star \; \vdash \; \text{unself} \, t : T t}
$</span> E-self</p>

<p>And intended evaluation rule (<span class="math-container">$\text{unself}\, (\text{self}\, t) \stackrel{\beta}{\rightarrow} t$</span>).</p>

<p>Unfortunately this is not working in Agda for various reasons:</p>

<pre><code>postulate 
  Self : (T : Set -&gt; Set) -&gt; Set
  unself : (T : Set -&gt; Set) -&gt; (t : Self T) -&gt; T t
  self : (T : Set -&gt; Set) -&gt; (t : T t) -&gt; Self T
</code></pre>

<p>Perhaps the technique described in <a href="https://github.com/agda/agda/issues/1556" rel="noreferrer">this mysterious issue in Agda</a> can be of help.</p>

<p>Please advise.</p>

CC BY-SA 4.0
2020-05-04T07:38:37.833Z
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 (https://github.com/cedille) will get you further.
Jesper
CC BY-SA 4.0
2020-05-04T16:55:52.403Z
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!
Labbekak
CC BY-SA 4.0
2020-05-07T17:41:08.037Z
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 -> *.
Labbekak
CC BY-SA 4.0
2020-05-07T18:09:29.213Z
So application: t1 t2 : B t1 t2 if t1 : Pi A B and t2 : A. Maybe that approach might help?
Labbekak
CC BY-SA 4.0
2020-05-07T20:49:51.603Z
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.
Łukasz Lew
CC BY-SA 4.0
2020-05-08T08:55:08.867Z
Honestly it was just a thought, I don't know how to apply the idea to Agda. But I know in the newest implementation of Formality, instead of self types being a new construct, they combine self-types and Pi in one construct. I'm trying to write an elaborator for a language with self types at the moment, but because you have to add untyped terms to the context before you typecheck the self-type introduction, it's tricky.
Labbekak
CC BY-SA 4.0
2020-05-09T01:53:27.033Z
I did not realize that you have to have untyped terms in the contex.. Can you show an example derivation?
Łukasz Lew
CC BY-SA 4.0
2020-05-10T14:23:01.193Z
Actually I misspoke I meant the substitution of the term you are typechecking in to the type in the introduction rule. So before you have typechecked the term you already substitute it in the type.
Labbekak
<type-theory><dependent-type><agda><inductive-type>
Postulating self types in a proof assistant
Łukasz Lew
# Postulating self types in a proof assistant

(Asked by: username_0 on 2020-05-03)

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.

**Tags:** type-theory, dependent-type, agda, inductive-type

> **Comments:**
> **username_1**: 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 (https://github.com/cedille) will get you further.  
> **username_2**: 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!  
> **username_2**: 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 -> *.  
> **username_2**: So application: t1 t2 : B t1 t2 if t1 : Pi A B and t2 : A. Maybe that approach might help?  
> **username_0**: 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.  
> **username_2**: Honestly it was just a thought, I don't know how to apply the idea to Agda. But I know in the newest implementation of Formality, instead of self types being a new construct, they combine self-types and Pi in one construct. I'm trying to write an elaborator for a language with self types at the moment, but because you have to add untyped terms to the context before you typecheck the self-type introduction, it's tricky.  
> **username_0**: I did not realize that you have to have untyped terms in the contex.. Can you show an example derivation?  
> **username_2**: Actually I misspoke I meant the substitution of the term you are typechecking in to the type in the introduction rule. So before you have typechecked the term you already substitute it in the type.  

---

## 0 answers

