2022 Developer Survey is open! Take survey.

Questions tagged [type-systems]

The tag has no usage guidance.

91 questions
Filter by
Sorted by
Tagged with
37 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 ...
371 views

"Spurious" Type Equivalences in MLSub/Algebraic Subtyping

I have been reading up on Stephen Dolan's "Algebraic Subtyping" in his PhD thesis and also the ICFP 2020 Paper "The simple essence of algebraic subtyping..." by Lionel Parreaux and ...
• 1,337
45 views

Which is more expensive, structural or nominal type-checking?

A type system is nominal when types can be given new names, and those new names are attached to new behaviors. To me, type-checking programs in a nominal type system seems like it must be no less work ...
• 243
59 views

1 vote
64 views

Properties of the polymorphic type $\Pi t : * . ((t \to t) \to t) \to t$

In the context of pure type systems (say Calculus of Constructions) I am looking for references discussing the properties of the following polymorphic type: $\Pi t : * . ((t \to t) \to t) \to t$. What ...
1 vote
109 views

Is Kotlin's type system Turing complete?

Java's type system is Turing complete. For whatever reason, I was under the impression that Kotlin's type system (for concreteness, let's say the latest version of the language -- ...
159 views

Calculus of constructions: Why forall when pi exists?

I'm studying the calculus of constructions from ATAPL, Chapter 2. I'm trying to understand the Type Equivalence rule, which describes the meaning of the new type family ...
1 vote
139 views

Explicit type system with infinite non-cumulative universe hierarchy

Is there an open-source proof assistant or at least an explicit set of rules written down somewhere for a type system with an infinite non-cumulative universe hierarchy and unique typing? I want to ...
164 views

Defining binary natural numbers without quotient types

Let's say we work in a dependent type theory with W-types and we want to have a type for binary natural numbers. We don't want to add quotient types or higher inductive types to the system. How to ...
142 views

Is the Mendler-encoding in System-F adequate?

In the paper "Efficiency of Lambda-Encodings in Total Type Theory" it is mentioned that the Church-encoding is adequate and the Parigot encoding is not adequate. This means that any ...
• 691
84 views

109 views

Completeness of Constraint Typing (type inference) question regarding $\sigma'$

The theorem of completeness of type inference states the following: Suppose $\Gamma \vdash t:S| _{\mathcal{X}}C$, ...
• 185
625 views

Determinism and pi-calculus

Milner embedded $\lambda$-calculus into $\pi$-calculus, showing that the $\pi$-calculus is capable of Turing-complete, deterministic calculation. Since parallel compositions of processes in the $\pi$-...
• 574
310 views

Recursive types and the empty type

In John Mitchell's book "The Foundations of Programming Languages", he considers a typed lambda calculus with unit, exponential, product, (binary) coproduct types, and arbitrary recursive types (p126)....
• 433
304 views

Efficiently ordering typed programs

Sometimes it is useful to enumerate in increasing order programs that have a given type. A simple example is test generation for compilers: we want to test a new optimising phase and are ...
• 10.3k
293 views

Type checking, Hypothetical judgments, meaning explanations and computational type theory

We say that a system is a computational type theory if it is a type theory defined by not a bunch of inference rules, but some sort of Martin-Löfian meaning explanations (e.g. in the sense of NuPRL). ...
• 777
141 views

How to prove relations between "classes" of types?

After reading Effects as Sessions, Sessions as Effects, I was wondering how would a proof of equivalence between both take place, or even, a proof of Sessions types being a Type and Effect System. In ...
• 181
326 views

Denotational semantics of System $F_\omega$ with recursive types and general recursion

Is there a denotational semantics for System $F_\omega$ in literature that supports both recursive types and general recursion? I'm looking for a model of Ralf Hinze's variant of System $F_\omega$ [4]...
• 161
4k views

How do you get the Calculus of Constructions from the other points in the Lambda Cube?

The CoC is said to be the culmination of all three dimensions of the Lambda Cube. This isn't apparent to me at all. I think I understand the individual dimensions, and the combination of any two seems ...
• 343
149 views

Is there any work relating type systems and Cook-Reckhow proof systems?

An important subfield of computational complexity is proof complexity, mostly due to Cook and Reckhow. E.g. one notable result is that a proof system that has efficient proofs (i.e., in length ...
• 175
377 views

Is there a "lambda cube" for interaction nets?

The lambda calculus is an untyped language that is often extended with logical frameworks such as the vertices of the λ-cube. Is there something similar to it, but for interaction nets? What about ...
• 3,045