Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [type-theory]

formal systems to specify properties of objects

9
votes
1answer
557 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 ...
28
votes
2answers
2k 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 ...
28
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?
37
votes
1answer
4k 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 ...
15
votes
2answers
744 views

Does the Y combinator contradict the Curry-Howard correspondence?

The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Curry-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true ...
28
votes
2answers
527 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{\...
14
votes
1answer
1k views

Why will the Hindley-Milner algorithm never yield a type like t1 -> t2?

I'm reading about the Hindley-Milner typing algorithm while writing an implementation, and see that, as long as every variable is bound, you'll always get either atomic types or types where the ...
4
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 ...
6
votes
2answers
669 views

What is the connection between data structures and data types?

I have read some books and wikipedia, which seem to give not completely consistent definitions and notations. I try to understand the concepts, regardless of what they are called. Here are what I have ...
5
votes
1answer
76 views

In type systems, is there a name for SQL's way of cutting and combining record types into new types?

I'd like to have this feature in my application programming language (which these days, is Scala), but when I went to learn more about it on the internets, I realized I don't know the name of it. I'm ...
48
votes
3answers
7k views

Dependent types vs refinement types

Could somebody explain the difference between dependent types and refinement types? As I understand it, a refinement type contains all values of a type fulfilling a predicate. Is there a feature of ...
28
votes
4answers
2k views

What exactly is the semantic difference between set and type?

EDIT: I've now asked a similar question about the difference between categories and sets. Every time I read about type theory (which admittedly is rather informal), I can't really understand how it ...
32
votes
2answers
5k views

What can Idris not do by giving up Turing completeness?

I know that Idris has dependent types but isn't turing complete. What can it not do by giving up Turing completeness, and is this related to having dependent types? I guess this is quite a specific ...
17
votes
2answers
381 views

“Minimal” intuitionistic type theory?

I'm surprised that people keep adding new types in type theories but no one seems to mention a minimal theory (or I can't find it). I thought mathaticians love minimal stuff, don't they? If I ...
17
votes
3answers
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 ...
12
votes
1answer
610 views

Why aren't we researching more towards compile time guarantees?

I love all that is compile time and I love the idea that once you compile a program a lot of guarantees are made about it's execution. Generally speaking a static type system (Haskell, C++, ...) seems ...
10
votes
1answer
220 views

Why are recursive types needed as primitives for proofs in dependent type systems?

I'm relatively new to type theory and dependent programming. I've been studying the calculus of constructions (CoC) and other pure type systems. I'm particularly interested in using it as a proof-...
6
votes
2answers
169 views

Is there a relationship between “sound and complete” in logic and “type safety” in PLs?

I've been wondering if there's a connection between "good logics" and "good programming languages". It seems that logics are shown to be "locally sound and complete" whereas programming languages are ...
4
votes
1answer
152 views

What are some examples of types that can't be derived set theoretically?

I'm hoping for examples that aren't too abstract or useless in day-to-day programming, though not with a lot of hope, since in Bartosz Milewski's book, it is stated that generally speaking, the ...
20
votes
2answers
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$...
2
votes
2answers
497 views

Is Wadler's 'Theorems for Free' as general as Design By Contract for establishing correctness?

Philip Wadler has written a brilliant paper called 'Theorems for Free'. The big idea is that you can use types to reason about your program, and even prove simple theorems about your program. We see ...
20
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 ...
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 ...
10
votes
1answer
5k views

Meaning of “positive position” and “negative position” in type theory?

What does "in positive position" and "in negative position" mean in the context of type theory? The only thing I understood from Bob Harper's blog post on the topic is that there is a connection ...
7
votes
2answers
315 views

Generating constraints to solve dependently-typed metavariables?

In dependent-types, Miller pattern unification is used to solve a decidable fragment of higher-order unification. This allows dependently-typed languages to contain metavariables or implicit arguments....
7
votes
1answer
265 views

Is there any difference between extensible records and dependent maps

In a typed setting, records can be thought of as a map from field to type. If there is a well-typed record merge operation (which allows overlapping fields), is there any real difference between the ...
7
votes
1answer
354 views

Curry Howard correspondence to Predicate Logic?

