Questions tagged [type-theory]

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

Filter by
Sorted by
Tagged with
4
votes
1answer
477 views

Church-style CoC with axiom for induction over Church-encoded unit, is it consistent?

If we start with the Calculus of Constructions, and then use the following definitions for the Church-encoded Unit: ...
4
votes
1answer
439 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}$. ...
4
votes
1answer
203 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, ...
4
votes
1answer
130 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 ...
4
votes
1answer
69 views

Why REFL rule is primitive in HOL Light?

HOL Light assumed REFL as a primitive. Why does it need to do so? Can't REFL rule be deduced in this way using ...
4
votes
1answer
133 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/...
4
votes
1answer
167 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
2answers
307 views

How do continuations represent negations (under the Curry–Howard correspondence)?

Under the Curry–Howard correspondence, types can be thought of as propositions, and values inhabiting a type can be thought of as proofs that the corresponding proposition is true. (E.g., the ...
4
votes
1answer
251 views

Is it possible to verify a typechecker for a total dependently-typed language in that language's logic?

I understand the diagonalization argument against implementing an eval function in a total language, and that typechecking in a dependently typed language requires ...
4
votes
1answer
415 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 ...
4
votes
1answer
127 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 ...
4
votes
1answer
114 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: ...
4
votes
1answer
521 views

Generalization and instantiation of types in Hindley-Milner type inference

I’m currently reading Heeren, B., Hage, J., & Swiestra, D. (2002). Generalizing Hindley-Milner Type Inference Algorithms in an attempt to understand Hindley-Milner-style type inference. I'm ...
4
votes
0answers
149 views

Is full ownership inference possible?

Rust is famous for its ownership type-system, but requires the programmer to annotate ownership in function signatures. Is it possible to do full program inference of ownership, without any ...
4
votes
0answers
117 views

Rules between UIP with function extensionality and univalence

I am wondering if there are any interesting rules/judgemental equalities, denoted $A$, which satisfy the following properties: $iMLTTfe+UA \implies \neg A$ $iMLTTfe+UIP \implies \neg A$, or more ...
4
votes
0answers
133 views

On the interpretation of coinduction in type theory

The notion of (co)datatype can be modeled satisfactorily in category theory as fixed-points of polynomial functors. Then, (co)induction principles are derived from initial algebras/terminal ...
4
votes
0answers
142 views

Implementations of Dependent Type Theory

I am trying to find a minimal implementation of dependent type theory that supports Pi Types (obviously) Modules containing records Inductive data types Universe Hierarchy A notion of equality ...
4
votes
0answers
182 views

Is my understanding regarding how to implement Quotient Types correct?

I was trying to understand Quotient Types, and determine if Self-Types can be used to implement them. From a Reddit post, Here is an example and explanation that may be more familiar to non-...
4
votes
0answers
98 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 ...
4
votes
0answers
138 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 ...
4
votes
0answers
470 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: ...
4
votes
0answers
126 views

Completeness of realizability semantics for higher-order type theory

In this answer I mention a paper by Geuvers in which he describes a class of models for a type theory $\lambda P_2$ which is a sub-system of the CoC and roughly corresponds to 2nd order predicate ...
4
votes
0answers
78 views

Coherence spaces and full completeness for the implicative fragment of linear logic

Linear logic isn't complete for coherence space semantics since $1$ and $\top$ get identified. But it is, I believe, complete for the fragment of linear logic whose only connective is $\multimap$. I ...
4
votes
0answers
252 views

Modeling union types using sum types

It is trivial to model sum types using only union types and product types: simply add a discriminant. $A + B \cong (0 \times A) \cup (1 \times B)$. What I am wondering is whether or not there is a ...
4
votes
0answers
275 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
0answers
311 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 ...
4
votes
0answers
193 views

Type-and-effect systems, stochasticism and effect squelching: how about quicksort?

There's a feature of Haskell's type system which bugs me: you can't implement a randomized sorting algorithm without the use of randomness spilling out into all of its callers. That seems undesirable....
3
votes
4answers
318 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/...
3
votes
2answers
342 views

Type a variable-argument function?

Is it possible to type a variable-argument function? EDIT: like those defined in Scheme.
3
votes
3answers
210 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, <...
3
votes
2answers
278 views

Extending Hindley-Milner to type mutable references

I have been trying to implement a programming language from scratch, and have gotten reasonably far. It reads just like Python, other than the fact that let is used ...
3
votes
4answers
310 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 ...
3
votes
2answers
130 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
2answers
343 views

Confusing (to me) statement from “Type Classes in Haskell”

I'm reading up on type classes, and started looking at the paper Type Classes in Haskell. In Section 2.2 - Superclasses, the authors use the following example: ...
3
votes
1answer
170 views

Why would the term “dynamically typed” be considered a misnomer?

In the book "Types and Programming Languages", the author writes: The word "static" is sometimes added explicitly - we speak of a "statically typed programming language",...
3
votes
1answer
122 views

Verified type checkers

Most of the work on programming language metatheory mechanization focus on the declarative properties of the languages (e.g., type soundness), but fail to address the algorithmic side, i.e. the type ...
3
votes
1answer
144 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 ...
3
votes
1answer
144 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 ...
3
votes
2answers
163 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 ...
3
votes
1answer
581 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. ...
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 ...
3
votes
1answer
107 views

Type of induction principle for fixpoint types

To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F is a ...
3
votes
1answer
316 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 ...
3
votes
1answer
196 views

Decidability in Extensional Type Theory

What are the ways in which one can add a decidable equivalence relation in a type system with undecidable type checking/extensional equality?
3
votes
0answers
66 views

Is there a known notion of “stochastic dependent pair”?

I came upon this when thinking about the semantics of probabilistic programs. Say you have a generative model N ~ Poisson() for n = 1:N X[i] ~ Normal() Then the ...
3
votes
0answers
106 views

Would it be possible to derive `transp` natively from Path, Interval and typecase?

Assume for a moment that we extended Agda with an Interval and a Path type, but not transp (which is a primitive currently). I'm ...
3
votes
0answers
128 views

Weakest model of computation that can typecheck?

What's the weakest (known) model of computation (or smallest language class) that can decide whether a simply-typed lambda calculus program type checks? What about an (explicitly typed) CoC program?
3
votes
0answers
132 views

Set:Set or Negative Inductives in a Total Language?

In total dependently typed languages, general recursion is forbidden, since this can allow for non-terimination. However, dependently typed language can still describe Turing-complete computations (...
3
votes
0answers
119 views

Is System-F with higher-kinded newtypes equivalent in computational power to System-F omega?

If we have System-F with higher-kinded types and newtypes, then we can express everything (I think) of System-F omega, except we have to manually (un)pack. For example: ...
3
votes
0answers
160 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, ...