Questions tagged [type-theory]

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

Filter by
Sorted by
Tagged with
3
votes
4answers
300 views

Why do non-proper types have no terms?

I'm attending a course on Type Theory. The textbook is 'Types and Programming Languages' by Prof. Benjamin C. Pierce. In Chapter 29, Prof. Pierce introduces 'type operator', which can generate ...
0
votes
1answer
64 views

Why is the polymorphic weight 1

I am reading through through a paper called HMF: Simple Type Inference for First-Class Polymorphism by Daan Leijen of Microsoft Research. In the paper it describes how to calculate the polymorphic ...
4
votes
0answers
301 views

Category theory in plain MLTT

I want to define a category in simple MLTT (not in HoTT). I defined it with the help of setoids. I.e. category consists of: a type of objects with equivalence relation (Obj : Set) a type of arrows ...
20
votes
2answers
1k views

Is there a typed lambda calculus which is consistent and Turing complete?

Is there a typed lambda calculus where the corresponding logic under the Curry-Howard correspondence is consistent, and where there are typeable lambda expressions for every computable function? This ...
15
votes
3answers
829 views

Why do constructivists not seem to care too much about call/cc

So a little while back I first had someone tell me that call/cc could allow proof objects for classical proofs by implementing Peirce's law. I did some thinking about the topic recently and I can't ...
11
votes
3answers
820 views

Ramification of An Impredicative Type Theory

Most type theories that I'm aware of are predicative by which I mean that Void : Prop Void = (x : Prop) -> x isn't well-typed in most theorem provers as this ...
6
votes
1answer
2k views

Why study type theory?

After reading the literature on type theory (especially the constructive kind - CTT) I'm left wondering "why" should one study type theory, specifically within the confines of "computing" in general? ...
28
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 ...
13
votes
1answer
1k views

Why was there a need for Martin-Löf to create intuitionistic type theory?

I've been reading up on Intuitionistic Type Theory (ITT) and it does make sense. But what I'm struggling to understand is "why" was it created in the first place? Intuitionistic Logic (IL) and Simply-...
7
votes
1answer
547 views

Squash type vs Propositional truncation type

Homotopy type theory has a notion of propositional truncation type. It seems to me that it's strongly related to a notion of squash types. (See https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf ...
11
votes
1answer
789 views

Logical framework vs type theory

What is the difference between logical framework and type theory? Both of them have types, terms, and are based on dependently typed lambda calculus. We have Edinburg LF which is based on lambda-pi ...
10
votes
1answer
211 views

Type systems preventing laziness-related memory leaks?

Perhaps the main source of performance problems in Haskell is when a program inadvertently builds up a thunk of unbounded depth - this causes both a memory leak and a potential stack overflow when ...
5
votes
1answer
203 views

Can type inference be classified in two groups: unification-based and control-flow-based?

I recently came across the 1995 paper Safety analysis versus type inference (pdf link) by Palsberg and Schartzbach that contrasts unification-based type inference and static analysis methods based on ...
-2
votes
1answer
161 views

Types as the Core of the Programming Languages

Why theoreticians consider 'types' as the core part of the programming languages?
10
votes
1answer
253 views

Reference for the fact that (0=1) implies false requires a universe in MLTT

It's a fairly well-known fact that deriving a contradiction from a disequality (for example, $(0=1) \to \bot$) in Martin-Loef type theory requires a universe. The proof is also fairly ...
5
votes
1answer
117 views

Logics for timed resource control

I'm studying proof theory and I've seen that linear logic can be used as a way to control resource usage, since by the propositions-as-types it is equivalent to the linear lambda calculus. Is there a ...
3
votes
0answers
160 views

Type theoretic equivalent of isomorphism class

How one defines the notion of isomorphism class in type theory? For concreteness I will describe what I mean with an example in Coq. Suppose I have a record ToyRec: ...
6
votes
1answer
275 views

How Univalence can be used for proofs about algorithm correctness

I read a book on homotopy type theory. HoTT has the univalence axiom. This axiom seems to simplify working in category theory, but which other fields of mathematics it simplifies? I.e. how can I use ...
3
votes
2answers
117 views

Typechecking liveness properties of coprograms

Clarification: in Total Functional Programming terminology, a program terminates with useful input, while a coprogram doesn't necessarily terminates, and repeatedly produces useful input. I am ...
3
votes
1answer
304 views

Constructing terms of function types out of the empty type

If a function $f$ is understood as its graph, i.e. a set of pairs $\langle x,y\rangle$ where $x$ is input and $y$ is output, then the empty set $\emptyset$ is a valid function, and for any set $A$, we ...
28
votes
5answers
8k views

What are some good introductory books on type theory?

I'm recently studying Haskell and programming languages. Could someone recommend some books on type theory?
13
votes
1answer
341 views

Minimal specification of Martin-Löf type theory

I'm reading the formal presentation of Martin-Löfs type theory (appendix of the HoTT book). The authors introduce a hierarchy of universes, then $\Pi, \Sigma,+, {\bf 0}, {\bf 1}$ and also $W$-types as ...
9
votes
1answer
127 views

Relating univalence for a theory of cateogries to the skeleton concept

