Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [type-systems]

The tag has no usage guidance.

8
votes
2answers
161 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
102 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
67 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
63 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 ...
5
votes
2answers
166 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[...
4
votes
1answer
100 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
248 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
207 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 ...
4
votes
1answer
103 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 ...
2
votes
1answer
97 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?
3
votes
1answer
123 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
vote
0answers
44 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 ...
9
votes
1answer
126 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.
8
votes
1answer
222 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
votes
1answer
142 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 ...
4
votes
0answers
61 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 ...
3
votes
1answer
82 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
333 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$-...
6
votes
1answer
208 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
221 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 ...
6
votes
1answer
215 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). ...
8
votes
1answer
128 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 ...
9
votes
0answers
220 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]...
20
votes
2answers
2k 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 ...
3
votes
1answer
126 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 ...
6
votes
2answers
260 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 ...
7
votes
1answer
280 views

What type system fits the subclass of λ-terms that can be reduced optimally?

There is a subset of λ-calculus terms that can be reduced by Lamping's Abstract Algorithm without using the Oracle. That is an interesting subset, because only for those terms it is proven that ...
12
votes
1answer
330 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
382 views

Featherweight Generic Java formalization in Coq

I've been searching for some nice formalization of FGJ (Featherweight Generic Java) in Coq. I am going to develop an extension of FGJ in Coq, so I hope there is an appropriate Coq implementation which ...
8
votes
3answers
688 views

Universal and existential types

I'm trying to wrap my head around the concepts of universal and existential types but everywhere I look, I see either logical or operational intuitions (or implementations) (e.g. TAPL book by B. ...
10
votes
1answer
302 views

Is `sort` typeable on elementary affine logic?

The following λ-term, here in normal form: ...
4
votes
1answer
117 views

Rendering of type-level computation

Programming languages with dependent types and/or higher-kinded types feature what might be called compile-time computation at the type-level. This is usually defined as follows (I'm omitting some ...
5
votes
1answer
263 views

Can all linear lambda calculi be linearity checked syntactically?

Given a lambda calculus with explicit linearity and usual application and abstraction, can the linearity check be done on an untyped syntax tree if we keep track of the structural types? Are the ...
1
vote
0answers
119 views

Has there been work on formal Semantics for linear algebra?

Could I get some references on formal semantics for a calculus on linear algebra that helps you study matrix or tensor based programming languages? I am looking for anything that encompasses linear or ...
6
votes
0answers
71 views

Decidability of equality between higher-kinded equirecursive types (or: between nonregular Böhm trees)

In §3 of Polytypic values possess polykinded types, Ralf Hinze described a calculus of types with higher-kinded recursive types. There is a fixed-point combinator $$\mu_\kappa : (\kappa \rightarrow \...
5
votes
1answer
198 views

Can type inference be classified in two groups: unification-based and control-flow-based?

I recently came across the 1995 paper Safety analysis versus type inference (pdf link) by Palsberg and Schartzbach that contrasts unification-based type inference and static analysis methods based on ...
5
votes
1answer
200 views

Commutativity of addition in polymorphic lambda calculus

In the article "Extensional models of polymorphism" by Breazu-Tannen and Coquand, natural numbers are presented using a Church-like encoding: $polyint = \forall t . (t \to t) \to t \to t$ Addition ...
11
votes
0answers
135 views

Are the types that show monads are more powerful than continuations revealing something of fundamental importance?

In 1992 in the paper Imperative Functional Programming, Simon Peyton Jones and Philip Wadler write: So monads are more powerful than continuations, but only because of the types! It is not clear ...
4
votes
0answers
75 views

Non-objected oriented type theories that can express the $\nu Obj$ calculus

Odersky et al.'s $\nu Obj$ calculus [1] adds just enough dependent typeness on top of object oriented programming to express interfaces that define types (and consequently module systems and other ...
6
votes
1answer
701 views

Practical implementation of Hindley–Milner with typeclasses — matching vs most general unifier

I'm trying to get a deep understanding of a (great) paper "Typing Haskell in Haskell". I'm having difficulties understanding the implementation of two methods there — the ...
5
votes
2answers
260 views

Isomorphism between algebraic data-types

I have two types of trees in Haskell, defined as the least solution of the following equations: $T_1(A) \cong 1 + A + T_1(A) \times T_1(A)$ $T_2(A) \cong 1 + A \times T_2(A) + T_2(A) \times T_2(A)$ ...
3
votes
1answer
462 views

Occurs check in type inference

I'm reading about type inference in chapter 30 of Programming Languages: Application and Interpretation and I'm trying to understand exactly how the occurs check works in an example I came up with. ...
10
votes
1answer
1k views

Homotopy type theory and Gödel's incompleteness theorems

Kurt Gödel's incompleteness theorems establish the "inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic". Homotopy Type Theory provides an alternative ...
3
votes
1answer
379 views

Language with extensible type system?

Is there a practical programming language that has an extensible type system? Or alternatively, an add-on type system that can be used with existing languages? With extensible I mean that the typing ...
5
votes
1answer
119 views

Extending simple types to allow `fix`

I'm reading some lecture notes saying that “fix cannot be defined in the simply typed lambda-calculus” and that “no expression that can lead to non-terminating ...
16
votes
2answers
2k views

What parts of homotopy type theory are not possible in Agda or Coq?

When we look at the book, Homotopy Type Theory - we see the following topics: ...
11
votes
2answers
1k 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 ...
1
vote
1answer
111 views

Type, operation and function, and their limits

First of all, sorry for my English. I would like to know, when I want to define a new type (I'm currently developing a computer interpreted language), how can I determine which "functions" are ...
5
votes
1answer
186 views

Typing relations terminology – how do I read typing relations?

I am currently trying to read up on type theory and have some quick questions on terminology. In the following rule, $$ \frac{x:T_1 \vdash t_2 : T_2}{\vdash \lambda x:T_1.t_2:T_1\to T_2} $$ How ...
7
votes
1answer
729 views

Constraint types (IBM/X10) compared to dependent types

Constraint types have been proposed by IBM in their X10 programming language (it's a commercial programming language, not open source software). Nystrom, Nathaniel, et al. "Constrained types for ...