<p>Let me first state that I'm not sure what are you getting at, I'm not sure how linearity/affinity is relevant. I'll answer the question in 'standard' setting. </p>

<p>How would you define how to compare two infinite types lazily?</p>

<p>It seems to me that it can't be done automatically since they can eventually diverge. </p>

<p>[Checking for  nominal equality ("pointer quality", exactly same identifier) seems shortsighted since you could define two identical infinite structures <code>Nat</code> and <code>Nat2</code> and they would not be equal nominally while they should.]</p>

<p>But in some cases it can be done, its just that the programmer needs to lead the checker on how the equality should be verified.</p>

<p>In your case, think about <code>Nat</code> as a type-level fix point:</p>

<pre><code>natF = 
  ∀ nat : * 
  ∀ P : *
  ∀ S : nat -&gt; P
  ∀ Z : P
  P

Nat = fix nat . natF nat
</code></pre>

<p>That gives <code>Nat</code> and the two functions:</p>

<pre><code>fix : Nat -&gt; natF Nat
unfix : natF Nat -&gt; Nat
</code></pre>

<p>You can use these functions as annotations that control the infinity and allow the checker to work with finite structures all the time. </p>

<p>This article has a nice intro (there are plenty of similar tutorials):
<a href="https://www.schoolofhaskell.com/user/bartosz/understanding-algebras." rel="nofollow noreferrer">Gentle introduction to the general technique of F-algebras</a></p>

<p>For <code>Nat</code>, you would use this functor:</p>

<pre><code>data Nat nat = Z | S nat
</code></pre>

CC BY-SA 4.0
2018-09-27T13:40:35.507Z
Is there an explanation of how to apply fix/unfix to mutually recursive definitions?
MaiaVictor
CC BY-SA 4.0
2018-09-27T22:05:07.987Z
I don't know. That would be a good stackexchange question :)
Łukasz Lew
CC BY-SA 4.0
2018-09-17T02:57:58.230Z
2018-09-17T02:57:58.230Z
Łukasz Lew
<p>Suppose we take the church-style calculus of constructions, except with affine functions (variables must occur at most once) and mutual recursive definitions. For example:</p>

<pre><code>Nat =
  ∀ P : *
  ∀ S : Nat -&gt; P
  ∀ Z : P
  P

Zer =
  λ P : *
  λ S : Nat -&gt; P
  λ Z : Nat
  Z

Suc =
  λ x : Nat
  λ P : *
  λ S : Nat -&gt; P
  λ Z : Nat
  S x

two =
  Suc (Suc Zer)
</code></pre>

<p>If we built an eager type-checker and asked it to infer <code>Zer</code>, it'd not halt, as <code>Zer</code>'s type is infinite:</p>