Say I work in homotopy type theory and my sole objects of study are conventional categories. Equivalences here are given by functors $F:{\bf D}\longrightarrow{\bf C}$ and $G:{\bf C}\longrightarrow{\...
3
votes
2answers
156 views

Can Curry-Howard prove a theorem from the types in your program, that has nothing to do with your program? [closed]

The following link states: Curry-Howard means that any type can be interpreted as a theorem in some logical system, and any term can be interpreted as a proof of its type. This does not mean that ...
7
votes
3answers
308 views

How high are the higher types that appear in practice?

This is admittedly a rather naively put and vague question, and I'm not sure how much more specific I want or can make it, but I'll try. By "practice" I mean surely in actual programming practice (of ...
11
votes
0answers
137 views

Are the types that show monads are more powerful than continuations revealing something of fundamental importance?

In 1992 in the paper Imperative Functional Programming, Simon Peyton Jones and Philip Wadler write: So monads are more powerful than continuations, but only because of the types! It is not clear ...
2
votes
1answer
379 views

Dependent Sums and Products

I'm trying to understand the connections between a few different concepts fundamental to dependent type theory. Dependent functions ($\Pi$-types) Including non-dependent functions ($A \rightarrow B$)...
8
votes
2answers
722 views

Explaining monad transformers in categorical terms

Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers. How could monad transformers be described in the terms ...
10
votes
1answer
538 views

Can affine lambda calculus solve every problem in P?

In Advanced Topics in Types and Programming Languages it is mentioned, in the chapter on sub-structural type systems, that a "carefully crafted" affine lambda calculus with a recursion combinator for ...
2
votes
2answers
202 views

How to translate the axiom schema of induction by Curry-Howard?

I'm trying to understand the Curry-Howard correspondence. I am comfortable with it for propositional logic, but get confused when $\forall, \exists$ quantifiers come in the picture. The axiom schema ...
6
votes
1answer
302 views

Type theory for memory safe data structures

Data structures such as a doubly linked list and a B+ tree have blocks of memory that have multiple pointers to it. This creates the risk that a bug will allow memory to be accessed after being freed. ...
6
votes
0answers
233 views

Generalizing Haskell: could we replace Hask with Cat?

N.B. I asked the same question on Stack Overflow but it was suggested that it is too theoretical for this forum. It is great that Haskell allows us to walk around in the category $Hask$. But ...
5
votes
1answer
520 views

Is this behavior in a programming language inconsistent?

I'm developing a tiny programming language to try to wrap my head around type inference, and I'm trying to figure out if its behavior makes sense or not. Here's the problem: The identity function <...
7
votes
1answer
760 views

Practical implementation of Hindley–Milner with typeclasses — matching vs most general unifier

I'm trying to get a deep understanding of a (great) paper "Typing Haskell in Haskell". I'm having difficulties understanding the implementation of two methods there — the ...
6
votes
1answer
127 views

A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2

I'm having a problem regarding Theorem 5.4.40.3 of Barendregt's Lambda calculi with types (1992), a chapter in Handbook in logic in computer science. (I'm referring to the PostScript version available ...
1
vote
0answers
78 views

How are these statements about CTT reconcilable?

From http://www.scholarpedia.org/article/Computational_type_theory#Judgements_and_Propositions: The other kind of logical claim made in CTT is the judgment that a belongs to A. This can be reduced ...
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 ...
5
votes
1answer
299 views

Can factorial be encoded in the Kappa-calculus with fixed point operator?

Suppose we have a $\kappa$-calculus with operator $fix$, that could be used to transform function with type $(1 \rightarrow a) \rightarrow a$ to a value of type $1 \rightarrow a$. We use a normal ...
4
votes
1answer
353 views

Rules about Prop and Set in UTT

In Luo's UTT (type theory which is used in Agda, Idris, and other dependently typed programming languages), there're are two rules for $\Pi$ types. One for $\mathsf{Prop}$ and one for $\mathsf{Set}$. ...
5
votes
1answer
499 views

Types which correspond to sets of cardinality of continuum

Are types which correspond to sets with cardinality of continuum possible in MLTT (or in any other constructive theory)? On the first sight, they aren't, since elements of types are terms and we ...
11
votes
1answer
1k views

W-types vs Inductive types

Martin-Löf type theory uses W-types to define inductive structures like integers, lists, etc. However, calculus of inductive constructions doesn't use them in the same way, inductive types there seems ...
3
votes
1answer
987 views

Monomorphic vs Polymorphic type theory

I am currently reading the book Programming in Martin-Löf type theory by Nordström et al. In the book they have two important parts, one about monomorphic set theory and the other about polymorphic ...
21
votes
1answer
2k views

What is the difference between arrows and exponential objects in a cartesian closed category?

In a Cartesian Closed Category (CCC), there exist the so-called exponential objects, written $B^A$. When a CCC is considered as a model of the simply-typed $\lambda$-calculus, an exponential object ...
3
votes
1answer
481 views

Occurs check in type inference

I'm reading about type inference in chapter 30 of Programming Languages: Application and Interpretation and I'm trying to understand exactly how the occurs check works in an example I came up with. ...
8
votes
0answers
385 views

Complete combinator basis for System F-omega

The S and K combinators form a complete (and Turing complete) basis when untyped. Within the Hindley-Milner type-system, and I believe within system $F$ as well, S and K can encode any well-typed ...
5
votes
1answer
120 views

Extending simple types to allow `fix`

I'm reading some lecture notes saying that “fix cannot be defined in the simply typed lambda-calculus” and that “no expression that can lead to non-terminating ...
6
votes
2answers
416 views

“Correctness” of type theory

How to "proof" that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one? When type ...
9
votes
1answer
242 views

Example of where violation of strict positivity condition in inductive types leads to inconsistency

Most dependent typed systems have a strict positivity conditions for inductive types. Does anybody know an example where violation of the condition leads to inconsistency in the system?
4
votes
2answers
146 views

Well-formedness condition for inductive types

I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. ...
10
votes
1answer
637 views

Algorithm to determine function equality on the simply typed lambda calculus?

We know that beta-equality of simply typed lambda-terms is decidable. Given M,N:σ→τ, is it decidable whether for all X:σ, MX $≃_β$ NX?