# Tag Info

### 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
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
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
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
Accepted

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
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
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

### "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 ...
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
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
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

### 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
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

### 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

### 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

### 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

### 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
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

### 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
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
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
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

### 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
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
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