Questions tagged [type-theory]

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

78 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
17 votes
0 answers
272 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 ...
Max New's user avatar
  • 1,675
14 votes
0 answers
425 views

Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
MaiaVictor's user avatar
  • 3,137
12 votes
0 answers
160 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 ...
hawkeye's user avatar
  • 2,581
10 votes
0 answers
264 views

Is there a text that discusses both the “lambda cube” of pure type theories and Martin-Löf's intuitionistic type theories, and compares them?

I am lost in a maze of twisty little type theories, all different. There are a number of works (textbooks and papers) that discuss pure type theories, and specifically the ones constituting the ...
Gro-Tsen's user avatar
  • 841
10 votes
0 answers
184 views

Stratification of System Fω

I'm wondering if there's any update on this conjecture listed by Urzyczyn from years and years ago (I don't think that's its first appearance), which I'll restate below. System Fω can be stratified ...
ionchy's user avatar
  • 325
10 votes
0 answers
306 views

Model of Coq (pCuIC) in higher toposes?

Can the type theory of Coq (pCuIC) be modeled in all higher Grothendieck toposes? First of all, even the set theoretical model is not complete (e.g. inductive types in Prop). Although, this is ...
Bas Spitters's user avatar
10 votes
0 answers
429 views

Typed Lambda Calculus models and denotations

I'm trying to draw a general mental picture about the models and the denotational semantics of the typed lambda calculus, in its different variants. I'm particularly interested in how the semantics ...
chi's user avatar
  • 668
9 votes
0 answers
204 views

Constructive Strong Normalization of the Extended Calculus of Constructions

The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof ...
helmut's user avatar
  • 375
9 votes
0 answers
522 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 ...
Jake's user avatar
  • 1,183
8 votes
0 answers
140 views

For which type systems have normalizaton proofs been formalized?

I am trying to understand what the open problems are in the area of formalizing proofs of normalization for type systems. Obviously STLC has been done many times. For predicative System F, I found one ...
while1fork's user avatar
8 votes
0 answers
241 views

Which types are nihilistic?

[Note 2020-02-08: I updated the definition of nihilistic types so that it relies less on the type Empty.] A discussion on Twitter prompted the following question, ...
Andrej Bauer's user avatar
  • 28.8k
8 votes
0 answers
440 views

Type inference with subtype constraints and polymorphism using Trifonov and Smith's constraint maps

Trifonov and Smith's Subtyping Constrained Types (1996) introduces constraint maps to represent consistent closed constraint sets (such maps providing sets of lower and upper bounds to each variable ...
sclv's user avatar
  • 1,379
7 votes
0 answers
186 views

$\lambda$-definability and structure preserved by homomorphisms

I imagine there are some standard results that bear on this, but I'm having trouble finding a proof or refutation of it. Some prelimary definitions. A Henkin structure $A = (A^\cdot, ⟦\cdot⟧_A)$ for ...
Andrew Bacon's user avatar
7 votes
0 answers
223 views

Relationship between Pataraia's theorem and inductive-recursive definitions?

Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
Neel Krishnaswami's user avatar
7 votes
0 answers
623 views

How to do Type Inference using an SMT solver?

