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 ...
user avatar
  • 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,...
user avatar
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 ...
user avatar
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 ...
user avatar
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 $...
user avatar
  • 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\...
user avatar
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. ...
user avatar
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) ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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, ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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. ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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}}$, $*_{\...
user avatar
  • 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 ...
user avatar
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 ...
user avatar

Only top scored, non community-wiki answers of a minimum length are eligible