21
votes
What should a proof of correctness for a typechecker actually be proving?
That's a good question! It asks what we expect from types in a typed language.
First note that we can type any programing language with the unitype: just pick a letter, say ...
- 26.6k
21
votes
Accepted
Subtypes as subsets of SML datatypes
These kinds of types -- where you define a subtype (basically) by giving a grammar of the acceptable values -- are called datasort refinements.
They were introduced by Tim Freeman and Frank Pfenning,...
- 31.6k
20
votes
Accepted
Swapping arguments of variables in higher-order pattern unification
I have developed this, but haven't yet published it in a more strucured/formal manner.
"Enhanced pattern unification" abstract here.
Demo implementation.
Video recording.
You're absolutely ...
- 1,349
14
votes
Accepted
Is this behavior in a programming language inconsistent?
Yes, your type inference seems incomplete. This example can be dealt with fairly trivially, by computing the respective type equations, e.g. in the style Hindley/Milner does it.
Alpha-renaming the ...
- 1,290
13
votes
Accepted
Can Isorecursive types capture mutually recursive data types?
In general, for any type (or domain, or complete lattice) $X$ we can consider the least fixed-point operator $\mu_X : (X \to X) \to X$. For recursive types we take $X = \mathsf{Type}$, i.e., we apply $...
- 26.6k
11
votes
Accepted
What is the difference between System F and Hindley-Milner type system?
Yes, In Hindley-Milner universal quantifiers are allowed only at the outside of a type (and therefore omitted). For example, in HM you can have the type $\forall \alpha.(\alpha\to\alpha) \to (\alpha\...
- 593
11
votes
Accepted
"Spurious" Type Equivalences in MLSub/Algebraic Subtyping
in their ICFP 2000 paper Intersection types and computational effects, Rowan Davies and Frank Pfenning showed that the distributivity rule for function types is unsound in the presence of effects.
...
- 31.6k
10
votes
Accepted
Decidability of type inference and type checking in MLTT
Certainly the decision problem
Given a (pre-)term $a$ Is there a type $A$ such that $\vdash a :A$ is derivable in MLTT?
Sometimes written $\vdash a\ :\ ?$ (and called the type inference problem) ...
- 13.2k
10
votes
Accepted
What should a proof of correctness for a typechecker actually be proving?
The question can be interpreted in two ways:
Whether the implementation does implement a given typing system $T$?
Whether the typing system $T$ does prevent the errors you think it should?
The ...
- 10.3k
10
votes
"Spurious" Type Equivalences in MLSub/Algebraic Subtyping
A typechecker for an ML-like language has two tasks:
Inference: given a program, come up with a type for it, or prove that none exists.
Subsumption: given an inferred type and a user-written type ...
- 101
9
votes
Accepted
Decidability of parametric higher-order type unification
No, it's not decidable. The pure simply-typed lambda calculus is parametric in your sense (it has no case analysis) and higher-order unification is undecidable.
In general, permitting partial ...
- 31.6k
9
votes
Accepted
Can all linear lambda calculi be linearity checked syntactically?
I don't want to make a statement about "all linear lambda calculi" since it's hard to make that precise, but for pure linear lambda-calculus the answer is yes. One way to enforce linearity in pure ...
- 4,309
9
votes
Accepted
Recursive types and the empty type
First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, ...
- 31.6k
9
votes
Decidability of type inference and type checking in MLTT
I would like to supplement the answer by cody by a general observation conveying my understanding of why the type checking algorithms work.
For a wide class of type theories, type checking or ...
- 26.6k
9
votes
Accepted
Extending Hindley-Milner to type mutable references
To get behaviour similar to Ocaml, simply avoid generalizing the type of mutable variables.
With ordinary let-bindings, you generalize if you bind a value, and don't generalize otherwise. With ...
- 31.6k
7
votes
Extending Hindley-Milner to type mutable references
As Martin Berger points out in his comment, it is not actually entirely obvious what the semantics of your language is supposed to be and what "automatically inserting !" means. Consider the following ...
- 1,290
7
votes
Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?
You should have a look at the following paper -- and the previous work by Gori and Levi:
On Polymorphic Recursion, Type Systems, and Abstract Interpretation
Marco Comini, Ferruccio Damiani, Samuel ...
- 1,882
6
votes
Verified type checkers
Here are some results of a simple Google search:
Certification of a Type Inference Tool for ML: Damas–Milner within Coq by Catherine Dubois and Valérie Ménissier-Morain
Formalization of a Polymorphic ...
- 26.6k
6
votes
Efficiently ordering typed programs
Two remarks first:
I have used the "randomly generate terms and check that they are well-typed" approach (you mention that "untyped" terms are generated, you can also randomly generate terms in a ...
- 1,882
6
votes
Accepted
Higher-rank polymorphism over unboxed types
I've thought a bit about this. The main issue is that in general, we
don't know how big a value of polymorphic type is. If you don't have
this information, you have have to get it somehow. ...
- 31.6k
5
votes
What should a proof of correctness for a typechecker actually be proving?
There are a few different things you could mean by "prove that my typechecker works". Which, I suppose, is part of what your question is asking ;)
One half of this question is proving that your type ...
- 720
5
votes
Accepted
Efficiently ordering typed programs
For ordered enumeration instead of random generation you are getting into the realm of combinatorics. I don't know of any generic results, but this paper Counting and Generating Lambda Terms describes ...
- 1,412
5
votes
Accepted
Can type inference be classified in two groups: unification-based and control-flow-based?
Perhaps an even better way to see type inference is as a specialization of a single framework: Abstract Interpretation (abbreviated AI). The hallmark of most unification-based type inference ...
- 1,490
5
votes
Accepted
Occurs check in type inference
Yes, the occurs check is there so that the algorithm is guaranteed to terminate. Without it, when we deal with an equation $X = T$ in which $X$ may occur, substituting $T$ for $X$ everywhere does not ...
- 26.6k
5
votes
Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?
Apart from what's already written in the slides you linked to, let me describe one possible approach.
For studying type inference semantically we need a model in which a term can have many types, or ...
- 26.6k
5
votes
Accepted
Decidability of rank-k polymorphism vs. System F
The conclusion of [Kfoury & Tiuryn 1992] says (emphasis mine):
We prove that [...] for every $k\ge 3$ there is a typing of constants
that assigns types in $S(1)$ such that the type ...
- 4,746
5
votes
Accepted
Universe polymorphism: the inference of universes and their constraints
It's complicated because universe constraints are simplified during inference (in order to avoid an explosion of constraints). Have a look at:
Matthieu Sozeau and Nicolas Tabareau: Universe ...
- 26.6k
5
votes
Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?
This isn't an excessively deep answer, but you can express a type system based on STLC with prenex polymorphism as a Pure Type System in a quite simple way, using sorts $*_{\mathrm{mono}}$, $*_{\...
- 13.2k
4
votes
Avoiding Cycles with Unification and Subtyping
From what I understand, it is likely that your subtyping constraints will always be of the form $\alpha \subseteq A$ or $A \subseteq \alpha$, where $\alpha$ is a unification variable. If that is the ...
- 311
4
votes
"Spurious" Type Equivalences in MLSub/Algebraic Subtyping
I'm late to the party, but I'd like to make a small clarification.
I did not really mean that MLsub has "too many" type equivalences. As explained in the same section of the Simple-sub paper ...
- 212
Only top scored, non community-wiki answers of a minimum length are eligible