<p>If we have System-F with higher-kinded types and newtypes, then we can express everything (I think) of System-F omega, except we have to manually (un)pack.
For example:</p>

<pre><code>newtype List t = List (forall r. r -&gt; (t -&gt; r -&gt; r) -&gt; r)

unList :: List t -&gt; (forall r. r -&gt; (t -&gt; r -&gt; r) -&gt; r)
unList (List f) = f
</code></pre>

<p>Is (I think) equivalent to System-F omega:</p>

<pre><code>List = \t. forall r. r -&gt; (t -&gt; r -&gt; r) -&gt; r
</code></pre>

<p>Except you have to call <code>List</code> and <code>unList</code> at the right moments.</p>

<p>Does this language with newtypes have more computation strength than System-F, equal to System-F omega?</p>

CC BY-SA 4.0
2019-10-01T20:57:58.077Z
Aside: the relationship between $F$ and $F_{\omega}$ is not well-understood. Pawel Urzyczyn conjectured that  $F_{\omega}$ is equivalent to typablility in $F_1$ (which is $F$ with first-order kinding).
Martin Berger
CC BY-SA 4.0
2019-10-03T14:57:55.933Z
@MartinBerger for typing individual terms: obviously there are functions which are well typed both in system $F_\omega$ and system $F$, but that can only be actually used in system $F_\omega$.
cody
CC BY-SA 4.0
2019-10-03T15:53:31.980Z
@cody I'm referring to Problem 12 in the [TLCA List of Open Problems](http://tlca.di.unito.it/opltlca/opltlca.pdf).
Martin Berger
CC BY-SA 4.0
2019-10-04T00:46:36.400Z
@MartinBerger I am familiar with the problem, but there is a subtle point here, which is that there are *functions* definable in $F_\omega$, which cannot be defined in $F$, if the function is to be taken $\mathbb{N}\rightarrow\mathbb{N}$.
cody
CC BY-SA 4.0
2019-10-04T09:01:47.270Z
@cody. By definable you mean semantically definable, not syntax? Aside, the conjecture is about $F_1$ vs $F_{\omega}$, that's what you meant?
Martin Berger
CC BY-SA 4.0
2019-10-04T13:12:40.803Z
@MartinBerger semantically definable, yes. And I did mean system $F$, but the argument generalizes to $F_1$.
cody
CC BY-SA 4.0
2019-10-04T19:12:14.793Z
@cody What blocks us from turning this semantic insight into a solution for #12 of TLCA's open problems?
Martin Berger
CC BY-SA 4.0
2019-10-04T19:53:22.707Z
@MartinBerger The fact that giving a type to an *individual term* is different than giving it a type *as a function from naturals to naturals*. E.g. *every normal form* can be typed in system F (curry style). Certainly, though, not every function from the untyped $\lambda$-calculus can be turned into a function in system F.
cody
<type-theory><lambda-calculus><type-systems><typed-lambda-calculus>
Is System-F with higher-kinded newtypes equivalent in computational power to System-F omega?
Labbekak
# Is System-F with higher-kinded newtypes equivalent in computational power to System-F omega?

(Asked by: username_0 on 2019-10-01)

If we have System-F with higher-kinded types and newtypes, then we can express everything (I think) of System-F omega, except we have to manually (un)pack.
For example:
newtype List t = List (forall r. r -> (t -> r -> r) -> r)

unList :: List t -> (forall r. r -> (t -> r -> r) -> r)
unList (List f) = f

Is (I think) equivalent to System-F omega:
List = \t. forall r. r -> (t -> r -> r) -> r

Except you have to call List and unList at the right moments.
Does this language with newtypes have more computation strength than System-F, equal to System-F omega?

**Tags:** type-theory, lambda-calculus, type-systems, typed-lambda-calculus
> **Comments:**
> **username_1**: Aside: the relationship between $F$ and $F_{\omega}$ is not well-understood. Pawel Urzyczyn conjectured that  $F_{\omega}$ is equivalent to typablility in $F_1$ (which is $F$ with first-order kinding).  
> **username_2**: @MartinBerger for typing individual terms: obviously there are functions which are well typed both in system $F_\omega$ and system $F$, but that can only be actually used in system $F_\omega$.  
> **username_1**: @cody I'm referring to Problem 12 in the [TLCA List of Open Problems](http://tlca.di.unito.it/opltlca/opltlca.pdf).  
> **username_2**: @MartinBerger I am familiar with the problem, but there is a subtle point here, which is that there are *functions* definable in $F_\omega$, which cannot be defined in $F$, if the function is to be taken $\mathbb{N}\rightarrow\mathbb{N}$.  
> **username_1**: @cody. By definable you mean semantically definable, not syntax? Aside, the conjecture is about $F_1$ vs $F_{\omega}$, that's what you meant?  
> **username_2**: @MartinBerger semantically definable, yes. And I did mean system $F$, but the argument generalizes to $F_1$.  
> **username_1**: @cody What blocks us from turning this semantic insight into a solution for #12 of TLCA's open problems?  
> **username_2**: @MartinBerger The fact that giving a type to an *individual term* is different than giving it a type *as a function from naturals to naturals*. E.g. *every normal form* can be typed in system F (curry style). Certainly, though, not every function from the untyped $\lambda$-calculus can be turned into a function in system F.  

---

## 0 answers

