Hindley Milner + Scott Encoding Musings

hm_scott.lhs

Sometimes it would be nice if a type system could automatically "do it's best"
to restrict what a value will be. For example, the type `Bool` is the compiler
saying the value will either be `True` or `False`, but it doesn't know which.
What we want is the compiler to be able to be precise when possible, so instead
of always saying `Bool` (or "I don't know"), it could say `True`, `False`, or
`Bool`. This gist shows how Hindley Milner already has this capability that can
be exercised by using Church or Scott encodings of simple data types.

> {-# LANGUAGE RankNTypes #-}
> import qualified Data.Maybe as M
> import Prelude hiding (and, or)

Instead of the standard data constructors, we define church booleans. `True` and
`False` are synonyms for the types inferred for `true` and `false`, respectively.

> type True = forall a b . a -> b -> a
> true t f = t
> type False = forall a b . a -> b -> b
> false t f = f

We can define logical `or` and `and`, leaving the types blank intentionally

> or a b = a true b 
> and a b = a b false

Some tests, showing us that Hindley Milner infers precise types

> test1 = true `and` false :: False
> test2 = true `and` true :: True

This is in contrast with using standard booleans

> test3 = True && False :: Bool

We can create corresponding type for `Bool`

> type Boolean = forall a . a -> a -> a

Indeed, Hindley Milner will infer this type if we force it to unify `True` and
`False`:

> g f = (f true, f false) 

`g` will have the type `(Boolean -> a) -> (a, a)`

We can also encode `Maybe a` in a data type, with the general type 

> type Possibly a = forall b . b -> (a -> b) -> b

And the more precise types and their respective constructors:

> type Just a = forall b c . b -> (a -> c) -> c
> just a n j = j a
> type Nothing = forall a b . a -> b -> a
> nothing n j = n

We can use the more precise types to construct a version of `fromJust` that is
total

> data Bottom = Bottom
> fromJust p = p Bottom id 
> plus x y = fromJust x + fromJust y
> test4 = just 1 `plus` just 2 :: Int

Now, the following expression would create a type error:

```haskell
  typeError = just 1 `plus` nothing
```

This is in contrast with using the partial function with the algebraic data
types, which will typecheck the `typeError` example without complaint:

> runTimeError = M.fromJust (Just 1) + M.fromJust Nothing

In fact, if Hindley Milner is implemented without an occurs check to allow
infinite types, one can do the same thing for lists and other infinite data
types, allowing for pure `head` implementations, etc.

So it seems there is some sense that by creating algebraic data types, we trade
off precision in inference for clarity.

I would love to hear from people who know more about this area, this is just a
result of me dabbling.