I understand that Hindley-Milner Type Inference can be implemented using an off-the-shelf SMT (Satisfiability Modulo Theories) solver? How would this work, for example for a very simple type system (...
n00b101's user avatar
  • 369
7 votes
0 answers
293 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 ...
Troy McClure's user avatar
6 votes
0 answers
113 views

List Functions That Don't Depend on Length

Intuitively, a polymorphic function of type $f : \forall a. [a] \to [a]$ cannot inspect the type of its elements. This intuition can be captured formally using either natural transformations or ...
vigenary's user avatar
6 votes
0 answers
122 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 ...
phipsgabler's user avatar
6 votes
0 answers
246 views

Postulating self types in a proof assistant

Self types introduce two typing new rules (simplified): $ \frac{\Gamma \; \vdash \; t : [t/x]T}{\Gamma \; \vdash \; t : \iota x. T}$ I-self and $ \frac{\Gamma \; \vdash \; t : \iota x. T}{\Gamma \; \...
Łukasz Lew's user avatar
  • 1,187
6 votes
0 answers
275 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 ...
Bob's user avatar
  • 381
5 votes
0 answers
224 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 ...
Yasmine Shaorda's user avatar
5 votes
0 answers
589 views

What is the proof for the inconsistency of impredicativity + 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 ...
Petercommand Hsu's user avatar
5 votes
0 answers
258 views

Commonalities and differences between canonical structures and the implicit calculus

There is a paper on The Implicit Calculus as a generalization of type classes. Coq's canonical structures are also a generalization of type classes. The paper does not mention canonical structures ...
Jules's user avatar
  • 390
4 votes
0 answers
64 views

Description of the CPS transformation for the typed lambda-calculus

Is there somewhere a precise but hopefully readable account of how the CPS (=continuation-passing-style) transformation applies to the typed lambda-calculus? (Say, simply-typed with product and sum ...
Gro-Tsen's user avatar
  • 841
4 votes
0 answers
172 views

Model of homotopy type theory where propositional & judgmental equality coincide for closed terms

In intensional Martin-Löf type theory we can prove the metatheorem that two closed terms are propositionally equal iff they are judgmentally equal. Is there a non-empty model of homotopy type theory ...
user avatar
4 votes
0 answers
98 views

Relative consistency of various Martin-Löf style type theories

I am wondering about relative consistency of various Martin-Löf type theories, when compared to one another, I will use MLTT for the intensional Martin-Löf type theory with $\Pi$, $\Sigma$, $\mathbb{N}...
Ilk's user avatar
  • 920
4 votes
0 answers
198 views

What logic do refinement types correspond to?

I'm interested in applicability of refinement types to theorem-proving hence the questions about their logical expressiveness. Let's say, we have a type system which corresponds to some logic ...
oquechy's user avatar
  • 41
4 votes
0 answers
181 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 ...
Olle Härstedt's user avatar
4 votes
0 answers
239 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 ...
Ilk's user avatar
  • 920
4 votes
0 answers
236 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-...
MaiaVictor's user avatar
  • 3,137
4 votes
0 answers
118 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 ...
Joey Eremondi's user avatar
4 votes
0 answers
169 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 ...
Joey Eremondi's user avatar
4 votes
0 answers
521 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: ...
MaiaVictor's user avatar
  • 3,137
4 votes
0 answers
151 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 ...
cody's user avatar
  • 13.8k
4 votes
0 answers
98 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 ...
Andrew Bacon's user avatar
4 votes
0 answers
279 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 ...
Carl Patenaude Poulin's user avatar
4 votes
0 answers
352 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 ...
isekaijin's user avatar
  • 501
4 votes
0 answers
342 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 ...
Konstantin Solomatov's user avatar
4 votes
0 answers
198 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....
Jonas Kölker's user avatar
3 votes
0 answers
95 views

Equality reflection without $\eta$

Are type theories with equality reflection (i.e. having a term of an identity type between two objects allows us to freely swap them) but not the $\eta$-rule for $\Pi$-types interesting? Does function ...
bkrl's user avatar
  • 31
3 votes
0 answers
95 views

Boltzmann sampling for containers/dependent polynomials?

I’d like to randomly sample from dependently-typed data structures. Has anyone looked at extending Boltzmann sampling to containers or dependent polynomials?
Neel Krishnaswami's user avatar
3 votes
0 answers
114 views

Request for an update on a discussion about coinductive types in HoTT (or anywhere else)

Googling something else I stumbled on a conversation titled "coinductives" initiated by Vladimir Voevodsky on Google groups in 2014. It lasted for three days, invloved a dozen people, and ...
მამუკა ჯიბლაძე's user avatar
3 votes
0 answers
135 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 ...
MaiaVictor's user avatar
  • 3,137
3 votes
0 answers
136 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?
bitconfused's user avatar
3 votes
0 answers
156 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 (...
Joey Eremondi's user avatar
3 votes
0 answers
127 views

Equational Theories for Type Systems

I was reading through Gunter's Semantics of Programming Languages: Structure and Techniques and in the second chapter on simply typed $\lambda$ calculus he introduces an equational theory with $\beta\...
Apoorv's user avatar
  • 141
3 votes
0 answers
412 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: ...
Labbekak's user avatar
  • 701
3 votes
0 answers
381 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, ...
MaiaVictor's user avatar
  • 3,137
3 votes
0 answers
118 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 ...
Łukasz Lew's user avatar
  • 1,187
3 votes
0 answers
207 views

Mildly dependently-typed metalanguage for mildly context-sensitive object languages

This is almost certainly not a new idea, but I haven't seen it elaborated or discussed elsewhere. A very natural way to represent the abstract syntax of an object language in a typeful metalanguage is ...
isekaijin's user avatar
  • 501