So I'm trying to get my head round Curry-Howard. (I've tried at it several times, it's just not gelling/seems too abstract). To tackle something concrete, I'm working through the couple of Haskell ...
5
votes
2answers
283 views

What terms type systems exclude?

I understand type systems like the simply typed lambda calculus, system F and the calculus of constructions include a different subset of all lambda terms. But what, precisely, are the terms each of ...
2
votes
1answer
315 views

Would adding recursive named functions to Simply typed lambda calculus make it Turing complete?

Say I have Simply typed lambda calculus, and add an assignment rule: <identifier> : <type> = <abstraction> Where ...
6
votes
2answers
277 views

Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion. Haskell is strongly typed and we can define the natural numbers ...
5
votes
1answer
76 views

Pure type systems and let-expressions

I can not find any simple and detailed source of how to add non-recursive let-expressions to pure type systems. The best I found is the Henk paper by Simon Peyton Jones, but his explanation of this ...
5
votes
1answer
330 views

Non-termination of types in Martin-Löf's Type:Type?

In the pre-history of dependent type theory, Per Martin Löf introduced a calculus that is in some sense the simplest dependent type theory and the most general form of impredicative polymorphism. It ...
5
votes
4answers
175 views

How to use Type application Rule to get a desired type

In type application Rule : $$\dfrac{ \Gamma \vdash t_1 : T_{11} \to T_{12} \qquad \Gamma \vdash t_2 : T_{11}} { \Gamma \vdash t_1 \ t_2 : T_{12} } \textsf{ (T-App)}$$ if we ...
3
votes
0answers
490 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 "...
2
votes
1answer
126 views

Why do we distinguish between term abstraction and type abstraction in System F?

In System F, we distinguish between types and terms. Types are defined by the following BNF: \begin{align} A, B ::=&~\alpha && \text{(type variable)} \\ &|~A \rightarrow B &...
2
votes
1answer
44 views

liskov substitution principle seems to have two conventional meanings

This is a question about the semantics of the name, rather than about the principle itself. What is the Liskov Substitution Principle (LSP)? LSP seems to have two meanings in the literature I've ...
1
vote
2answers
152 views

How is a type system related to a progam?

In another question about Lambda Calculus, Andrej Bauer made the comment: Lambda calculi of various forms are formal systems. They consist of abstract syntax (for terms and for types, if present),...
4
votes
1answer
714 views

What is the use case for multi-type-parameter generics?

In C#, one can define a class/method/function with multiple type parameters. For example, ...
3
votes
1answer
42 views

Multiplicative Pure Type Systems

All the references about Pure Type Systems I know consider only systems that allow to recover natural deduction systems with additive rules. Is there any variant that allows it to recover natural ...
3
votes
2answers
77 views

The difference between a Hoare Triple/Assertion and a Typed Function

I have been trying to wrap my head around applying Hoare Logic and am running into the question of how Hoare triples are any different from (simply) a typed function. That is, say you have a typed ...
3
votes
1answer
119 views

Is it possible that the universe of types could be closed?

I asked a pretty vague question. I wasn't able to make it precise, but I can now. It seems to be out of the scope of the previous question, so I open another one. In dependently-typed languages such ...
2
votes
1answer
393 views

Does types being terms imply your dependend theory is considered polymorphic?

In the introduction of the book by B.Jacobs, "Categorical Logic and Type Theory" (it's online here), he classifies type systems into three general flavours: Simply typed ones, depended typed (term ...
2
votes
1answer
41 views

How to define function type in AGDA

The "function" type $\rightarrow$ is predefined in Agda. But how would one define it if it was not predefined? Specifically I am talking about $\rightarrow$ in: ...
2
votes
1answer
55 views

Induction on typing derivation in refinement types system

From the text Principles of Type Refinement page 14: The author introduces in definition 2.2.7 the rule: $$ \dfrac{\Pi \vdash t : R \qquad R \le S}{\Pi \vdash t : S} $$ and gives the following ...
1
vote
1answer
52 views

how to deduce a function subtype rule from a given function type definition

This question relates to liskov substitution principle seems to have two conventional meanings but is really a different question, so I'm posing it as a new question. I'm doing a bit of research into ...