27
Here are a few things to keep in mind:
Although we generally think we know what we mean by set-theoretic intersection and union, there have been several different takes on what exactly intersection and union types are. So, it's worth pinning this down before you embark on an implementation.
One element which I think is awfully important for understanding ...
21
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 U, and say that every program has type U. This isn't terribly useful, but it makes a point.
There are many ways to understand types, but from a programmer's point of view the following ...
21
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, in their 1991 PLDI paper, Refinement Types for ML.
Rowan Davies studied type inference for refinement types in his PhD thesis, Practical Refinement Type ...
14
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 example makes it easier to follow:
((\x.x) (\y.y)) 10
For maximum clarity, let's start by assigning type variables to each sub expression:
x : A
(\x.x) : B
y : C
...
13
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 $\mu$ at the universe of all types. Given a system of mutually recursive equations
\begin{align*}
A &= F(A, B)\\
B &= G(A, B)
\end{align*}
where $F, G : ...
11
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\to\alpha)$ usually abbreviated as $(\alpha\to\alpha)\to(\alpha\to\alpha)$, but you cannot have $(\forall \alpha.\alpha\to\alpha) \to (\forall \alpha.\alpha\to\...
10
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 former is really a question in program verification and has little to
do with typing. Just needs showing that your implementation meets its
specification, see Andrej'...
10
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) is decidable, which is to say it doesn't matter whether $a$ is well-typed or not to get an answer. Indeed, all proof checkers based on MLTT implement some ...
9
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 inference is performed in such a way that we never attempt to normalize a term, unless we have established beforehand that it is well-typed. Similarly, we never ...
9
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 application of type synonyms is equivalent to adding lambda-abstraction to the language of type expressions. This is because type synonyms suffice to encode the SKI ...
8
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 lambda calculus is by trying to type application and abstraction using the linear implication $A \multimap B$,
$$
\frac{\Gamma \vdash t:A\multimap B\quad \Delta\...
8
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, your derivation works regardless of the type of the answer -- the very same term you have works for $\mu a.\; a \to X$ for any $X$.
This is known as Curry's ...
8
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 mutable variable bindings, you never generalize.
The standard ML-like behaviour is then:
let xs = [] // xs : forall a. list a
let as = 1 :: xs // ...
7
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 Vrech, 2008
The problem of typing polymorphic recursion (i.e., recursive function
definitions rec {x = e} where different occurrences of x in e are used
...
6
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 Subtyping Algorithm by Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers
type-inference formalization in Coq, based on A Rewriting Semantics for Type ...
6
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 bindings:
let mut x = 1
let y = x // x or !x ?
let mut z = x // x or !x ?
let f a = (y := a) // legal?
let g a = (z := a; x) // ...
6
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 Church-style grammar with explicit type annotations) and it worked very well in practice, it revealed all the bugs there was to find on this particular part of the ...
6
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. Monomorphisation
gets this information for you by specializing away the
polymorphism. Boxing gets this information for you by putting
everything into a representation of ...
5
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 get rid of $X$, and so we can run in circles, as your example shows.
There is a way to avoid this by allowing arbitrary recursive types. If we have an equation ...
5
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 algorithms is that they generate the principal type for a term; translated into AI terms, this means that you never need to widen, nor do you need to go to power ...
5
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 Polymorphism in Coq, Interactive Theorem Proving - 5th International Conference, ITP 2014
Beta Ziliani & Matthieu Sozeau: A Unification Algorithm for Coq featuring ...
5
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 theory is good enough to prove whatever properties about the language. Andrej's answer tackles this area very well imo. The other half of the question is —...
5
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 none. This naturally leads to Curry-style typing, i.e., we think of $t : A$ as a relation where both the term $t$ and the type $A$ are meaningful by themselves. (...
5
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}}$, $*_{\mathrm{poly}}$ and $\square$ along with the axioms
$$ *_{\mathrm{mono}}, *_{\mathrm{poly}}\ :\ \square$$
and the rules
$$(*_{\mathrm{mono}},*_{\mathrm{mono}},*_{\...
4
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 reconstruction problem
for $\Lambda_k$ extended by this typing is undecidable.
Unfortunately, this result does not give any clue as to whether type
reconstruction ...
4
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 case, then one idea would be to follow a kind of occurs-check discipline. One thing that you can do to eliminate cycles is to maintain the invariant that there ...
4
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 an enumeration of untyped terms and empirical data on the sieve approach to enumerating typed lambda terms. It looks like they use a hindley-milner type system ...
3
Ok, so I figured it out the next day. It's all dead simple as it came out.
Let's use an example – type applications z a a and z a b where z :: * -> * -> *. The unification will yield that (without further context) z a a is the most general type for both giving substitution {b↦a}. On the other hand, z a a cannot be matched to z a b, as they are simply ...
3
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 apply it to an integer you don't want the type of that identity function to be specialized to int -> int. That's why you generalize it. Note that this is done at ...
3
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
Assuming ≡ to be the homogeneous equality type and refl to be its constructor, the solution to the underscore is B, which is not defined there yet. Type checking the above code (with open import ...
Only top voted, non community-wiki answers of a minimum length are eligible
