Questions tagged [type-systems]
The type-systems tag has no usage guidance.
91
questions
0
votes
0
answers
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 ...
- 111
9
votes
3
answers
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
0
votes
0
answers
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
0
votes
0
answers
59
views
A fundamental question about the proof by induction in session types
I have a question about proof by induction in the domain of session types. Let's assume we have the following lemma:
$$
\text{Let}~ \Gamma \vdash P : T. ~~\text{If } P = \mu X.
Q ~~\text{then}~~ \...
- 109
10
votes
2
answers
368
views
What are the issues with a set-like interpretation of quantifiers in type theory?
In his answer to a question that tries to treat universal and existential quantifiers as intersections and unions of sets, Andrej Bauer says:
Forget the intersections and unions. People get this idea ...
- 170
1
vote
0
answers
32
views
Can this be formalized as a conversion rule for CoC?
Consider the Church encoding of booleans in CoC
$$
Bool := \forall t : * . t \to t \to t \\
T := \lambda t : * . \lambda x : t . \lambda y : t . x \\
F := \lambda t : * . \lambda x: t . \lambda y : t ....
- 151
1
vote
0
answers
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 ...
- 151
1
vote
0
answers
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 -- ...
- 603
0
votes
1
answer
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 ...
- 565
1
vote
2
answers
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 ...
user61651
3
votes
1
answer
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 ...
user61651
5
votes
1
answer
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
0
votes
1
answer
84
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 ...
- 13
7
votes
2
answers
232
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 ...
- 1,125
3
votes
1
answer
209
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",...
- 43
2
votes
0
answers
157
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. ...
- 737
6
votes
0
answers
114
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 ...
- 713
3
votes
0
answers
150
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 (...
- 2,724
8
votes
1
answer
478
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 ...
- 2,724
5
votes
2
answers
229
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 ...
- 53
3
votes
0
answers
291
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:
...
- 691
7
votes
1
answer
199
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 ...
- 691
2
votes
1
answer
299
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 ...
- 121
7
votes
2
answers
334
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 ...
- 691
12
votes
2
answers
587
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 ...
- 2,724
1
vote
1
answer
149
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
1
answer
122
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 ...
- 263
0
votes
1
answer
80
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 ...
- 263
6
votes
2
answers
274
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[...
- 2,724
5
votes
1
answer
316
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 ...
- 1,147
7
votes
1
answer
566
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,131
1
vote
2
answers
530
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 ...
- 129
5
votes
1
answer
180
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 ...
- 1,147
2
votes
1
answer
288
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,147
3
votes
1
answer
143
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 ...
- 1,147
1
vote
0
answers
58
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 ...
- 121
9
votes
1
answer
192
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.
- 701
7
votes
1
answer
364
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 ...
- 2,724
2
votes
1
answer
435
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 ...
- 123
4
votes
0
answers
64
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 ...
- 601
2
votes
1
answer
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
7
votes
1
answer
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
5
votes
1
answer
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
7
votes
2
answers
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
7
votes
1
answer
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
8
votes
1
answer
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
8
votes
0
answers
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
24
votes
2
answers
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
4
votes
1
answer
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
5
votes
2
answers
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