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]

Type structure is a syntactic discipline for enforcing levels of abstraction.

19
votes
2answers
3k views

What's the difference between ADTs, GADTs, and inductive types?

Might anyone be able to explain the difference between: Algebraic Datatypes (which I am fairly familiar with) Generalized Algebraic Datatypes (what makes them generalized?) Inductive Types (e.g. Coq) ...
3
votes
2answers
336 views

Confusing (to me) statement from “Type Classes in Haskell”

I'm reading up on type classes, and started looking at the paper Type Classes in Haskell. In Section 2.2 - Superclasses, the authors use the following example: ...
15
votes
1answer
886 views

Can boolean algebra be expressed in simply typed lambda caclulus?

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way. ...
26
votes
6answers
9k views

What is the difference between propositions and judgments?

I get confused by the subtle difference between propositions and judgments when exposed to intuitionistic type theory. Can any one explain to me what is the point to distinguish them and what ...
11
votes
3answers
1k views

Type system based on naive set theory

As I understand, in computer science data types are not based on set theory because of things like Russell's paradox, but as in real world programming languages we can't express such complex data ...
32
votes
3answers
2k views

Type classes vs object interfaces

I don't think I understand type classes. I'd read somewhere that thinking of type classes as "interfaces" (from OO) that a type implements is wrong and misleading. The problem is, I'm having a problem ...
11
votes
6answers
2k views

Functions that typed lambda calculus cannot compute

I just want to know some examples of the functions that can be computed by the untyped lambda calculus but not by typed lambda calculi. As I am a beginner, some reiteration of background information ...
7
votes
1answer
251 views

How to define eta-equivalence for F-omega types?

There are (at least) two styles for defining a (declarative) equivalence judgement for a typed lambda calculus: via a plain relation $t_1 = t_2$, via an indexed relation $\Gamma \vdash t_1 = t_2 : T$...
13
votes
4answers
725 views

Modeling objects (OOP) in dependent type theory

I am interested in modeling objects, from object oriented programming, in dependent type theory. As a possible application, I would like to have a model where I can describe different features of ...
6
votes
3answers
517 views

Boolean as subtype of integer

In languages oriented towards systems programming, digital logic and hardware design, it's common to treat boolean as a subtype of integer. In languages oriented towards mathematics and type theory, ...
9
votes
2answers
315 views

Research on call-site based type inference?

I'm trying to learn more about whole-program type checking and type inferencing systems that use information from function call sites to compute type information (in addition to the standard approach ...
10
votes
3answers
2k views

Type inference for imperative statements other than assignment

In my search for research papers about type systems for imperative languages, I only find solutions for a language with mutable references but without genuine imperative control structures such as ...
12
votes
1answer
364 views

Barendregt's proof of subject reduction for $\lambda2$

I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of Lambda calculi with types). The last step of the proof (page 60), says: "and hence by Lemma 4.1.19(1), $\quad\Gamma,x:\rho\...
15
votes
3answers
847 views

Can we prove weak normalization for System F by induction on a transfinite ordinal

Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
22
votes
2answers
1k views

Is there an expressiveness hierarchy for type systems?

Inspired by the extensive hierarchies present in complexity theory, I wondered if such hierarchies were also present for type systems. However, the two examples I've found so far are both more like ...
15
votes
2answers
378 views

Proof theory of biproducts?

A category has biproducts when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts? Perhaps the best-known example is the ...
22
votes
1answer
2k views

What's the relation and difference between Calculus of Inductive Constructions and Intuitionistic Type Theory?

As stated in the title, I wonder any relation and difference between CIC and ITT. Could someone explain or point to me some literature that compares these two systems? Thanks.
9
votes
1answer
428 views

What is the role of the Bicolored Calculus of Constructions?

So, I'm reading a bit about elaboration, particularly, algorithms based on the Bicolored Calculus of Construction, and I'm a bit confused. I don't understand what exactly the purpose of the $CC^{bi}$ ...
13
votes
2answers
427 views

What are the equational laws for zero types?

Disclaimer: while I care about type theory, I don't consider myself an expert on type theory. In the simply typed lambda calculus, the zero type has no constructors and a unique eliminator: $$\frac{\...
16
votes
1answer
645 views

Seeking Scott's original LCF paper

Is the following manuscript publically available? Dana Scott, 1969, A theory of computable functions of higher type. Unpublished seminar notes, 7 pages, University of Oxford. There is a discussion ...
7
votes
1answer
318 views

Implications of the rule of cumulativity in the Calculus of Constructions

Please help me understand some type theory research. As suggested in "Type Checking with Universes" by Robert Harper and Robert Pollack, we can add the following rule to our otherwise standard COC or ...
6
votes
2answers
405 views

With equirecursive types are there downsides to making all types potentially recursive?

