8 votes

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 ...
Andrej Bauer's user avatar
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)) . ...
Andrej Bauer's user avatar
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 ...
cody's user avatar
  • 8,114
2 votes

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.'s user avatar
  • 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, ...
Trebor's user avatar
  • 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 \...
chi's user avatar
  • 14.4k

Only top scored, non community-wiki answers of a minimum length are eligible