22 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 ...
Andrej Bauer's user avatar
  • 28.9k
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,...
Neel Krishnaswami's 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 ...
András Kovács's user avatar
15 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\...
Martin Hofmann's user avatar
14 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 $...
Andrej Bauer's user avatar
  • 28.9k
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. ...
Neel Krishnaswami's 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 ...
Stephen Dolan's 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) ...
cody's user avatar
  • 13.9k
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 ...
Martin Berger's 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, ...
Neel Krishnaswami's 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 ...
Andrej Bauer's user avatar
  • 28.9k
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 ...
Neel Krishnaswami's user avatar
9 votes

Example of a term in system F which is not typable in the simply typed lambda calculus

Reacting to the previous answers, I think this is the simplest self-application which only contains types which have closed inhabitants. $$\lambda\,(f\,:\,\forall\,\alpha.\,\alpha\to\alpha).\,f\,(\...
András Kovács's 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 ...
gasche's user avatar
  • 2,040
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 ...
Andreas Rossberg's user avatar
7 votes
Accepted

Example of a term in system F which is not typable in the simply typed lambda calculus

Every normal term may be typed in system F (I can't seem to find a reference now, I'll come back with one when I have some more time). So, for example, letting $A:=\forall X.X$, then $$x^A(A\to\alpha)...
Damiano Mazza's user avatar
7 votes

Example of a term in system F which is not typable in the simply typed lambda calculus

Damiano Mazza's example uses an uninhabited type, $∀ X ⋅ X$. It is correct, but raises the obvious question whether one can do without. Here is an example that I find quite natural: $$Λ \ A B ⋅ λ \ (p ...
Jean Abou Samra's user avatar
6 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 ...
Max New's user avatar
  • 1,675
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 ...
gasche's user avatar
  • 2,040
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. ...
Neel Krishnaswami's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.9k
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}}$, $*_{\...
cody's user avatar
  • 13.9k
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 ...
Andrej Bauer's user avatar
  • 28.9k
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 ...
Radu GRIGore's user avatar
  • 4,796
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 ...
Andrej Bauer's user avatar
  • 28.9k
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 ...
wren romano's user avatar
4 votes

Generalization and instantiation of types in Hindley-Milner type inference

However, I fail to see what this accomplishes and when you want to do this, and would be very grateful if someone can point me in the right direction. When you define the function x -> x and first ...
J D's user avatar
  • 375
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 ...
Rodolphe Lepigre's 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 ...
Lionel Parreaux's user avatar
3 votes
Accepted

Counterexample request: ill-scoped metavariable solution

I think I just came up with one. The following code block is written in a syntax similar to Agda. test : (a : _) (B : Set) (b : B) -> a ≡ b test a B b = refl ...
ice1000's user avatar
  • 965

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