Questions tagged [type-theory]

formal systems to specify properties of objects

Filter by
Sorted by
Tagged with
12
votes
1answer
2k views

Concise example of exponential cost of ML type inference

It was brought to my attention that the cost of type inference in a functional language like OCaml can be very high. The claim is that there is a sequence of expressions such that for each expression ...
1
vote
3answers
404 views

Why classes implicitly derive from only the Object Class?

I do not have any argument opposing why we need only a single universal class. However why not we have two universal classes, say an Object and an AntiObject Class. In nature and in science we find ...
11
votes
1answer
605 views

Inferring refinement types

At work I’ve been tasked with inferring some type information about a dynamic language. I rewrite sequences of statements into nested let expressions, like so: <...
32
votes
1answer
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?
5
votes
2answers
787 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 ...
15
votes
1answer
682 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 ...
23
votes
3answers
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 ...
20
votes
3answers
3k 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 ...
8
votes
3answers
428 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 ...
26
votes
1answer
1k 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 ...
11
votes
1answer
497 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 ...
22
votes
2answers
3k 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$...
21
votes
2answers
2k views

Recursive definitions over an inductive type with nested components

Consider an inductive type which has some recursive occurrences in a nested, but strictly positive location. For example, trees with finite branching with nodes using a generic list data structure to ...
29
votes
2answers
669 views

Characterization of lambda-terms that have union types

Many textbooks cover intersection types in the lambda-calculus. The typing rules for intersection can be defined as follows (on top of the simply typed lambda-calculus with subtyping): $$ \dfrac{\...
20
votes
2answers
772 views

Are universal types a sub-type, or special case, of existential types?

I would like to know whether a universally-quantified type $T_a$: $$T_a = \forall X: \left\{ a\in X,f:X→\{T, F\} \right\}$$ is a sub-type, or special case, of an existentially-quantified type $T_e$ ...

1
6 7 8 9
10