Questions tagged [type-theory]

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

Filter by
Sorted by
Tagged with
4
votes
0answers
135 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 ...
3
votes
1answer
145 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",...
-2
votes
0answers
34 views

Escape analysis as ownership inference

Escape analysis will let you know if a variable can escape its current scope. Do you think this would be usable together with ownership inference, where only the owner is allowed to modify a variable'...
2
votes
2answers
84 views

What is the relation of HOL Light type theory and some of the intuitionistic type theories?

I'm trying to understand how HOL Light deductive rules relate to mainstream intuitionistic type theories. Here is a sample of questions that come to my mind. Does ...
4
votes
1answer
68 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 ...
3
votes
0answers
101 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 ...
6
votes
1answer
122 views

What arithmetical theorems can plain $\lambda \Pi$ reason about?

I've read that System F cannot state or prove theorems of the First Order Theory of Arithmetic. I assume this is because we lack dependent types, so we cannot explicitly express $\forall n:\mathbb{N}....
2
votes
1answer
126 views

Defining finite sets inductively in a proof assistant?

To represent finite sets within coq, we either use something like ListSet, which are just definitions on top of list, or we ...
6
votes
0answers
119 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 \; \...
3
votes
0answers
124 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?
5
votes
1answer
74 views

Decidability of rank-k polymorphism vs. System F

There's a paper by Kfoury from 1992, "Type Reconstruction in Finite Rank Fragments of the Second-Order $\lambda$-Calculus", that proves that type inference for Curry-style rank-$k$ polymorphic lambda ...
4
votes
0answers
114 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
1answer
475 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: ...
0
votes
0answers
56 views

Sample Terms in System Omega

I've been implementing mini languages that fall into each corner of the Lambda Cube. My main reference for this has been Types and Programming Languages. The latest one I finished is System Omega. I ...
2
votes
1answer
160 views

Non-termination, strict positivity and free monads

Using the standard encoding of a free monad in Haskell and its fmap instance: ...
2
votes
1answer
143 views

From Church-encoding to induction principle

I am looking for an algorithm to go from a Church-encoded datatype to their induction principle in the Calculus of Constructions. For example: ...
1
vote
1answer
118 views

Extensional type theory and function extensionality

Is the principle of function extensionality $ (\forall x. f(x) = g(x)) \implies f = g$, derivable from ETT? Most notably is this derivable in Agda with axiom K?
7
votes
0answers
188 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, ...
5
votes
1answer
119 views

Semantic definition of strict positivity for a functor

If we consider a definition of recursive type as: F : Type -> Type; T = fix F; It is customary to talk about the functor F ...
3
votes
1answer
105 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
0answers
130 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 (...
2
votes
0answers
105 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\...
5
votes
1answer
232 views

Applications of Barendregt–Geuvers–Klop conjecture

I was learning about type systems from Benjamin C. Pierce's Types and Programming Languages and came across the Lambda cube in the chapter on Higher-Order Polymorphism. After reading up more about it ...
4
votes
0answers
128 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 ...
0
votes
1answer
92 views

What is the role of “universe” types in intuitionistic type theory?

According to the Wikipedia article on intuitionsitic type theory: The universe types allow proofs to be written about all the types created with the other type constructors. Every term in the ...
4
votes
0answers
129 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 ...
1
vote
1answer
141 views

Extended Church's thesis and internal parametricity

I am wondering if there is any known relationship between these 2 concepts in intensional MLTT as formulated here. Does $Internal\ parametricity \implies ECT$ hold? For forumlation of ECT see https://...
1
vote
1answer
130 views

Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook

I am working through the Dependent Types chapter from Advanced Topics in Types and Programming Languages (ATTAPL) by Benjamin Pierce et al. I am confused with the calculus presented Fig 2-7 (Calculus ...
0
votes
0answers
63 views

Proposition terms vs types in Coq

Consider the following div function written in Coq. It takes in a proof that the divider is non-zero. Definition div (n d:nat) (pf: ~(d = 0)) := n/d. Focus on <...
6
votes
2answers
160 views

How to define list zipping categorically/inductively?

Lists and fixpoints The type of $A$-lists is defined as $\mu F_A$, where $F_A(X) = 1 + A \times X$ is the "cons-or-nil"-functor and $\mu$ is the least fixpoint operator. In Haskell syntax, this would ...
8
votes
1answer
395 views

PHOAS with extrinsic typing?

Parameterized Higher Order Abstract Syntax (PHOAS) is a representation of syntax trees that allows the host language's binding to be used to represent binding in the language being modelled, while ...
5
votes
2answers
176 views

What's the point of stack judgement in CBPV?

Call-by-push-value (CBPV) introduces two main families of types, values and computations, and their corresponding judgements. However, in some extensions/variants/adaptation of CBPV, there is a third ...
3
votes
0answers
111 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: ...
6
votes
1answer
262 views

Fixed set of type constructors to simulate all intensional inductive families?

I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction ...
6
votes
1answer
185 views

Structural equality of Pi Types with heterogeneous equality?

I'm trying to implement a proof of the following type: ...
4
votes
0answers
181 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-...
8
votes
1answer
223 views

Type-theoretic interpretation of Skolemization

What is the type-theoretic interpretation / equivalent of Skolemization? Skolemization converts some formula into Skolem normal form. The two formulae are equisatisfiable with each other. Or, to say ...
9
votes
0answers
198 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 ...
5
votes
1answer
140 views

Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?

To perform type inference in the presence of polymorphic recursion, one can use a Kleene-Mycroft iteration to compute the principal type of an expression. To type $\mathsf{fix}\ f\ldotp e$, we define $...
4
votes
2answers
295 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 ...
3
votes
1answer
120 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 ...
21
votes
3answers
3k views

Why colon to denote that a value belongs to a type?

Pierce (2002) introduces the typing relation on page 92 by writing: The typing relation for arithmetic expressions, written "t : T", is defined by a set of inference rules assigning types to ...
9
votes
2answers
423 views

Applications of algebraic geometry in type theory/programming language theory

Lately, I have become interested in algebraic geometry and have started reading on it. I still know very little about this field, but I do want to know if it has any connection with my main field, ...
8
votes
1answer
225 views

Can Isorecursive types capture mutually recursive data types?

I've been reading TAPL, and reached the section on recursive types. I understand the type operator $\mu$. For example, the two type expressions are equivalent ...
10
votes
2answers
291 views

Intuition Behind Strict Positivity?

I'm wondering if someone can give me the intuition behind why strict positivity of inductive data types guarantees strong normalization. To be clear, I see how having negative occurrences leads to ...
6
votes
1answer
171 views

What will go wrong if a recursive record type has a negative eta rule?

In the context of Agda like dependent type theory: This short paper https://jesper.sikanda.be/files/vectors-are-records-too.pdf says some inductive type can be seen as records, for example ...
3
votes
2answers
268 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 ...
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/...
0
votes
1answer
128 views

Definitional equality of recursive function definition by “infinite unfolding”

The context is checking definitional equality in dependent type theory implementations. Consider in Coq ...
4
votes
0answers
97 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 ...

1
2 3 4 5 6