ByteLabs

The following shows some dummy Haskell example code that demonstrates the usage of rank-n types:

{-# LANGUAGE RankNTypes #-}
module Main (main) where
-- g1: identity function
-- GHC implicitely quantifies it to: forall a. a -> a
g1 :: a -> a
g1 x = x
-- g2: Rank2Type
g2 :: (forall a. a -> a) -> (Bool, Char)
g2 f = (f True, f 'a')
-- g3: Rank3Type
g3 :: ((forall a. a -> a) -> (Bool, Char)) -> (Char, Bool)
g3 f = (\x -> (snd x, fst x)) (f g1)
-- g4: Rank4Type
g4 :: (((forall a. a -> a) -> (Bool, Char)) -> (Char, Bool)) ->
         (Bool, Char)
g4 f = (\x -> (snd x, fst x)) (f g2)

main :: IO ()
main = do
  putStrLn "Rank-2 Example:" 
  putStrLn . show . fst . g2 $ g1
  putStrLn . show . snd . g2 $ g1
  putStrLn "Rank-3 Example:" 
  putStrLn . show . fst . g3 $ g2
  putStrLn . show . snd . g3 $ g2
  putStrLn "Rank-4 Example:" 
  putStrLn . show . fst . g4 $ g3
  putStrLn . show . snd . g4 $ g3

If you want to see more ‘useful’ examples have a look at the paper Practical Type Inference for Arbitrary-Rank Types.

The polymorphism of System F is often called impredicative. A definition is called impredicative if it involves a quantifier whose domain includes the very thing being defined. For example in System F, the type variable X in the type T = ∀X. X → X ranges over all types, including T itself (so that, for example, we can instantiate a term of type T at type T, yielding a function from T to T).[6]

The polymorphism found in ML is called predicative, because the range of type variables is restricted to monotypes (i.e. quantifier-free types), which do not contain quantifiers.

When talking about type reconstruction the previous definitions are important. There is a growing “[...] need for ever more expressive type system features, most of which threaten the decidability and practicality of Damas-Milner type inference. One such feature is the ability to write functions with higher-rank types—that is, functions that take polymorphic functions as their arguments.”[1]

Complete type inference is known to be undecidable for higher-rank (impredicative) type systems. This post serves as a reference for type reconstruction in the presence of polymorphism in higher-rank type systems.

[1] Practical type inference for arbitrary-rank types

[2] Haskell/Polymorphism

[3] Type Polymorphism – DocForge

[4] Type Polymorphism -Wikipedia

[5] System F – Polymorphic/Second-Order Lambda Calculus

[6] Types and Programming Languages [p.360]

The term “Hindley-Milner type system” is one I have read quite often only having had an intuitive understanding of what it means. Since every paper about Type Systems or some Functional Programming papers often use the term in such a way that one might get the impression that it is universally understood by everyone, I was firstly reluctant to ask the simple question:

• What is a Hindley-Milner type system?

But the simple questions are usually the interesting ones! When you write a program in an imperative programming language like Java, C, etc. the compiler depends on explicit type annotations in order to do its type checking. This may not sound particularily disturbing since a good programmer should always know the types of function arguments, return types, etc. Type ascriptions also serve as documentation. So what’s wrong with explicit type annotation?

1. It is tedious!
2. You do not always get it right!
3. It is tedious!
4. You do not always get it right!
5. ...

But what about languages like Ruby, Perl, PHP etc. where there is no need – or almost no need – for explicit type annotations? How do those languages infer the types of expressions, function parameters, variables etc. (e.g. Perl example ‘sub foo($) { my $arg = shift; }‘) In order to answer this question it necessary to distinguish between the following type checking strategies:

• Statically checked: Static type checking happens during compile time. It can be seen as a static approximation to the run-time behaviors of terms in a program.

• Dynamically checked: Dynamic or latent type checking occurs during run-time, where run-time type tags are used to distinguish different kinds of structures in the heap.

• Hybrid – statically & dynamically checked: Many languages like Java do extensive static type checking as well as some dynamic type checking during run-time (e.g. to support down casts (a.k.a. widening))

Thus ‘type inference’ and ‘type checking’ in languages such as Ruby, Perl, PHP etc. happens at run-time when all the expressions are evaluated. Even some language constructs in Java require run-time ‘type checking’. A language like Haskell infers and checks types statically – so you do not have to run a program to find out about possible type errors.

There is a lot of debate on what strategy is ‘better’ or ‘worse’, but hey, what about Hindley-Milner? So let others do the debating about the merits of language XYZ and its type checking strategy and let’s concentrate on the original problem.

Type Inference

Type inference is the ability to deduce the type of a value derived from the eventual evaluation of an expression. So we do not actually evaluate an expression to ‘infer’ its type (dynamic typing), but rather infer the type of a value before the expression which produces it is evaluated (static typing). How can this work? Well, if the compiler is able to recognize the eventual reduction of an expression to implicitly typed atomic values (e.g. 1, “string”, 1.3, False), it is able to type check and compile a program completely without type annotations. Now there are limits to this, but delving into those would be a bit too much for now.

• So what does Hindley-Milner stand for ?!

Finally we can answer this question! The common algorithm used to perform type inference is referred to as Hindley-Milner or Damas-Milner algorithm. So if you have a language with a Hindley-Milner type system, it basically means that the language can infer almost all types and you do not have to explicitly write type ascriptions. Of course you can still make type annotations where it makes sense for better readabilty. Hindley-Milner type inference will check if your ascriptions are correct and ensure that there are no type errors before you execute the program. In case of type errors it is even able to tell you what type it would have expected at the erroneous position. That’s pretty cool and very powerful indeed!

Sources:

• http://en.wikipedia.org/wiki/Type_inference
• Pierce, Benjamin C.. Types and Programming Languages (Chapters 1, 23)