Questions tagged [type-systems]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0
votes
1answer
132 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
2answers
110 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 ...
3
votes
1answer
149 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 ...
7
votes
2answers
819 views

Free theorems, where?

I've found this webapp which lets you generate a free theorem for a given type. The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of which ...
5
votes
1answer
118 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 ...
0
votes
1answer
63 views

Pi-calculus (or session types) - proof for weakening lemma

I'm writing a thesis about session types and am currently writing a section concerning type soundness for the system. I started to proof weakening lemma, which states, that $$ \text{If } \Gamma \vdash ...
7
votes
2answers
202 views

Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?

It is well known that any CCC (cartesian closed category) is a model of the simply-typed $\lambda$-calculus. It is less well known that System F admits a categorical model, but it is also well studied ...
3
votes
1answer
201 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
143 views

Types as abstract interpretations

In Types as Abstract Interpretations, Cousot seems to propose a method to derive various type systems by succesive abstract interpretation of the denotational semantics of an untyped lambda-calculus. ...
6
votes
0answers
109 views

Programmatic higher inductive/inductive-inductive types with equalities between equalities

I can think of practical HITs in verified software that capture some form of alpha equivalence, context equivalence or the example which defines well-typed syntax of type theory from Signatures and ...
3
votes
0answers
146 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 (...
8
votes
1answer
451 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
207 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
228 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: ...
7
votes
1answer
179 views

Example of a function that you can write in Calculus of Constructions but not in System-F

It's been suggested in an answer to this question that the Calculus of Constructions has more computational strength than System-F. What are examples of functions that you express in CoC that you ...
2
votes
1answer
283 views

Difference between statically and dynamically typed languages

When writing a course on computer science where students get an introduction to both Python and OCaml, I was on the verge of saying that Python is dynamically typed and OCaml is statically typed. I ...
7
votes
2answers
299 views

Termination checking for Scott-encodings in System F with positive-recursive types

Is there any research on termination analysis on Scott-encodings in System F with positive-recursive types. All papers I have found use languages with constructors and case analysis (for example ...
11
votes
2answers
442 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 ...
1
vote
1answer
135 views

Dependent C-style types with subtyping rule

I'm looking for previous work regarding an extension of a C-style type system in which types may have constraints and have a defined subtyping rule. In particular, I'm interested in defining algebra-...
-3
votes
1answer
93 views

Soundness of type (systems)

For someone without strong background in theoretical computer science: can soundness be a property of a type (given a type system), or a property of type systems only? In other words, can we say that ...
0
votes
1answer
69 views

Is a reference on T a subtype of T?

If I take the book Practical Foundations for Programming Languages by Robert Harper, the following definition is given for subtyping: A subtype relation is a pre-order on types that validates the ...
12
votes
2answers
2k views

Is compiler for dependent type much harder than an intepreter?

I have been learning something about implementing dependent types, like this tutorial, but most of them is implementing interpreters. My question is, it seems that implementing a compiler for ...
5
votes
2answers
260 views

Typing of substitution in a bidirectional type system

In most typed lambda calculi, we have the following lemma: If $\Gamma \vdash t_1 : \tau_1$ and $\Gamma, x : \tau_1, \Delta \vdash t_2 : \tau_2$ then $\Gamma,\Delta[t_1/x] \vdash t_2[t_1/x] : \tau_2[...
5
votes
1answer
234 views

Complexity of type-checking in relation to complexity of normalization

In order to verify that a terminating program terminates, one thing that can be done is to actually run the program. That may take a lot of time. If the program is typed in a total type-system, we can ...
7
votes
1answer
480 views

Fixed points in dependent type theories

Most dependent type theories aim for some notion of correctness in two respects: The type system must be decidable. The type system must be consistent. e.g. $\forall \tau. \tau$ should not be ...
1
vote
2answers
460 views

What are the limitations of dependent typing?

It seems dependent types can provide lots of desirable guarantees about program behavior. What kinds of program properties can they NOT guarantee (besides what's computationally infeasible)? Is there ...
34
votes
3answers
2k views

Type classes vs object interfaces

I don't think I understand type classes. I'd read somewhere that thinking of type classes as "interfaces" (from OO) that a type implements is wrong and misleading. The problem is, I'm having a problem ...
15
votes
4answers
632 views

Unary parametricity vs. binary parametricity

I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( https://dl.acm.org/citation.cfm?id=2359499). In this paper, they internalize unary ...
11
votes
1answer
479 views

Dependent types over Church-encoded type in PTS/CoC

I'm experimenting with pure type systems in Barendregt's lambda cube, specifically with the most powerfull one, the Calculus of Constructions. This system has sorts ...
5
votes
1answer
169 views

What's the difference between proving weak normalization and implementing evaluator?

Implementing an normalization (cut elimination) procedure for a type system A in a language with a total type system B, automatically proves cut elimination for type system A since the implementation ...
3
votes
1answer
140 views

Is there a 'very fast growing' hierarchy that would capture System F?

Particular ordinals in slow-growing and fast growing hierarchies can capture the expressiveness of many predicative type systems. Is there a hierarchy of function that could possibly capture ...
2
votes
1answer
176 views

Is there a formalization of normalization of impredicative system F?

In particular Agda seems not strong enough to prove that. Is the predicative Calculus of Inductive Constructions universes (Coq without Prop) sufficient? How about with the impredicative Prop?
1
vote
0answers
56 views

Effect handlers, arrows and applicatives

After reading Lindley's paper on effect handlers for arrows and applicatives, I got the gist about dynamic and static flow and that it was added to the effect system and so on. However, I do not ...
7
votes
1answer
334 views

Avoiding Cycles with Unification and Subtyping

Context I realize that subtyping often doesn't admit principle types, and that inference in the presence of subtypes is undecidable. I'm working in a context where typechecking should simply fail ...
5
votes
2answers
349 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 ...
9
votes
1answer
178 views

System F and System T names

Does anyone know where do the names System "F" and System "T" comes from? I am not asking who introduced those names (Girard System F, and Gödel System T), but what the "F" and the "T" means.
2
votes
1answer
397 views

programming language with type-level functions

Is there any programming language out there that allows the same set of tools it offers, to be used at the type level as well? I know, Haskell and some other ML family languages allow parametric types ...
22
votes
2answers
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 ...
4
votes
0answers
63 views

Finite intersection property of polymorphic type families

Let $\Phi$ be a type functor definable in polymorphic lambda calculus: $$ \alpha : * \vdash \Phi(\alpha) : * $$ $$ f : A \to B \vdash \mathsf{Map}^{A,B}_\Phi(f) : \Phi(A) \to \Phi(B)$$ Suppose further ...
2
votes
1answer
101 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$, ...
7
votes
1answer
568 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$-...
5
votes
1answer
296 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)....
7
votes
2answers
300 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 ...
12
votes
3answers
1k 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 ...
7
votes
1answer
275 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). ...
6
votes
1answer
276 views

Forms of types in the calculus of constructions

In the usual presentations of the calculus of constructions (CC) with two kinds Prop and Type such that Prop:Type and impredicative on Prop, it is easy to show the following result: every closed term ...
8
votes
1answer
140 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 ...
8
votes
0answers
291 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]...
4
votes
1answer
144 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 ...
10
votes
1answer
367 views