# Tagged Questions

**5**

votes

**2**answers

380 views

### Why is there no product type in simply typed lambda-calculus?

Consider simply typed $\lambda$-calculus that has only the unit type as primitive. We would like to encode the product and the sum types. An encoding of the product type in the untyped ...

**6**

votes

**4**answers

649 views

### What is the intuitive meaning of star and box in a pure type system?

The systems of the λ-cube have the axiom $\star:\square$.
I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meanings of $\star$ and ...

**6**

votes

**4**answers

670 views

### Can dependent sums be encoded as dependent products?

Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the ...

**12**

votes

**8**answers

2k views

### What is lambda calculus related to?

So I'm not much of a math guy but I've really enjoyed programming in Lisp and have become interested in the ideas of lambda calculus which it is based.
I was wondering if anyone had a suggestion ...