# Questions tagged [type-theory]

formal systems to specify properties of objects

47 questions
Filter by
Sorted by
Tagged with
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?
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 ...
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 ...
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 ...
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 ...
568 views

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{\... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 <... 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 ... 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-... 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 ... 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 ... 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... 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 ... 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 ... 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 ... 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 ... 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 ... 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.... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 ... 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 "... 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 &... 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 ... 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),... 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 ... 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, ... 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 ... 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 ... 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 ... 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 ...
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: ...