Questions tagged [type-theory]

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

Filter by
Sorted by
Tagged with
7
votes
0answers
275 views

MLTT vs. [weak] MSOL

I've noted that both Martin-Lof type theory and [Weak] Monadic Second-Order logic (eg over trees) enjoy the ability to express basically any finite computer program, in a decidable manner. I was ...
1
vote
1answer
163 views

What's the effect of imposing the following restriction on inductive type families?

Let a simple expression be either: A free variable A data constructor of an inductive type family, applied to 0 or more simple expressions What would be the effect of imposing the following ...
9
votes
0answers
207 views

reference request: deciding validity of higher-order quantified boolean formulas is not Kalmar-elementary

$\newcommand\iddots{⋰}$In "A simple proof of a theorem of Statman" (TCS 1992), Harry Mairson gives a simple proof of Statman's result that deciding $\beta\eta$-equality of terms in simply typed lambda ...
4
votes
0answers
314 views

Subtyping rules for extension of System $F_\omega$ with subtyping and kind-level variance tracking

I need an extension of System $F_\omega$ with subtyping, and where the variance of type constructors is reflected in their kind. Unfortunately, System $F^\omega_{<:}$, as defined in chapter 31 of ...
4
votes
1answer
168 views

What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?

In the context of constructive type theory, a term inhabiting some type is said to be in canonical form if it is explicitly built up using the constructors of that type. Particularly, the only ...
11
votes
1answer
454 views

Is there a good notion of non-termination and halting proofs in type theory?

Constructive type theory with its basic interpretation under the curry howard correspondence consists only of total, computable functions. In the literature, some has been said on using "computational ...
11
votes
2answers
478 views

Implementing "Internal" Languages

One of the most practical consequences of the "Curry-Howard-Lambek" correspondence is that the syntax of many lambda-calucli/logics can be used to perform constructions in a sufficiently structured ...
8
votes
1answer
500 views

Examples of Universe inconsistency in normal use of dependent types

In dependent types, Type : Type results in inconsistency (Girard's or Hurken's paradox). Are there examples of universe inconsistency (where assuming ...
8
votes
1answer
395 views

PiSigma: why does 'unfold' bind a variable?

I'm trying to understand the paper ΠΣ: Dependent Types without the Sugar by implementing an interpreter and type checker for the language. In doing so, I've seen that the ...
5
votes
2answers
359 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
195 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
333 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 ...
11
votes
1answer
513 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 ...
4
votes
1answer
435 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
496 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 ...
13
votes
3answers
786 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 ...
14
votes
2answers
409 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 ...
15
votes
1answer
421 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 ...
10
votes
3answers
939 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
714 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) (p q ...
7
votes
1answer
333 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
138 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 ...
14
votes
1answer
692 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 $\mathtt{...
5
votes
1answer
535 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
329 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 ...
1
vote
1answer
70 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
328 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
2k 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 ...
16
votes
3answers
1k 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 ...
19
votes
1answer
1k 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: ...
10
votes
3answers
1k 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 ...
9
votes
1answer
3k 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? ...
13
votes
3answers
833 views

For what languages is there already a theory of observational equivalence?

For a correctness proof, I'm looking for a usable notion of program equivalence $\cong$ for Barendregt's pure type systems (PTSs); missing that, for enough specific type systems. My goal is simply to ...
14
votes
1answer
2k 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-...
8
votes
1answer
641 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
919 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 ...
9
votes
1answer
238 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
179 views

Types as the Core of the Programming Languages

Why theoreticians consider 'types' as the core part of the programming languages?
7
votes
1answer
323 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 ...
12
votes
1answer
299 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
174 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
3answers
1k views

Law of excluded middle in MLTT

Is it possible to add law of excluded middle to Martin-Löf 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 ...
7
votes
1answer
305 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
120 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
2answers
455 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
2answers
189 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?
16
votes
1answer
491 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 ...
3
votes
2answers
142 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 ...
10
votes
1answer
172 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{\...
9
votes
1answer
320 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. ...

1
4
5
6 7 8