Tag Info

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 ...
• 30.5k

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)) . ...
• 30.5k

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,233
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 ...
• 160k
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, ...
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 \...