<pre><code>two : ∀ (P : *) -&gt; ∀ S : (∀ (P : *) -&gt; ∀ S : (∀ (P : *) -&gt; ∀ S : ...
</code></pre>

<p>But if we do it lazily, then it'd output:</p>

<pre><code>Zer :
  ∀ P : *
  ∀ S : Nat -&gt; P
  ∀ Z : Nat
  Z
</code></pre>

<p>Which is the same as <code>Nat</code> and correct, since <code>Zer</code> is indeed a proof of <code>Nat</code>. One could wonder if it could accept "wrong" proofs such as <code>false : ∀ (P : *) -&gt; P</code>, for some construction of <code>false</code>. The obvious approach, though, seems not to work:</p>

<pre><code>false = (λ (x : ∀ (P : *) -&gt; P) -&gt; x) false
</code></pre>

<p>If we had top-level type-annotations (such as <code>false : ∀ (P : *) -&gt; P</code>), the checker would indeed accept this term. But, because of curry-style, the only way to infer the type of <code>false</code> is by inferring the type of <code>false</code>: it'll be stuck in an infinite loop and never output anything.</p>

<p>In other words, it seems that, for the subset of terms that this type-inferencer halts, it behaves as a consistent proof assistant. Of course, it works a bit differently from usual as it has infinite types and whatnot, but, intuitively, it seems to be a functional system for mathematical proofs, since it seems to be unable to accept <code>false</code> or other incorrect proofs. <strong>If one is able to prove that this type-checker could never accept <code>false</code>, would it indeed be well suited for mathematical proofs?</strong></p>

CC BY-SA 4.0
2018-09-15T09:27:50.220Z
The title of your question talks about linearity, but the body allows affine. Is that deliberate?
Martin Berger
CC BY-SA 4.0
2018-09-15T17:11:33.783Z
@MartinBerger no, that was a mistake.
MaiaVictor
CC BY-SA 4.0
2018-09-19T08:15:33.147Z
I am not totally sure what the intention of the recursive types you present is. To me, it seems that two styles are mixed, which makes things unnecessarily complex: There are the equi-recursive types, see Part IV of _Types and Programming Languages_ by Pierce, and the second-order encoding of inductive types, see the work by [Mendler](https://dx.doi.org/10.1016/0168-0072(91)90069-X) or [Herman Geuvers](http://www.cs.ru.nl/~herman/PUBS/ChurchScottDataTypes.pdf). It would be helpful if you could clarify how exactly your recursively types should behave. Also, what is the role of affinity here?
Henning Basold
CC BY-SA 4.0
2018-09-19T14:35:46.027Z
@HenningBasold there is just equi-recursive types, which are then used to define what you identify as second-order encoding of inductive types. (Or did I make some mistake?) The rule of affinity was just to make it less complex and avoid different ways to define `false` that I hadn't predicted...
MaiaVictor
CC BY-SA 4.0
2018-09-19T14:41:55.280Z
(You speak as if "affinity" is "extra stuff", but IMO that is reversed, affinity is the baseline and exponential functions would be the addition; you should be asking the role of contraction if I had it!)
MaiaVictor
CC BY-SA 4.0
2018-09-19T17:17:49.077Z
@MaiaVictor My confusion mainly arises by the fact that the second-order encoding in, say, System F does not need (equi-)recursive types because it is impredicative. But maybe your intention is to remove impredicativity? About affinity: Fair enough. I merely asked about this to understand where you think affinity is important in your example and question.
Henning Basold
<type-theory><lambda-calculus><constructive-mathematics>
Is the church-style affine calculus of constructions with unrestricted recursion consistent?
MaiaVictor
# Is the church-style affine calculus of constructions with unrestricted recursion consistent?

(Asked by: username_0 on 2018-09-15)

Suppose we take the church-style calculus of constructions, except with affine functions (variables must occur at most once) and mutual recursive definitions. For example:
Nat =
  ∀ P : *
  ∀ S : Nat -> P
  ∀ Z : P
  P

Zer =
  λ P : *
  λ S : Nat -> P
  λ Z : Nat
  Z

Suc =
  λ x : Nat
  λ P : *
  λ S : Nat -> P
  λ Z : Nat
  S x

two =
  Suc (Suc Zer)

If we built an eager type-checker and asked it to infer Zer, it'd not halt, as Zer's type is infinite:
two : ∀ (P : *) -> ∀ S : (∀ (P : *) -> ∀ S : (∀ (P : *) -> ∀ S : ...

But if we do it lazily, then it'd output:
Zer :
  ∀ P : *
  ∀ S : Nat -> P
  ∀ Z : Nat
  Z

Which is the same as Nat and correct, since Zer is indeed a proof of Nat. One could wonder if it could accept "wrong" proofs such as false : ∀ (P : *) -> P, for some construction of false. The obvious approach, though, seems not to work:
false = (λ (x : ∀ (P : *) -> P) -> x) false

If we had top-level type-annotations (such as false : ∀ (P : *) -> P), the checker would indeed accept this term. But, because of curry-style, the only way to infer the type of false is by inferring the type of false: it'll be stuck in an infinite loop and never output anything.
In other words, it seems that, for the subset of terms that this type-inferencer halts, it behaves as a consistent proof assistant. Of course, it works a bit differently from usual as it has infinite types and whatnot, but, intuitively, it seems to be a functional system for mathematical proofs, since it seems to be unable to accept false or other incorrect proofs. If one is able to prove that this type-checker could never accept false, would it indeed be well suited for mathematical proofs?

**Tags:** type-theory, lambda-calculus, constructive-mathematics

> **Comments:**
> **username_1**: The title of your question talks about linearity, but the body allows affine. Is that deliberate?  
> **username_0**: @MartinBerger no, that was a mistake.  
> **username_2**: I am not totally sure what the intention of the recursive types you present is. To me, it seems that two styles are mixed, which makes things unnecessarily complex: There are the equi-recursive types, see Part IV of _Types and Programming Languages_ by Pierce, and the second-order encoding of inductive types, see the work by [Mendler](https://dx.doi.org/10.1016/0168-0072(91)90069-X) or [Herman Geuvers](http://www.cs.ru.nl/~herman/PUBS/ChurchScottDataTypes.pdf). It would be helpful if you could clarify how exactly your recursively types should behave. Also, what is the role of affinity here?  
> **username_0**: @HenningBasold there is just equi-recursive types, which are then used to define what you identify as second-order encoding of inductive types. (Or did I make some mistake?) The rule of affinity was just to make it less complex and avoid different ways to define `false` that I hadn't predicted...  
> **username_0**: (You speak as if "affinity" is "extra stuff", but IMO that is reversed, affinity is the baseline and exponential functions would be the addition; you should be asking the role of contraction if I had it!)  
> **username_2**: @username_0 My confusion mainly arises by the fact that the second-order encoding in, say, System F does not need (equi-)recursive types because it is impredicative. But maybe your intention is to remove impredicativity? About affinity: Fair enough. I merely asked about this to understand where you think affinity is important in your example and question.  

---

## 1 answers

### Answer by username_3 on 2018-09-17. Score: 2 | Accepted answer

Let me first state that I'm not sure what are you getting at, I'm not sure how linearity/affinity is relevant. I'll answer the question in 'standard' setting. 
How would you define how to compare two infinite types lazily?
It seems to me that it can't be done automatically since they can eventually diverge. 
[Checking for  nominal equality ("pointer quality", exactly same identifier) seems shortsighted since you could define two identical infinite structures Nat and Nat2 and they would not be equal nominally while they should.]
But in some cases it can be done, its just that the programmer needs to lead the checker on how the equality should be verified.
In your case, think about Nat as a type-level fix point:
natF = 
  ∀ nat : * 
  ∀ P : *
  ∀ S : nat -> P
  ∀ Z : P
  P

Nat = fix nat . natF nat

That gives Nat and the two functions:
fix : Nat -> natF Nat
unfix : natF Nat -> Nat

You can use these functions as annotations that control the infinity and allow the checker to work with finite structures all the time. 
This article has a nice intro (there are plenty of similar tutorials):
Gentle introduction to the general technique of F-algebras
For Nat, you would use this functor:
data Nat nat = Z | S nat

> **Comments:**
> **username_0**: Is there an explanation of how to apply fix/unfix to mutually recursive definitions?  
> **username_3**: I don't know. That would be a good stackexchange question :)  

---

