Questions tagged [type-systems]
The type-systems tag has no usage guidance.
83
questions
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 ...
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 ...
17
votes
1answer
4k 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?
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
629 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
1k 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 ...
12
votes
1answer
2k 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 ...
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 ...
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
2answers
426 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 ...
11
votes
1answer
470 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
150 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
2answers
885 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
1answer
365 views
9
votes
3answers
846 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. ...
9
votes
2answers
373 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
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.
9
votes
1answer
474 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
1answer
358 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
1answer
440 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
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
1answer
920 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 ...
8
votes
0answers
289 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]...
8
votes
0answers
84 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 \...
7
votes
2answers
816 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 ...
7
votes
2answers
201 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 ...
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 ...
7
votes
1answer
782 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
288 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
178 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
560 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
268 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). ...
7
votes
1answer
470 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
295 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 ...
7
votes
1answer
331 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 ...
6
votes
1answer
323 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
198 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
275 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
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 ...
5
votes
2answers
399 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
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
2answers
367 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
125 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
288 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
486 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
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 ...
5
votes
1answer
165 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 ...
5
votes
1answer
226 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 ...
5
votes
2answers
344 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
108 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 ...
