Questions tagged [type-theory]
Type structure is a syntactic discipline for enforcing levels of abstraction.
403
questions
2
votes
1
answer
117
views
Derivability of `Vector` in pure calculus of constructions
I am learning pure type systems to better understand functional (and general) programming.
My question arises mainly from the two facts:
It is known that we can define (co)inductive types in pure ...
3
votes
2
answers
154
views
Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?
This question is about using relational parametricity to resolve practical questions in pure functional programming in System F.
Consider the following type of polymorphic functions:
$$T = \forall a. ...
2
votes
1
answer
72
views
What Pure Type Systems have dependent types
What precisely are dependent types? Is it a syntactic property of some type system? This seems to suggest that dependent types are defined through phase distinctions. For example, if a variable is ...
2
votes
2
answers
200
views
Generalizations, or extensions of W-types in MLTT
I'm interested in making a very stripped down implementation of MLTT, or possibly HoTT or cubical type theory (though I've yet to grok the glue rule in cubical type theory and both it and composition ...
4
votes
2
answers
208
views
Denotational semantics of intersection types
Is there a denotational (possibly, domain theoretic) semantics of intersection types? If yes, could you provide some references?
Let me try to give some context to my question. In the usual ...
2
votes
0
answers
42
views
Why use A-normal form in type systems and program verification systems?
In the literature of refinement type systems and program logics, I've observed that many authors choose to confine the programs under consideration to A-normal form. For context, A-normal form ...
2
votes
1
answer
141
views
Power of existential types
It is well known that simply typed lambda calculus becomes much more expressive if you allow universal types, as in Girards system F. Thus, for example, you can encode the booleans as forall a. a ->...
7
votes
3
answers
616
views
Example of a term in system F which is not typable in the simply typed lambda calculus
What is the simplest possible example of a (correctly typed) term in system F that does not correspond to any correctly typed term in the simply typed λ-calculus?
More precisely, I am looking for a ...
10
votes
1
answer
874
views
Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic
Reading Barendregt's chapter “Lambda Calculi with Types” in the Handbook of Logic in Computer Science (vol. 2: Computational Structures) (Abramsky, Gabbay & Maibaum eds., 1992) I learned (op. cit. ...
4
votes
0
answers
65
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 ...
1
vote
0
answers
82
views
Is the Category of $(* \to)^n *$-kinded types freely generated from the discrete graph with $n$ nodes?
In Introduction to Higher Order Categorical Logic part 1, section 4, Lambek defines an adjunction between $\mathbf{Graph}$, the category of graphs and graph homomorphisms, and the category of ...
10
votes
0
answers
266
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 ...
2
votes
3
answers
345
views
How to prove `(∀(M : Monad). ∀a. a → M a) ≅ 𝟙`
Just like the title says, how to prove that equation? The equation basically says that there is only one function a -> M a parametric in both ...
8
votes
1
answer
300
views
Is is true that every monad transformer is equivalent to its underlying/base monad?
Question originally asked in proofassistants.stackexchange
Just like the title says, is it true (in some sensible model)? And if so, how to prove it? Something tells me it should be true and higher-...
0
votes
0
answers
52
views
Product types: algebraic structure for modeling product types with commutative and associative product operation
Is there a known algebraic structure over set of Types (however they are defined) which is equipped with:
commutative and associative product operation for building product types from simpler types, ...
7
votes
1
answer
193
views
Can you regain the Church-Rosser property in languages with continuations?
I'm aware that if you naively add continuations to a language, the Church-Rosser property no longer holds. For example, suppose we have some variant of the STLC with basic arithmetic and integer types....
3
votes
1
answer
72
views
Is Linear Evaluation Parametric?
Parametric functions satisfy free theorems which state that they take related arguments to related results. This is formalized by the notion of parametric transformation introduced in section 5 of ...
1
vote
2
answers
184
views
How is runtime downcasting modeled in type theory?
I'm trying to reconcile two opposing viewpoints I have relating to runtime type introspection and whether or not it is a type-safe operation or how that is modeled in type theory.
Suppose I have types ...
1
vote
1
answer
158
views
What is an efficient algorithm to check for equivalence on symmetric interaction combinators?
Symmetric interaction combinators are a graph-rewriting model of deterministic computation derived from Lafont's interaction nets. In the paper "Observational Equivalence and Full Abstraction in ...
3
votes
1
answer
183
views
Is there an efficient algorithm to check for duplicator-invariant equivalence on symmetric interaction combinators?
Consider the 3 symmetric interaction combinator nets below:
Despite being different nets, they are equal, in the sense that, if we view white nodes as lambdas and applications, and black nodes as ...
14
votes
4
answers
2k
views
Where is the model theory in programming language theory?
I have a background in mathematical logic and am trying to learn some programming language theory. In the syntax of, say, first-order logic, one of the first distinctions you learn about is between ...
1
vote
1
answer
230
views
Type of the Recursor in Lean
I need some help working through the type of the recursor, the eliminator for the inductive type. If
$F=\forall a::\alpha.\mathsf{U}_\ell$
$P=\mu t:F.K$
$K=\sum_c(c:\forall b::\beta.tp[b])$
$u::\...
-1
votes
1
answer
79
views
Typing rule for corresponding `val` and `let` bindings
$\newcommand{\clet}{\texttt{let }}
\newcommand{\cval}{\texttt{val }}
\newcommand{\cin}{\texttt{ in }}
$I have the syntax for a programming language containing both let-bindings of the form $\clet x = ...
1
vote
1
answer
91
views
Intuition behind UTT's internal logic
The "internal logic" of type theory UTT is defined in LF as follows:
What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - ...
1
vote
1
answer
135
views
Formulation of Tarski-style universes in LF
Lately I've been asking questions on type theory on MSE, and I've been getting great answers, but I decided to give a try to this site and see if it will be helpful as well.
I'm looking at this note ...
5
votes
2
answers
332
views
Lambda-calculus: Beta-equivalent terms have the same type
In the simply-typed lambda calculus, how do you prove that: If two terms are beta-equivalent, then they have the same type?
My guess is that I should use the subject reduction, and maybe the ...
4
votes
1
answer
160
views
Free type variables in Hindley-Milner type inference
I'm trying to understand how generalization works in H-M type inference. In order to generalize a function, we:
Collect all the free type variables in the type of the function body,
Subtract away any ...
6
votes
0
answers
114
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 ...
7
votes
1
answer
231
views
Stronger "induction" principles than induction-recursion
Are there type theories in the literature with "induction" principles stronger than induction-recursion? This answer gives System F as an example of a theory stronger than MLTT + induction-...
7
votes
1
answer
380
views
The precise definition of Normalization By Evaluation?
The Wikipedia article suggests that NbE is a technique for obtaining "the normal form of terms" by translating the object language into abstractions of the meta (host) language:
The ...
1
vote
0
answers
69
views
Interpretation of the degree of a redex
In Girard Proofs and Types, The degree of a type is defined as follows
$$\begin{align*}\partial(T_i)&=1\text{ if }T_i\text{ is atomic}\\\partial(U\times V)=\partial(U\rightarrow V) &=\max(\...
5
votes
1
answer
303
views
Dependent type theory and definitions of cumulativity
Many dependent type theories employ an universe hierarchy to compensate for the fact that Type : Type is inconsistent (due to Girard's paradox). A cumulativity relation is then defined to lift terms ...
2
votes
0
answers
147
views
How to implement the next type inference algorithm?
Here I mean only simple typed Lambda calculus / Combinatory logic.
Notation: Combinatory logic terms: $F, X_i, Y_i$. Term application: $(F*X_1)$. Type variables $x_i,y_i$. Type assignment: $X:x_i$.
...
3
votes
1
answer
167
views
Exposition of categorical models of type theory from type-theoretic perspective
Are there any formalizations or expositions of categorical models from type theoretic point-of-view? What I have in mind to get a better grasp of categorical models of dependent types, treating ...
3
votes
1
answer
194
views
How far is the distance between Mahlo Universe and Mahlo Cardinal?
There seems to be some literature stating that Mahlo Universe[1][2] is the counterpart of Mahlo Cardinal in type theory, but I don't fully understand this point of knowledge.
More explicitly, I would ...
1
vote
1
answer
194
views
Defining normalization with respect to judgmental equality instead of reduction
In type theory with a type $\mathbb{N}$ of natural numbers (or some other base type such as booleans) and judgmental equality instead of reductions, canonicity is a meta-theoretical statement claiming ...
2
votes
0
answers
129
views
Why Multiple Clocks in Guarded Dependent Type Theories?
The main purpose of clocks in guarded type theories (originating in Atkey & McBride ICFP 2013) is so that we can define coinductive constructions from guarded recursive definitions.
Semantically ...
10
votes
0
answers
189
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 ...
0
votes
1
answer
112
views
Is there a type theory system which includes an Any type
It's been a while since I read any type theory, so this might sound kind of dumb.
Anyway, if I look at examples of type systems, they all seem to be based around having an empty type, and then ...
5
votes
2
answers
188
views
Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories
In Atkey & McBride ICFP 2013, they extend a simple type theory with guarded recursion indexed by clock variables $\triangleright^k$ and a clock quantification $\forall k. A$ that conveniently ...
2
votes
2
answers
409
views
What is the computational power of the Calculus of Constructions?
The calculus of constructions (CoC) without fix is clearly not Turing complete, as the program that loops infinitely cannot be expressed in it. What I'm wondering: ...
2
votes
1
answer
79
views
Question about "Free-ness" of Free SCWF
In Category with Family by Castellan et al., they introduce the concept of Free SCWF as correspondence of STLC with base type. Seemingly, they define Free B-SCWF as the synonym of initial B-SCWF.
My ...
1
vote
1
answer
69
views
Question in relating STLC and Free CCC
In Lambek's Intro to Higher Order Cat Logic, Chapter 1 Section 4 introduces the free construction (upon graph)
My question is, if I want to have STLC + (fake/incomplete) boolean type, how do I have ...
0
votes
0
answers
130
views
Boolean logic: What is the name of this trick to replace explicit negations by implications?
Consider a Boolean circuit $C$ composed of some finite set of input variables $A_1,\ldots, A_n$ and the connectives $\lor\land\neg\rightarrow$ (with $X\rightarrow Y=\neg X\lor Y$) (update: assume that ...
0
votes
0
answers
87
views
Type theory: Eliminating callback functions?
Consider a type theory such as the one developed in Chapter 1 of the HoTT book, or similar. In fact, I am currently only interested in the types that can be constructed from a collection of elementary ...
0
votes
0
answers
66
views
What does impredicativity mean in substructural and co-intuitionistic logics?
Predicative foundations puts restrictions on power sets and function sets.
Entirely apart from the philosophy predicative theories are a lot easier to prove things about and this sounds interesting to ...
5
votes
1
answer
333
views
How do we use directed univalence in directed type theory?
In directed type theory of Riehl and Shulman, we have a new type, $hom_A\:x\:y$ representing arrows between elements $x$, $y$ of type $A$, note that these are not a priori functions.
I will call the ...
6
votes
1
answer
203
views
Is there a way to define dependent types without explicit substitutions internally within agda?
I am playing around the Programming Language Foundations in Agda exercises and wondering if we can achieve the same level of theories with dependent types. With simple types, the definition usually ...
11
votes
2
answers
581
views
Induction-recursion in models other than $\mathbf{Set}$
It is well-known that various flavors of induction-recursion are consistent*. Typically, this is proven by showing that the standard model of type theory in sets can be extended to include induction-...
8
votes
3
answers
751
views
What's the logical counterpart to jumps with arguments on CPS terms?
It's well known that the CPS (continuation-passing style) translation often employed in compilers corresponds to double negation translation under the Curry-Howard isomorphism. Though often the target ...