Questions tagged [type-systems]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
1 answer
115 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 ...
Andrew's user avatar
  • 121
2 votes
2 answers
195 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 ...
Jake's user avatar
  • 1,183
2 votes
0 answers
40 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 ...
yiyuan-cao's user avatar
2 votes
1 answer
135 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 ->...
manu fava's user avatar
  • 123
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 ...
nullUser's user avatar
  • 111
3 votes
1 answer
262 views

Model foreign keys as dependent types?

A database consists a list of tables. For example you have a table of Worker and a table of Project where each project needs a ...
molikto's user avatar
  • 347
4 votes
1 answer
149 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 ...
Brian Berns's user avatar
10 votes
0 answers
183 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 ...
ionchy's user avatar
  • 325
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 ...
user3113723's user avatar
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 ...
Molly Stewart-Gallus's user avatar
9 votes
3 answers
535 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 ...
Max New's user avatar
  • 1,663
0 votes
0 answers
68 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}~~ \...
Coder's user avatar
  • 109
10 votes
2 answers
483 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 ...
Jozef Mikušinec's user avatar
1 vote
0 answers
36 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 ....
Cristian Gratie's user avatar
2 votes
0 answers
75 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 ...
Cristian Gratie's user avatar
1 vote
0 answers
188 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 -- ...
Nathan BeDell's user avatar
0 votes
1 answer
246 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 ...
Siddharth Bhat's user avatar
1 vote
2 answers
195 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 ...
user avatar
3 votes
1 answer
178 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 ...
user avatar
5 votes
1 answer
218 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 ...
Labbekak's user avatar
  • 701
0 votes
1 answer
119 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 ...
PePe's user avatar
  • 13
8 votes
2 answers
335 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 ...
xrq's user avatar
  • 1,175
3 votes
1 answer
248 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",...
Léo Vital's user avatar
6 votes
0 answers
125 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 ...
Ilk's user avatar
  • 920
3 votes
0 answers
156 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 (...
Joey Eremondi's user avatar
8 votes
1 answer
519 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 ...
Joey Eremondi's user avatar
5 votes
2 answers
266 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 ...
Qhead's user avatar
  • 53
3 votes
0 answers
409 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: ...
Labbekak's user avatar
  • 701
7 votes
1 answer
250 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 ...
Labbekak's user avatar
  • 701
2 votes
1 answer
315 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 ...
InsideLoop's user avatar
7 votes
2 answers
405 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 ...
Labbekak's user avatar
  • 701
12 votes
2 answers
754 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 ...
Joey Eremondi's user avatar
1 vote
1 answer
197 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-...
Francesco Bertolaccini's user avatar
-3 votes
1 answer
184 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 ...
Vincent's user avatar
  • 307
0 votes
1 answer
99 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 ...
Vincent's user avatar
  • 307
6 votes
2 answers
299 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[...
Joey Eremondi's user avatar
5 votes
1 answer
464 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 ...
Łukasz Lew's user avatar
  • 1,187
8 votes
1 answer
778 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 ...
Jake's user avatar
  • 1,183
2 votes
2 answers
661 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 ...
Rusty Fieldstone's user avatar
5 votes
1 answer
251 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 ...
Łukasz Lew's user avatar
  • 1,187
2 votes
1 answer
503 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?
Łukasz Lew's user avatar
  • 1,187
3 votes
1 answer
223 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 ...
Łukasz Lew's user avatar
  • 1,187
1 vote
0 answers
64 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 ...
Jesper Dahl's user avatar
9 votes
1 answer
237 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.
Alejandro DC's user avatar
7 votes
1 answer
463 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 ...
Joey Eremondi's user avatar
2 votes
1 answer
491 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 ...
Sam R.'s user avatar
  • 123
4 votes
0 answers
65 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 ...
Andrew Polonsky's user avatar
2 votes
1 answer
120 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$, ...
lilott8's user avatar
  • 185
7 votes
1 answer
751 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$-...
Turion's user avatar
  • 616
6 votes
1 answer
371 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)....
Andrew Bacon's user avatar