<p>Consider a type theory such as the one developed in Chapter 1 of the <a href="https://homotopytypetheory.org/book/" rel="nofollow noreferrer">HoTT book</a>, or similar. In fact, I am currently only interested in the types that can be constructed from a collection of elementary &quot;initial types&quot; <span class="math-container">$A_0,A_1,\ldots$</span> as well as <span class="math-container">$+\times\rightarrow$</span>.</p>
<p>Usually, one is allowed to define function types which take function types themselves, e.g. a type of the form <span class="math-container">$W=(P\rightarrow Q)\rightarrow R$</span>. In programmer-speak, a representative <span class="math-container">$w:W$</span> takes a &quot;callback function&quot; as input.</p>
<p>My question is: Suppose we are given a type-theoretic construction of <span class="math-container">$f:X\rightarrow Y$</span>, with <span class="math-container">$X$</span> and <span class="math-container">$Y$</span> formed using only <span class="math-container">$A_1,A_2,\ldots,+,\times$</span>. Can we transform this construction - with polynomial proof complexity overhead - into one <s>that never constructs intermediate types with closures or callback functions</s> in which, whenever a type of the form <span class="math-container">$X\rightarrow Y$</span> appears in the construction, <span class="math-container">$X$</span> is constructed using only <span class="math-container">$A_1,A_2,\ldots,+,\times$</span>, i.e. <span class="math-container">$X\rightarrow Y$</span> is &quot;callback-function-free&quot;?</p>
<p>I'm also interested in related statements.</p>

