Questions tagged [type-theory]
formal systems to specify properties of objects
465
questions
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 ...
asked Mar 7 '12 at 17:38
Gilles 'SO- stop being evil'
39.9k7 gold badges106 silver badges171 bronze badges
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{\...
asked Mar 7 '12 at 2:07
Gilles 'SO- stop being evil'
39.9k7 gold badges106 silver badges171 bronze badges
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$ ...
