26
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 ...
20
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 ...
20
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
If you're looking for a neat, functional reference to type-inference, I'm a bit partial to Gundry, McBride, and McKinna's 2010 "Type Inference in Context", though this may not be a good guide to any actual existing implementations.
I think part of the answer is that, beyond the value restriction, there really isn't that much difficulty adapting Hindley-...
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 : ...
11
Almost all systems with type inference use call-site information to do this. Examples include Standard ML, OCaml, F#, and Haskell. Many other languages use call-site information to infer type parameter instantiation, such as Java, C#, Scala, and Typed Racket. This often goes by the name "Local Type Inference".
I would just describe what you're looking ...
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\...
11
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 : ...
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'...
9
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
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
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 ...
7
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 // ...
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 ...
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
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
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 Comini1, Ferruccio Damiani2, 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
...
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
As far as I know, showing that this direction is the hard part of Wells proof! At least this is what Pawel (Urzyczyn) explained to me a few years back.
Apparently it is not too hard to show that type checking is undecidable; the hard part is showing that this implies undecidability of type reconstruction! Indeed there are some cases in which the first is ...
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
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
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 —...
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
The way Haskell solves this problem is through Type Classes (see these papers for an overview). The idea is that it is not the $\_^{-1}$ operation that is special; it is the $\mathrm{\bf Array}$ type! To this end, you can define a (statically) overloaded method $map$ which works on each such type. In Haskell:
class Mappable m where
map : (a -> b) -> ...
3
Xavier Leroy's PhD thesis is a good start.
2
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 ...
Only top voted, non community-wiki answers of a minimum length are eligible
