# Questions tagged [type-theory]

formal systems to specify properties of objects

312 questions
2k views

### Does there exist a Turing complete typed lambda calculus?

Do there exist any Turing complete typed lambda calculi? If so, what are a few examples?
608 views

### What is the type theory judgement symbol?

In type theory judgements are often presented with the following syntax: My question is what is that symbol in the middle called? All the papers I've found seem to use an image rather than a unicode ...
550 views

### Type inference with product types

I’m working on a compiler for a concatenative language and would like to add type inference support. I understand Hindley–Milner, but I’ve been learning the type theory as I go, so I’m unsure of how ...
1k views

### Categorisation of type systems (strong/weak, dynamic/static)

In short: how are type systems categorised in academic contexts; particularly, where can I find reputable sources that make the distinctions between different sorts of type system clear? In a sense ...
2k views

### How to read typing rules?

I started reading more and more language research papers. I find it very interesting and a good way to learn more about programming in general. However, there usually comes a section where I always ...
374 views

### Simple explanation as to why certain computable functions cannot be represented by a typed term?

Reading the paper An Introduction to the Lambda Calculus, I came across a paragraph I didn't really understand, on page 34 (my italics): Within each of the two paradigms there are several versions ...
936 views

### Is there a typed SKI calculus?

Most of us know the correspondence between combinatory logic and lambda calculus. But I've never seen (maybe I haven't looked deep enough) the equivalent of "typed combinators", corresponding to the ...
400 views

### Constraint-based Type Inference with Algebraic Data

I am working on an expression based language of ML genealogy, so it naturally needs type inference >:) Now, I am trying to extend a constraint-based solution to the problem of inferring types, based ...
2k views

### What is beta equivalence?

In the script I am currently reading on the lambda calculus, beta equivalence is defined as this: The $\beta$-equivalence $\equiv_\beta$ is the smallest equivalence that contains $\rightarrow_\beta$...