The 2024 Developer Survey results are live! See the results

# Questions tagged [typed-lambda-calculus]

The tag has no usage guidance.

83 questions
Filter by
Sorted by
Tagged with
129 views

### How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

Following Wadler's paper "Recursive types for free" and having spent some months on reconstructing the proof that $\exists A. ~ A \times (A\to F~ A)$ is the terminal $F$-coalgebra, I am ...
• 552
89 views

### Is the encoding of existential types in System F adequate?

This is somewhat related to How to encode a function from an existential type Existential types can be encoded in System F. If $P$ is any type constructor, not necessarily covariant, then the ...
• 552
46 views

### Relationship between differential lambda calculus and automatic differentiation

I'm familiar with both, especially the dual numbers form of automatic differentiation. I'm wondering if someone could clarify the relationship between the two -- as I understand it, they coincide on ...
• 41
141 views

### What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?

In what books or papers is it explained how the type constructions of a functional programming language correspond to category theory, and what are the models (a rigorous semantics) of programs of ...
• 552
1 vote
101 views

### Formalising Church numerals in Agda

Beginer here. I'm trying to show that the closed $\beta$-nf's of type $(\iota \to \iota) \to (\iota \to \iota)$ are the Church numerals ($\iota$ the base type, using the simply-typed lambda calculus)...
• 13
240 views

### How to encode a function from an existential type

I am having trouble using parametricity to show that existential types work in System F (or System Fω) in the way one would expect them to work. It is known that an existential type $\exists t.~P~t$ (...
• 552
205 views

• 11
1 vote
112 views

### Extension of primitive recursion, that is as powerful as System-T

I know that System-T restricted to first-order types is exactly as powerful as primitive recursive functions, because I proved it in Agda. I asked myself, if there is a extension of primitive ...
183 views

### Can we use relational parametricity to simplify the type $\forall a.\,((a\to r)\to a)\to a$ and similar types?

This question is similar to Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$? but looks more complicated. It is about using relational ...
• 552
152 views

• 101
1 vote
210 views

### Explicit type system with infinite non-cumulative universe hierarchy

Is there an open-source proof assistant or at least an explicit set of rules written down somewhere for a type system with an infinite non-cumulative universe hierarchy and unique typing? I want to ...
159 views

### $\mathbb{N}$ in intensional MLTT with judgmentally commutative $+$ and $\times$

Is there a way to implement natural numbers in intensional Martin-Löf type theory so that addition and multiplication is judgmentally commutative?
246 views

### Model of MLTT with $\eta$ rule where function extensionality fails

Consider intensional Martin-Löf type theory with judgmental $\eta$ rule for dependent product types. Is there a model of it where function extensionality fails?
91 views

### Normal term of double negation of W-type

Consider the intensional Martin-Löf type theory without axiom of choice or the law of excluded middle. Let $A:U_0$ be a type and $B:A\to U_0$ be a function such that $\Sigma_{a:A}(B(a)\to 0)$is ...
113 views

### Typing inference as a map on abstract syntax trees

Is there a reference that explains typing inference for Martin-Löf type theory as a computable map from abstract syntax trees of terms to abstract syntax trees of types? I don't want to identify non-...
236 views

### Is the Mendler-encoding in System-F adequate?

In the paper "Efficiency of Lambda-Encodings in Total Type Theory" it is mentioned that the Church-encoding is adequate and the Parigot encoding is not adequate. This means that any ...
• 701
556 views

### Complexity of type inference in the simply typed lambda calculus

A similar question was answered here: Is simply typed lambda calculus equivalent to primitive recursive functions What I conclude from the answers is that the complexity is that of the extended ...
• 531
252 views

### Category theory lambda cube?

If simply typed lambda calculus corresponds to cartesian closed categories, what types of categories do other calculi in the lambda cube correspond to? https://en.m.wikipedia.org/wiki/Lambda_cube
• 163
644 views

### Is there an efficient beta-equivalence algorithm?

Is there an efficient algorithm to determine if two terms are beta-equivalent? Specifically, I am curious about simply-typed-lambda-calculus, so you can assume both terms are strongly normalizing. I ...
• 101
132 views

• 219
267 views

### Decidability of rank-k polymorphism vs. System F

There's a paper by Kfoury from 1992, "Type Reconstruction in Finite Rank Fragments of the Second-Order $\lambda$-Calculus", that proves that type inference for Curry-style rank-$k$ polymorphic lambda ...
• 335
217 views

### Type of induction principle for fixpoint types

To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F is a ...
• 701
186 views

### Type System Of $\lambda\mu$-Calculus

reading this paper on CPS-tranformation from the $\lambda\mu$-calculus, I'm a bit confused about the type system presented: Why second-order formulas in the types? Is this according to the Curry-...
• 139
272 views

### What's the point of stack judgement in CBPV?

Call-by-push-value (CBPV) introduces two main families of types, values and computations, and their corresponding judgements. However, in some extensions/variants/adaptation of CBPV, there is a third ...
• 53
443 views

### Is System-F with higher-kinded newtypes equivalent in computational power to System-F omega?

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: ...
• 701