Questions tagged [type-systems]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
33
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 ...
21
votes
2answers
3k 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 ...
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: ...
15
votes
4answers
576 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 ...
15
votes
1answer
3k views

How does inheritance differ from subtyping?

In programming language perspective, what is mean by subtyping? I heard that "Inheritance is not Subtyping". Then what are the differences between inheritance and subtyping?
14
votes
1answer
966 views

A mathematical (categorical) description of type classes

A functional language can be viewed as a category where its objects are types and morphisms functions between them. How do type classes fit in this model? I assume we should only consider those ...
11
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 ...
11
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 ...
11
votes
1answer
370 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 ...
11
votes
0answers
141 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 ...
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 ...
10
votes
2answers
814 views

Ownership types and Separation Logic

Ownership types and Separation Logic seem to have similar goals, control over ownership and aliasing. Perhaps, I should also add: the ability to write modular specifications. What is known about the ...
10
votes
2answers
220 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 ...
10
votes
1answer
314 views

Is `sort` typeable on elementary affine logic?

The following λ-term, here in normal form: ...
9
votes
2answers
324 views

Research on call-site based type inference?

I'm trying to learn more about whole-program type checking and type inferencing systems that use information from function call sites to compute type information (in addition to the standard approach ...
9
votes
1answer
146 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.
9
votes
1answer
443 views

What are possible implementations of Haskell's type classes and what are their (dis)advantages?

As far as I know, a Haskell function with type classes constraints is internally compiled to a function with additional arguments that receive dictionaries with the necessary implementations of each ...
8
votes
2answers
676 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 ...
8
votes
1answer
327 views

Proofs techniques related to Curry–Howard correspondence

I am looking for sources about formalized notion of programs. This seems to be closely related to Curry-Howard correspondence, but one could also track this back to Universal Turing Machines and its ...
8
votes
3answers
747 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. ...
8
votes
1answer
360 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 ...
8
votes
1answer
130 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
251 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]...
7
votes
2answers
297 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 ...
7
votes
1answer
744 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 ...
7
votes
2answers
207 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 ...
7
votes
1answer
433 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$-...
7
votes
1answer
136 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 ...
7
votes
1answer
321 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 ...
7
votes
1answer
247 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 ...
7
votes
1answer
793 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 ...
6
votes
1answer
293 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 ...
6
votes
1answer
191 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 ...
6
votes
1answer
230 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
265 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 ...
6
votes
0answers
77 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
2answers
392 views

the type system does not tell the whole story due to “exception”

I am wondering whether it is a bad style to use "exception". For example, in Ocaml, the exception does not appear as the .mli file. So it appears to me that "exception" is something that cannot be ...
5
votes
2answers
215 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
2answers
288 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)$ ...
5
votes
1answer
122 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 ...
5
votes
1answer
230 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)....
5
votes
1answer
343 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 ...
5
votes
2answers
162 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 ...
5
votes
2answers
297 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 ...
5
votes
1answer
208 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
218 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 ...
5
votes
0answers
256 views

Commonalities and differences between canonical structures and the implicit calculus

There is a paper on The Implicit Calculus as a generalization of type classes. Coq's canonical structures are also a generalization of type classes. The paper does not mention canonical structures ...
4
votes
1answer
113 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 ...
4
votes
1answer
133 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 ...
4
votes
1answer
281 views

Classes and types in object-oriented languages

In typical object-oriented programming languages like Java, classes are used as types. On the other hand, type-theoretic approaches to object-oriented languages treat interfaces as types. Are there ...