Questions tagged [type-theory]
Type structure is a syntactic discipline for enforcing levels of abstraction.
261
questions
5
votes
2answers
151 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
76 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
232 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
158 views
Structural equality of Pi Types with heterogeneous equality?
I'm trying to implement a proof of the following type:
...
4
votes
0answers
163 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
178 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
153 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
110 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
216 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
106 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 ...
19
votes
3answers
2k 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
295 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, ...
7
votes
1answer
146 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
204 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
137 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 ...
