We’re rewarding the question askers & reputations are being recalculated! Read more.

Questions tagged [type-theory]

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

Filter by
Sorted by
Tagged with
7
votes
1answer
309 views

Decidability of parametric higher-order type unification

I'm making a language that has higher-kinded types (like Haskell) and allows type synonyms to appear partially applied in type expressions (unlike Haskell). As an example, consider the following ...
4
votes
1answer
121 views

Rendering of type-level computation

Programming languages with dependent types and/or higher-kinded types feature what might be called compile-time computation at the type-level. This is usually defined as follows (I'm omitting some ...
5
votes
1answer
321 views

Can all linear lambda calculi be linearity checked syntactically?

Given a lambda calculus with explicit linearity and usual application and abstraction, can the linearity check be done on an untyped syntax tree if we keep track of the structural types? Are the ...
3
votes
4answers
303 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
65 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
303 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
846 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
830 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? ...
27
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
555 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
798 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
212 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
204 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
162 views

Types as the Core of the Programming Languages

Why theoreticians consider 'types' as the core part of the programming languages?
10
votes
1answer
255 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
163 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
279 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
118 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
308 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
347 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 ...
10
votes
1answer
132 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
158 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
310 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
140 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
388 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
742 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
550 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
206 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
234 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
772 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
304 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
366 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
517 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
2k 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
1k 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
492 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
389 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
423 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 ...