CC BY-SA 4.0
2022-04-17T15:20:54.547Z
What does it mean for a function to "ever constructs intermediate types"? In what sense do functions "construct types"?
Andrej Bauer
CC BY-SA 4.0
2022-04-17T17:49:50.080Z
@AndrejBauer Sorry, that what imprecise, I meant "involves constructing a function that is an inhabitant of a type that involves callback functions". I updated the question text.
Duyal Yolcu
CC BY-SA 4.0
2022-04-17T19:37:11.947Z
Type theory is not going to help with proof complexity.
Andrej Bauer
CC BY-SA 4.0
2022-04-17T20:45:17.257Z
@AndrejBauer My rough intuition: If a type-theoretic proof constructs $f:X\rightarrow Y$, it implicitly constructs an inhabitant of $Y$ for any inhabitant of $X$. If $X$ is built using $A_1,\ldots,+,\times$, there can be exponentially many different inhabitants of $X$. In each case, the combinations of elementary types must be put together to create an inhabitant of $Y$. If one shows that it is not possible to construct inhabitants for exponentially many different inputs in the same proof steps in parallel, one has shown a lower bound. Can you elaborate on why you think type theory won't help?
Duyal Yolcu
CC BY-SA 4.0
2022-04-18T06:38:56.780Z
Because whatever analysis you perform using type theory, you could have performed it directly on proofs of a natural deduction system, by the Curry-Howard isomorphism. And people would have done it, if it were possible. Don't get me wrong, if you proved a new result in proof complexity using type theory that would be absolutely amazing. (Also, your ideas at the moment are still quite vague, you say things like "in parallel" which are undefined, etc.)
Andrej Bauer
CC BY-SA 4.0
2022-04-18T08:28:25.987Z
I think there are concepts that are more natural for computer programs than for ND proofs, even if the CH correspondence says they are just different ways of looking at the same set of symbols. Take execution traces: With the execution trace of a computer calculating/simplifying $f(x):Y$ using the proof-as-program, one can pinpoint exactly where and when in the code the different building blocks of $f(x):Y$ are put together for a given $x$. This yields a formal notion of "in parallel", although I am not sure if what I hope is true for this exact definition.
Duyal Yolcu
CC BY-SA 4.0
2022-04-18T08:55:53.183Z
I didn't say it was impossible. You're more than welcome to discover something new using ideas I don't believe in :-)
Andrej Bauer
CC BY-SA 4.0
2022-04-18T11:27:36.913Z
@AndrejBauer this leaves the original question :) Which, it seems to me, can be considered without hoping for lower bounds. In what context, do you think, would I be most likely to find this sort of theorem?
Duyal Yolcu
CC BY-SA 4.0
2022-04-18T12:10:27.290Z
Consider the normal form of $f$.
Andrej Bauer
CC BY-SA 4.0
2022-04-18T12:29:57.220Z
You mean, a simple case distinction (that generally takes an exponential number of steps)? If yes: Do you think anyone might be interested in an efficient algorithm, e.g. automated theorem proving people?
Duyal Yolcu
CC BY-SA 4.0
2022-08-13T03:05:35.687Z
Is [Defunctionalization](https://en.wikipedia.org/wiki/Defunctionalization) the sort of thing you are looking for?
Potato44
<type-theory>
Type theory: Eliminating callback functions?
Duyal Yolcu
# Type theory: Eliminating callback functions?

(Asked by: username_0 on 2022-04-17)

Consider a type theory such as the one developed in Chapter 1 of the [HoTT book](https://homotopytypetheory.org/book/), or similar. In fact, I am currently only interested in the types that can be constructed from a collection of elementary "initial types" $A\_0,A\_1,\ldots$ as well as $+\times\rightarrow$.

Usually, one is allowed to define function types which take function types themselves, e.g. a type of the form $W=(P\rightarrow Q)\rightarrow R$. In programmer-speak, a representative $w:W$ takes a "callback function" as input.

My question is: Suppose we are given a type-theoretic construction of $f:X\rightarrow Y$, with $X$ and $Y$ formed using only $A\_1,A\_2,\ldots,+,\times$. Can we transform this construction - with polynomial proof complexity overhead - into one ~~that never constructs intermediate types with closures or callback functions~~ in which, whenever a type of the form $X\rightarrow Y$ appears in the construction, $X$ is constructed using only $A\_1,A\_2,\ldots,+,\times$, i.e. $X\rightarrow Y$ is "callback-function-free"?

I'm also interested in related statements.

**Tags:** type-theory
> **Comments:**
> **username_1**: What does it mean for a function to "ever constructs intermediate types"? In what sense do functions "construct types"?  
> **username_0**: @AndrejBauer Sorry, that what imprecise, I meant "involves constructing a function that is an inhabitant of a type that involves callback functions". I updated the question text.  
> **username_1**: Type theory is not going to help with proof complexity.  
> **username_0**: @AndrejBauer My rough intuition: If a type-theoretic proof constructs $f:X\rightarrow Y$, it implicitly constructs an inhabitant of $Y$ for any inhabitant of $X$. If $X$ is built using $A_1,\ldots,+,\times$, there can be exponentially many different inhabitants of $X$. In each case, the combinations of elementary types must be put together to create an inhabitant of $Y$. If one shows that it is not possible to construct inhabitants for exponentially many different inputs in the same proof steps in parallel, one has shown a lower bound. Can you elaborate on why you think type theory won't help?  
> **username_1**: Because whatever analysis you perform using type theory, you could have performed it directly on proofs of a natural deduction system, by the Curry-Howard isomorphism. And people would have done it, if it were possible. Don't get me wrong, if you proved a new result in proof complexity using type theory that would be absolutely amazing. (Also, your ideas at the moment are still quite vague, you say things like "in parallel" which are undefined, etc.)  
> **username_0**: I think there are concepts that are more natural for computer programs than for ND proofs, even if the CH correspondence says they are just different ways of looking at the same set of symbols. Take execution traces: With the execution trace of a computer calculating/simplifying $f(x):Y$ using the proof-as-program, one can pinpoint exactly where and when in the code the different building blocks of $f(x):Y$ are put together for a given $x$. This yields a formal notion of "in parallel", although I am not sure if what I hope is true for this exact definition.  
> **username_1**: I didn't say it was impossible. You're more than welcome to discover something new using ideas I don't believe in :-)  
> **username_0**: @AndrejBauer this leaves the original question :) Which, it seems to me, can be considered without hoping for lower bounds. In what context, do you think, would I be most likely to find this sort of theorem?  
> **username_1**: Consider the normal form of $f$.  
> **username_0**: You mean, a simple case distinction (that generally takes an exponential number of steps)? If yes: Do you think anyone might be interested in an efficient algorithm, e.g. automated theorem proving people?  
> **username_2**: Is [Defunctionalization](https://en.wikipedia.org/wiki/Defunctionalization) the sort of thing you are looking for?  

---

## 0 answers

