Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [type-theory]

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

Filter by
Sorted by
Tagged with
0 votes
1 answer
91 views

What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?

In what books or papers is it explained how the type constructions of a functional programming language correspond to category theory, and what are the models (a rigorous semantics) of programs of ...
2 votes
1 answer
78 views

What are some practical applications of inductive-inductive and inductive-recursive types?

Since this question got not many answers Im hoping asking again could convey that this has some importance. Anyway so in undergraduate education, I was working on research to implement dependent-...
1 vote
1 answer
92 views

Formalising Church numerals in Agda

Beginer here. I'm trying to show that the closed $\beta$-nf's of type $ (\iota \to \iota) \to (\iota \to \iota) $ are the Church numerals ($\iota$ the base type, using the simply-typed lambda calculus)...
3 votes
3 answers
189 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. ...
14 votes
3 answers
893 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
3 answers
370 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 ...
3 votes
1 answer
216 views

How to encode a function from an existential type

I am having trouble using parametricity to show that existential types work in System F (or System Fω) in the way one would expect them to work. It is known that an existential type $\exists t.~P~t$ (...
1 vote
1 answer
188 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 ...
11 votes
4 answers
1k views

Explaining monad transformers in categorical terms

Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers. How could monad transformers be described in the terms ...
2 votes
1 answer
121 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 ...
4 votes
2 answers
216 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
1 answer
76 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 ...
3 votes
1 answer
211 views

Are uniqueness rules converse to introduction rules?

I've seen many people connecting introduction rules and elimination rules, saying that they're dual notion. Indeed, like in the categorical model, these rules are symmetric morphisms. However, if we ...
3 votes
2 answers
213 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 ...
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
164 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
647 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
891 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
81 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 ...
1 vote
2 answers
186 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 ...
10 votes
0 answers
294 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 ...
8 votes
1 answer
308 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
53 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
198 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
75 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 ...
3 votes
1 answer
188 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
243 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::\...
10 votes
1 answer
611 views

A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?

Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a ...
2 votes
1 answer
438 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 ...
-1 votes
1 answer
84 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 = ...
4 votes
1 answer
184 views

What is the relation of parametricity and function extensionality?

In Agda function extensionality can be defined like this: funExt = {A : Set} {B : Set} {f1 f2 : A → B} → (∀ x1 x2 → x1 ≡ x2 -> f1 x1 ≡ f2 x2) → f1 ≡ f2 One may ...
1 vote
1 answer
94 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
141 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 ...
14 votes
3 answers
2k views

Type system based on naive set theory

As I understand, in computer science data types are not based on set theory because of things like Russell's paradox, but as in real world programming languages we can't express such complex data ...
5 votes
2 answers
350 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 ...
3 votes
1 answer
201 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 ...
4 votes
1 answer
177 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
1 answer
659 views

Strong normalization property of CoC inside CoC

Wikipedia says that The CoC is strongly normalizing, although, by Gödel's incompleteness theorem, it is impossible to prove this property within the CoC since it implies inconsistency. Why is ...
21 votes
1 answer
2k views

Why it's impossible to declare an induction principle for Church numerals

Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way: ...
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 ...
5 votes
2 answers
189 views

Relating functors to relational functors with the parametricity translation

$\newcommand{\Type}{\text{Type}}\newcommand{\id}{\text{id}}\newcommand{\map}{\text{map}}$ In attempting to answer the question: Rigorous proof that parametric polymorphism implies naturality using ...
20 votes
4 answers
2k views

How can relational parametricity be motivated?

Is there some natural way to understand the essence of relational semantics for parametric polymorphism? I have just started reading about the notion of relational parametricity, a la John Reynolds' ...
7 votes
1 answer
245 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-...
9 votes
2 answers
2k views

What exactly is "large elimination"?

I'm studying type theory (mostly Coq) and often encounter the term "large elimination", usually when talking about type universes hierarchy consistency, for example: impredicative polymorphism + ...
12 votes
1 answer
5k views

Why study type theory?

After reading the literature on type theory (especially the constructive kind - CTT) I'm left wondering "why" should one study type theory, specifically within the confines of "computing" in general? ...
7 votes
1 answer
411 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 ...
11 votes
1 answer
315 views

reference request: deciding validity of higher-order quantified boolean formulas is not Kalmar-elementary

$\newcommand\iddots{⋰}$In "A simple proof of a theorem of Statman" (TCS 1992), Harry Mairson gives a simple proof of Statman's result that deciding $\beta\eta$-equality of terms in simply typed lambda ...
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(\...

1
2 3 4 5
9