Questions tagged [type-theory]
formal systems to specify properties of objects
477
questions
12
votes
3answers
1k views
Relation between Russellian type theory and type systems
I recently realized that there is some sort of relation between Russellian type theory and type systems, as found e.g. in Haskell. Actually, some of the notation for types in Haskell seems to have ...
5
votes
1answer
652 views
lambda calculus as a type theory
From the Introduction section of Homotopy Type Theory book:
Type theory was originally invented by Bertrand Russell ... It was later developed as a rigorous formal system in its own right(under tha ...
11
votes
2answers
1k views
Universes in dependent type theory
I am reading about dependent types theory in the Homotopy Type Theory online book.
In section 1.3 of the Type Theory chapter, it introduces the notion of hierarchy of Universes: $\mathcal{U}_0 : \...
8
votes
2answers
457 views
To what does typing correspond in a Turing Machine?
I hope my question makes sense: Starting with the premise that the untyped $\lambda $ calculus is equivalent in power to a Turing machine, to what in a Turing machine does adding types to the $\lambda ...
9
votes
1answer
727 views
Example of a false proposition when assuming Type : Type
In Type Theory if one allows Type to be a member of itself, it makes the theory inconsistent. I understand it by analogy to Russel's paradox in Set Theory, but would prefer to see it done in Type ...
6
votes
2answers
349 views
What kinds of programming pitfalls modern languages are able to find?
I often see claims that modern functional strictly-typed languages are 'safer' than others. These statement mostly linked with type systems and their ability to explicitly express the following ...
45
votes
1answer
6k views
What makes type inference for dependent types undecidable?
I have seen it mentioned that dependent type systems are not inferable, but are checkable. I was wondering if there is a simple explanation of why that is so, and whether or not there is there a limit ...
0
votes
1answer
238 views
Is constant a variable or subtype?
I think of type as a range of values that the variable can take whereas the rest is known constant or does not matter. Variables (instances or objects), which share common properties, are considered ...
6
votes
1answer
553 views
Encoding row types
I'm working on a type system with extensible records, similar to ones explained in "A Polymorphic Type System for Extensible Records and Variants - Benedict R. Gaster and Mark P. Jones" and "...
5
votes
1answer
2k views
What is the difference between the semantic and syntactic views of function types?
Edit: My original question referred to nonconstructive and constructive definitions of function types. I changed the terminology in the question and the title to semantic and syntactic, which the ...
31
votes
2answers
3k views
How are programming languages and foundations of mathematics related?
Basically I am aware of three foundations for math
Set theory
Type theory
Category theory
So in what ways are programming languages and foundations of mathematics related?
EDIT
The original ...
4
votes
3answers
958 views
How can SML infer types like this?
Wikipedia says:
fun factorial n =
if n = 0 then 1 else n * factorial (n-1)
A Standard ML compiler is required to infer the static type int -> int of this ...
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
408 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
611 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
805 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
690 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 ...
21
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
431 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
499 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$...
22
votes
2answers
3k 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'
40.3k7 gold badges108 silver badges171 bronze badges
29
votes
2answers
682 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'
40.3k7 gold badges108 silver badges171 bronze badges
20
votes
2answers
801 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$ ...
