Questions tagged [type-theory]

formal systems to specify properties of objects

Filter by
Sorted by
Tagged with
29
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?
9
votes
1answer
590 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 ...
39
votes
1answer
5k 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 ...
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 ...
15
votes
2answers
832 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
568 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
2k 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 ...
7
votes
2answers
334 views

What is the Curry-Howard analogue for linear logics?

As defined by Wikipedia, (The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by 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
680 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
77 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 ...
55
votes
3answers
9k 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 ...
32
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 ...
34
votes
2answers
6k 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
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 ...
17
votes
2answers
409 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 ...
27
votes
2answers
3k views

Why is C's void type not analogous to the empty/bottom type?

Wikipedia as well as other sources that I have found list C's void type as a unit type as opposed to an empty type. I find this confusing as it seems to me that <...
12
votes
1answer
711 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
241 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-...
5
votes
2answers
194 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
163 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
519 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
6k 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 ...
9
votes
2answers
882 views

Type inference + overloading

I'm looking for a type inference algorithm for a language I'm developing, but I couldn't find one that suits my needs because they usually are either: à la Haskell, with polymorphism but no ad-hoc ...
7
votes
2answers
334 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
302 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
398 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
336 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
360 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
285 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
355 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
183 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
506 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
133 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
48 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
158 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
2answers
97 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 ...
4
votes
1answer
728 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
137 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 ...
3
votes
1answer
43 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 ...
2
votes
1answer
467 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
78 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 ...
2
votes
1answer
51 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: ...
1
vote
1answer
63 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 ...