8
votes
Accepted
How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?
The $x$ in $\forall x . P(x)$ is not an argument. It is a bound variable indicating which variable the quantifer is ranging over.
Let us compare the situation to the definite integral, for concretness ...
- 30k
4
votes
Uncurrying and Polymorphism
The other answers are good, I just wanted to make it explicit that currying for dependent types is
$$
\textstyle
\prod (x : A) . \prod (y : B(x)) . C(x, y)
\ \cong \
\prod (p : \sum (x : A) . B(x)) . ...
- 30k
3
votes
Higher order rewriting theory and critical pairs with the beta rule
The theory of higher-order critical pairs can indeed handle this example, as outlined in the following article:
Higher-Order Rewrite Systems and their Confluence, Richard Mayr & Tobias Nipkow
...
- 8,114
2
votes
Accepted
How would you model Rust procedural macros?
I wouldn't consider it a higher-order function. A higher-order function takes a function as input, or yields a function as its output. In contrast, it sounds to me like your compiler extension is ...
D.W.♦
- 156k
2
votes
Uncurrying and Polymorphism
The uncurrying process will lead to existential types. Since the adjoint of $(X\to)$ is $(X\times\vphantom{Y})$ and the adjoint of $(\forall X.)$ is $(\exists X.)$, it is appearently inevitable. Also, ...
- 170
1
vote
Uncurrying and Polymorphism
I can only think of some uncurrying of 1 and 3.
$\forall X. (X \times int) \rightarrow X$
It looks like we can not uncurry this one, unless we transform it first into the isomorphic type 1.
$int \...
- 14.4k
Only top scored, non community-wiki answers of a minimum length are eligible