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.

3
votes
1answer
75 views

Is there a simple algorithm for proof search on CoC?

Given the usual Calculus of Constructions with an extra primitive, _, that stands for "attempt to fill this location in a way that type-checks", is there any simple/...
-1
votes
0answers
23 views

Encoding naturals in the calculus of constructions and in a language like Idris

I'm learning some type theory and trying to relate that to what I already know about proving things in Idris and similar languages. So, if I were to encode natural numbers in CoC, I'd probably have ...
0
votes
1answer
84 views

Definitional equality of recursive function definition by “infinite unfolding”

The context is checking definitional equality in dependent type theory implementations. Consider in Coq ...
3
votes
0answers
57 views

Proof that CIC or Dybjer-style eliminators are strongly-normalizing?

Related to this question I'm wondering, what is the standard technique for showing that dependent types with eliminators are strongly normalizing? I'm thinking something like the Calculus of ...
3
votes
0answers
67 views

Is it possible to check equality of equi-recursive types, or recursive λ-terms?

Can we determine if two λ-terms are equal? Given two lambda terms, let's say they are equal if their (possibly infinite) Bohm trees are. Under this definition, for example, ...
3
votes
1answer
93 views

Universe polymorphism: the inference of universes and their constraints

When making a universe polymorphic definition in Coq, universes and their constraints are automatically inferred. Are they somewhat the most general ones (in a sense similar to the principal type ...
4
votes
0answers
120 views

Hereditary Substitution with Inductives and Eliminators?

I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators? In particular, normalizing the application of an eliminator to an ...
2
votes
0answers
74 views

What's the example of natural transformation in 'Type" that is not a parametric function?

Take a type theory of your choice (perhaps System Fω). Parametric functions are known to be natural transformations in 'Type' category. Yet not every natural transformation in 'Type' is a polymorphic ...
6
votes
1answer
178 views

Where do people publish/submit their work on type theory?

Besides the most common venues (perhaps POPL, ICFP, LICS and FSCD), where else are papers on type theory commonly published? Especially, I'm looking for more "pure mathematical" venues/journals which ...
6
votes
1answer
80 views

Is CoC inconsistent with cnat_ind axiom?

It is not possible to derive induction for Church-encoded datatypes on the Calculus of Constructions (source). Moreover, according to the accepted answer to another question, it is also not possible ...
6
votes
2answers
189 views

Is case analysis on normal forms of lambda terms sufficient to prove parametricity results?

There are many closed terms of a given type. For instance, both of these terms: $$ \lambda x . x $$ $$ \lambda x . (\lambda y . y) x $$ have a type of a polymorphic identity function: $$ \forall X ....
-1
votes
0answers
39 views

What is the difference between a Top type and a Unit type [migrated]

Wikipedia defines a Top type: (edited for readability) The Top type [...] is the universal supertype, as all other types in any given type system are subtypes of Top However, the article goes on ...
6
votes
3answers
267 views

When a type is a value?

In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason ...
-3
votes
1answer
67 views

Soundness of type (systems)

For someone without strong background in theoretical computer science: can soundness be a property of a type (given a type system), or a property of type systems only? In other words, can we say that ...
4
votes
1answer
162 views

Can a term on normal form prove an illogical assertion?

Suppose we take a language such as Agda and disable the features that make it consistent; for example, universe polymorphism, structural recursion checks and similar. Suppose then that we take a term ...
0
votes
1answer
56 views

Is a reference on T a subtype of T?

If I take the book Practical Foundations for Programming Languages by Robert Harper, the following definition is given for subtyping: A subtype relation is a pre-order on types that validates the ...
5
votes
1answer
97 views

Strong Normalization of Extended Calculus of Constructions (CC with cumulative universes)

There are some proofs around to prove the strong normalization of the calculus of constructions (i.e. that all type systems in the lambda cube are strongly normalizing). I have analyzed the proof ...
9
votes
2answers
276 views

Hereditary substitution with a universe hierarchy

I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types. I'm wondering, are there any examples of hereditary substitution in ...
6
votes
1answer
123 views

General Induction Principle

Let us suppose that we want to provide for each inductive type an axiom describing the associated elimination/induction principle. For example, given a definition for the naturals: ...
8
votes
1answer
167 views

Understanding the Proof of Strong Normalization of the Calculus of Constructions

I have difficulties in understanding the proof of strong normalization for the calculus of constructions. I try to follow the proof in the paper of Herman Geuvers "A short and flexible proof of Strong ...
5
votes
2answers
153 views

Typing of substitution in a bidirectional type system

In most typed lambda calculi, we have the following lemma: If $\Gamma \vdash t_1 : \tau_1$ and $\Gamma, x : \tau_1, \Delta \vdash t_2 : \tau_2$ then $\Gamma,\Delta[t_1/x] \vdash t_2[t_1/x] : \tau_2[...
5
votes
2answers
302 views

Preservation under Substitution with Telescopes

In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution": If $\Gamma \vdash v : \tau_1$ and $(x : \tau_1) \vdash t : \tau_2$, then $\Gamma \...
8
votes
1answer
160 views

Type theory and computational complexity

Is there a type system, which restricts the lambda terms to the terms which fall inside a complexity class? Like the typable terms in the theory are strictly inside the complexity class ? Or is it not ...
9
votes
1answer
407 views

Proof techniques for showing that dependent type checking is decidable

I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and ...
2
votes
3answers
184 views

Is it reasonable to allow the type of a λ/∀-bound variable to refer to itself?

Usually, in Pure Type Systems, the type of a λ/∀-bound variable is only accessible on its body. That is, on λ (X : A) -> B, <...
4
votes
1answer
96 views

Is the church-style affine calculus of constructions with unrestricted recursion consistent?

Suppose we take the church-style calculus of constructions, except with affine functions (variables must occur at most once) and mutual recursive definitions. For example: ...
9
votes
2answers
152 views

Decidability of type inference and type checking in MLTT

In Martin-Löf's An Intuitionistic Theory of Types: Predicative Part it is proved that type checking $a \colon A$ is decidable subject to $a$ being typeable in the first place, by proving a ...
4
votes
1answer
87 views

Complexity of type-checking in relation to complexity of normalization

In order to verify that a terminating program terminates, one thing that can be done is to actually run the program. That may take a lot of time. If the program is typed in a total type-system, we can ...
4
votes
1answer
167 views

Why isn't it “enough” to prove induction with one extra “INat” argument?

It is well known that it is impossible to prove the induction principle for Natural numbers on the Calculus of Constructions. That is, ...
2
votes
1answer
84 views

Representable functions on System T

In Proof and Types by Girard et alii. Section 7.4.2, I think that the authors want to show that: (1) The set of functions definable in System T coincides with the set of recursive functions whose ...
7
votes
1answer
155 views

If the untyped language is terminating, can we still derive a contradiction from `Type : Type`?

Question If a pure type system has a terminating proof language, can we have Type : Type at the logic level without causing paradoxes (i.e., without causing ...
6
votes
2answers
135 views

Is it possible to create a “quote” function that, given a native λ-term, returns its λ-encoded representation?

Suppose we implement the λ-calculus inside the λ-calculus itself with λ-encodings and Bruijn indices: ...
7
votes
1answer
227 views

Fixed points in dependent type theories

Most dependent type theories aim for some notion of correctness in two respects: The type system must be decidable. The type system must be consistent. e.g. $\forall \tau. \tau$ should not be ...
5
votes
2answers
105 views

Does Standard ML validate (CBV) eta equivalence?

$\eta$ equality of functions is fundamental in their Category-theoretic semantics but in practice even "functional" languages include "impure" features that violate it. Note that this is not an issue ...
1
vote
2answers
184 views

What are the limitations of dependent typing?

It seems dependent types can provide lots of desirable guarantees about program behavior. What kinds of program properties can they NOT guarantee (besides what's computationally infeasible)? Is there ...
2
votes
0answers
116 views

What is the proof for the inconsistency of impredicaitivity + excluded middle + large elimination in type theory

Why is the combination of impredicativity + excluded middle + large elimination inconsistent in dependent type theory? My understanding of large elimination is I am doing large elimination if I am ...
7
votes
1answer
474 views

Is Church-pentation implementable in Agda?

Inspired by suggestion in this question, I've implemented predicative Church encoding of Peano arithmetic. Exponentiation works fine, unfortunately tetration requires the level of one of the arguments ...
4
votes
1answer
93 views

What's the difference between proving weak normalization and implementing evaluator?

Implementing an normalization (cut elimination) procedure for a type system A in a language with a total type system B, automatically proves cut elimination for type system A since the implementation ...
1
vote
0answers
152 views

Is it possible to type Ackermann function with (stratified variant of) System F?

I was surprised to find no open-source implementation of Ackermann function in pure System F as an illustrative example. I finally managed to implement it myself in Haskell using Church encoding: <...
2
votes
1answer
64 views

Does an initial algebra for a class have to belong to the class itself?

In the context of algebraic data types, a concept of initial algebras is usually defined, e.g., in the following way: An algebra $S$ is initial in a class $C$ of algebras iff for every $A\in C$ ...
8
votes
1answer
214 views

Avoiding Cycles with Unification and Subtyping

Context I realize that subtyping often doesn't admit principle types, and that inference in the presence of subtypes is undecidable. I'm working in a context where typechecking should simply fail ...
3
votes
1answer
320 views

What exactly is “large elimination”?

I'm studying type theory (mostly Coq) and often encounter the term "large elimination", usually when talking about type universes hierarchy consistency, for example: impredicative polymorphism + ...
13
votes
1answer
243 views

What makes a language (and its type-system) capable of proving theorems about its own terms?

I've recently attempted to implement Aaron's Cedille-Core, a minimalist programming language capable of proving mathematical theorems about its own terms. I've also proven induction for λ-encoded ...
15
votes
0answers
173 views

Using Dependent Type Theory for Categories that are not LCCC

I have recently been working with polynomial functors and monads based mostly on Gambino-Kock. There they define polynomial functors in a Locally Cartesian Closed Category (LCCC) and extensively use ...
10
votes
1answer
229 views

Cantor's theorem in type theory

Cantor's theorem states that For any set A, the set of all subsets of A has a strictly greater cardinality than A itself. Is it possible to encode something like this using only types / ...
3
votes
4answers
281 views

Philosophy behind monotonicity requirement for inductive types

Is there a good philosophical reason for why inductive types with negative occurrences or non-monotonicity should not be considered valid constructions? According to my understanding of the Bishop/...
0
votes
1answer
103 views

Language/type system closest to Haskell without general recursion

I've implemented a completely functional DSL, and now I'd like to reason about it. It would be helpful to be able to compare it to existing languages. The type system is parametric polymorphic with ...
1
vote
1answer
129 views

What is the coproduct: A + A? [closed]

In the HoTT book, it is said The type of booleans 2 : U is intended to have exactly two elements. It is clear that we could construct this type out of coproduct and unit types as 1 + 1. I don't ...
4
votes
0answers
451 views

Is it possible to derive induction by extending CoC with recursion?

Suppose we extended the CoC with primitive recursion; that is, we added a term µ x . t such that equality allowed unrolling recursive terms: ...
5
votes
1answer
628 views

What is the difference between System F and Hindley-Milner type system?

Hindley-Milner type system is some restriction of System F, which allows type inference. But from simple descriptions I cannot see, what is the difference between them?