By this I mean to ask, is it a bad idea to have all type constructor term expressions abstracted with $\mu$ just in case they need to be recursive? For example, $Bool : Type;$ $Bool = (\mu Bool' ...
9
votes
2answers
285 views

Does the order of declarations in an inductive type matter?

I was wondering if the order of declarations of an inductive type can matter. For example in Coq you can define Nat either by: ...
23
votes
2answers
1k views

Do dependent types give you everything subtyping does?

Types and Programming Languages focuses quite a bit on subtyping, but as far as I can tell, subtyping doesn't seem especially fundamental. Does subtyping give you anything more than dependent types do?...
27
votes
1answer
866 views

Inductive types for large countable ordinal notations.

I'm looking to build notations for large countable ordinals in a "natural way". By "natural way" I mean that given an inductive data type X, that equality should be the usual recursive equality (the ...
46
votes
5answers
5k views

What is the most intuitive dependent type theory I could learn?

I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles ...
16
votes
3answers
1k views

What is the role of predicativity in inductive definitions in type theory?

We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A :...
11
votes
2answers
312 views

References to programming languages based on conditional logics

Conditional logics are logics which augment traditional logical implication with modal operators corresponding to other notions of condition (for example, the causal conditional $A\; \square\!\!\!\!\...
25
votes
1answer
1k views

Are types propositions? (What are types exactly?)

I've been reading a lot on type systems and such and I understand roughly why they were introduced (in order to resolve Russel's paradox). I also understand roughly their practical relevance in ...
39
votes
4answers
3k views

How would I go about learning the underlying theory of the Coq proof assistant?

I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
18
votes
3answers
2k views

Classification of Typed/Untyped Lambda Calculi

Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi? I'm particularly ...
44
votes
3answers
3k views

How do 'tactics' work in proof assistants?

Question: How do 'tactics' work in proof assistants? They seem to be ways of specifying how to rewrite a term into an equivalent term (for some definition of 'equivalent'). Presumably there are formal ...
31
votes
4answers
2k views

Relationship between contracts and dependent typing

I've been reading some articles on dependent types and programming contracts. From the majority of what I've read, it seems that contracts are dynamically checked constraints and dependent types are ...
17
votes
1answer
2k views

Prove proof irrelevance in Coq?

Is there a way to prove the following theorem in Coq? Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. EDIT: An attempt to give a brief ...
12
votes
1answer
2k views

Data structures in programming language with linear types

Assume we are dealing with a programming language that has support for linear types (terms of linear type can be used at most once, so to say). This allows for treating some computational effects (...
1
vote
0answers
447 views

Well Defined Ordering Relations in Object Oriented Type Systems [closed]

In any Object-Oriented type system the type relation of two objects A and B can be characterized in exactly one of the following ways: A has the same type as B A is a subtype of B B is a subtype of A ...
10
votes
2answers
333 views

Are there semi-decision procedures for this theory?

I have the following typed theory |- 1_X : X -> X f : A -> B, g : B -> C |- compose(g,f) : A -> C F, f : A -> B |- apply(F,f) : F(A) -> F(B) ...
17
votes
2answers
2k views

Implicit vs explicit subtyping

This page asserts that many languages do not use implicit subtyping (structural equivalence), prefering explicit/declared subtyping (declaration equivalence) I've mostly used programming ...
28
votes
6answers
2k views

Why naturals instead of integers?

I'm interested in why natural numbers are so beloved by the authors of books on programming languages theory and type theory (e.g. J. Mitchell, Foundations for programming languages and B. Pierce, ...
7
votes
2answers
725 views

An example of a totally computable function that is not definable in system T?

Could you give me an example of a totally computable function of type N × N → N that is not definable in System T? Thanks.
12
votes
2answers
439 views

What happens if we try to extract a witness but it actually does not exist from a term of existential type?

Given a term t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y)) in Martin-Lof's type theory, what's the value of w(t(0)), where ...
25
votes
2answers
1k views

Context Sensitive Grammars and Types

1) What, if any, is the relationship between static typing and formal grammars? 2) In particular, would it be possible for a linear bounded automaton to check whether, say, a C++ or SML program was ...
5
votes
1answer
165 views

Nested automatization of type inference of forall elimination

Following a previous question about how to automatize the type inference in a forall elimination of an application, now suppose we want to do the same but for a nested forall, say $(\Lambda X_1.\...
3
votes
2answers
317 views

Type a variable-argument function?

Is it possible to type a variable-argument function? EDIT: like those defined in Scheme.
9
votes
1answer
425 views

In System F à la Church, can we automatize type inference for the for-all elimination?

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$. Now, suppose ...
11
votes
2answers
414 views

Does the System F with pairs have the strong normalisation and subject reduction properties?

It is easy to look in a lot of textbooks the proofs of subject reduction and strong normalisation for System F, also, sometimes there are definitions of System F with pairs, where (t,r) is a term, not ...
7
votes
0answers
388 views

Type inference with subtype constraints and polymorphism using Trifonov and Smith's constraint maps

Trifonov and Smith's Subtyping Constrained Types (1996) introduces constraint maps to represent consistent closed constraint sets (such maps providing sets of lower and upper bounds to each variable ...