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

learn more… | top users | synonyms

4
votes
1answer
38 views

Is there a “lambda cube” for interaction nets?

The lambda calculus is an untyped language that is often extended with logical frameworks such as the vertices of the λ-cube. Is there something similar to it, but for interaction nets? What about ...
6
votes
1answer
96 views

Is there a theory of overloading types?

There is a sound theory of overloading operators and functions realized by type classes in Haskell, and to rougher extent by traits in Rust, etc. In mathematics however, there are many situations ...
6
votes
1answer
189 views

What type system fits the subclass of λ-terms that can be reduced optimally?

There is a subset of λ-calculus terms that can be reduced by Lamping's Abstract Algorithm without using the Oracle. That is an interesting subset, because only for those terms it is proven that ...
9
votes
1answer
122 views

Dependent types over Church-encoded type in PTS/CoC

I'm experimenting with pure type systems in Barendregt's lambda cube, specifically with the most powerfull one, the Calculus of Constructions. This system has sorts ...
5
votes
1answer
84 views

Featherweight Generic Java formalization in Coq

I've been searching for some nice formalization of FGJ (Featherweight Generic Java) in Coq. I am going to develop an extension of FGJ in Coq, so I hope there is an appropriate Coq implementation which ...
9
votes
1answer
239 views

Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?

On one hand, Gödel's Second Incompleteness Theorem states that any consistent formal theory that is strong enough to express any basic arithmetical statements can't prove its own consistency. On the ...
12
votes
3answers
409 views

What are the negative consequences of extending CIC with axioms?

Is it true that adding axioms to the CIC might have negative influences in the computational content of definitions and theorems? I understand that, in the theory's normal behavior, any closed term ...
10
votes
2answers
103 views

Church-Rosser property for dependently typed lambda calculus?

It is well-known that the Church-Rosser property holds for $\beta \eta$-reduction in simply-typed lambda calculus. This implies that the calculus is consistent, in the sense that not all equations ...
9
votes
1answer
116 views

Logical Reations for an Impredicative System in a Predicative MetaTheory

Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in ...
6
votes
3answers
264 views

Universal and existential types

I'm trying to wrap my head around the concepts of universal and existential types but everywhere I look, I see either logical or operational intuitions (or implementations) (e.g. TAPL book by B. ...
1
vote
1answer
165 views

What's wrong with this LEAN proof? [closed]

I'm learning to use the LEAN theorem prover and I got stuck in a proof of a simple fact in first-order logic: $$ p(x) \rightarrow \forall x p(x) $$ My code is the following: variables (A : Type) ...
3
votes
1answer
139 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
68 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 ...
7
votes
1answer
99 views

Is MLTT effectively pCiC without Prop?

Is Martin-Löf type theory basically the predicative Calculus of inductive Constructions without impredicative $\mathtt{Prop}$? If they're closely related but with more differences than just ...
5
votes
1answer
110 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 ...
2
votes
4answers
266 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
53 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 ...
3
votes
0answers
174 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 ...
8
votes
2answers
398 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 ...
11
votes
3answers
461 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 ...
8
votes
1answer
272 views

Why it's impossible to declare an induction principle for Church numerals

Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way: ...
8
votes
3answers
296 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 ...
-1
votes
1answer
241 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? ...
10
votes
1answer
886 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 ...
6
votes
1answer
369 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 ...
10
votes
1answer
373 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
174 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 ...
-2
votes
1answer
115 views

Types as the Core of the Programming Languages

Why theoreticians consider 'types' as the core part of the programming languages?
3
votes
1answer
107 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 ...
10
votes
1answer
201 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 ...
3
votes
0answers
80 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: ...
5
votes
2answers
241 views

Law of excluded middle in MLTT

Is it possible to add law of excluded middle to Martin Lof Type Theory as an axiom? It seems to me, that it's possible to add it to Coq since Coq has a module for non constructive reasoning. Also, it ...
6
votes
1answer
204 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 ...
5
votes
1answer
109 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
1answer
105 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 ...
4
votes
1answer
114 views

What is the first name of Bainbridge?

Bainbridge coauthored the paper `Functorial Polymorphism' with Freyd, Scedrov and Scott (DOI). What is his/her first name?
9
votes
1answer
182 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 ...
2
votes
2answers
92 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 ...
9
votes
1answer
97 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 ...
7
votes
1answer
109 views

Where is relational parametricity in hyperdoctrine or topos models explored?

Reynolds originally proposed a relational semantics for the second order polymorphic lambda calculus[1]. However he later showed[2] that this approach was inconsistent with classical set theory. ...
7
votes
3answers
230 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 ...
3
votes
2answers
133 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 ...
11
votes
0answers
108 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 ...
0
votes
1answer
113 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 ...
8
votes
2answers
295 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 ...
15
votes
5answers
2k 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?
10
votes
1answer
388 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
124 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 ...
5
votes
1answer
253 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. ...
5
votes
0answers
177 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 ...