Region, Effect and Closure Inference, implemented

Last post

Ben Lippmeier has posted an implementation of his region, effect, and closure inference in a Haskell dialect called The Disciplined Disciple Compiler.

Types at reddit

I have created a subreddit for types. (Static analysis is also welcome.)

Types, named (was: "Name that type!"), plus two more questions

Here are the answers to the previous quiz.

The first datatype holds any factorial number of values. Here it is again, with one small change and a few de-obfuscations:

> data FacHelp (f :: * -> *) (y :: *) = 
>      Stop y
>    | More (FacHelp (OneMore f) (f y))
> newtype OneMore (f :: * -> *) (y :: *) = 
>      OneMore (y, f y)
> newtype Identity y = Identity y
> type Factorial y = FacHelp Identity y

The second is lists of length more than two containing lists of length more than two. This means that no inhabitant contains a prime number of elements. As far as I know, it is unknown whether there is a datatype with every inhabitant containing a prime number of elements. (GADTs can do it, of course, but I'm ignoring those for now, since they can do anything. (mirror, mirror 2, mirror 3, mirror 4)

Here's that datatype again, renamed:

> data LongList x = Two x x
>                 | AndAnother x (LongList x)
> data Composite x = Composite (LongList (LongList x))

Update:
Chung-chieh Shan pointed out to me that I got that datatype wrong. (The other text above is correct, I think.) Anyway, here's his counterexample:

> test :: Composite Char
> test = Composite (Two (Two 'a' 'b')
>                       (AndAnother 'c' (Two 'd' 'e')))

This is a correct (I think!) implementation of a container that can't be of a prime size:

> data Product f g a = Times (f (g a))
>                    | LeftIncr (Product (OneMore f) g a)
>                    | RightIncr (Product f (OneMore g) a)
> newtype Pair a = Pair (a,a)
> type Comp = Product Pair Pair

End update

The third datatype uses the type H, which encodes containers with a square number of elements. H is based on the idea that the sequence of partial sums of the sequence of odd natural numbers is the same as the sequence of squares. That is, {0, 1, 1+3, 1+3+5, …} = {0², 1², 2², 3², …}

We can now use Lagrange's four-square theorem to see that question 3(b) is, strangely, a container that can hold any number of elements. An extension of this by Legendre showed [cite] that every number not of the form 4^k(8m + 7) is representable by the sum of three squares, and this answers question 3(a).

Here are both parts again, renamed and cleaned up a bit:

> data SqHelp x y = End
>                 | Extra x (SqHelp (y,y,x) y)
> type Square a = SqHelp a a
> data Legendre x = Legendre (Square x) (Square x) (Square x)
> data Lagrange x = Lagrange (Square x) (Legendre x)

Here are two more questions:
4. Can we write something analogous to 3(a) in a more direct way?
5.

> data M a b = N b
>            | O (M (a,b) a)
> newtype P a = P (M a a)

Name that type! (nested types edition)

Jump to the bottom for the quiz

If we want to write a type for binary trees in Haskell, it is easy to do so:

> data BinaryTree a = Leaf
>                   | InternalNode (BinaryTree a) a (BinaryTree a)

The structure of the type guarantees certain things about its inhabitants. For instance, every node has exactly two children. If we want to guarantee stronger invariants, we can change the shape of the type. We can write a a type for complete binary tree (that is, binary trees in which every leaf is at the same depth), as

> data CompleteBinaryTree a = Leaves
>                           | NonLeaves a (CompleteBinaryTree (a,a))

The argument in the recursive part of this datatype is not the same as it is in the declaration. Datatypes with this property are called nested or non-regular or heterogeneous or non-uniform. We can express all sorts of invariants with these datatypes. Here's another example:

> data AList a b = Nil
>                | Cons a (AList b a)

If we want to manipulate lists that alternate between two types a and b, we could use the type [Either a b], but this doesn't ensure that we don't have two as or two bs in a row. We could, instead, use the type [(a,b)], but this would only allow us to create lists of even length. By switching the position of the parameters in the recursion in AList, we can represent alternating lists of any length.

Here are some other examples of data structure invariants we can ensure with nested types:

• Cyclic data structures (mirror)
• Many different types of lists with fast cons, snoc, concatenation, and indexing, including
  • Finger trees (mirror, mirror 2)
  • Binary random-access lists, catenable lists, and catenable deques (earlier version, earlier version mirror, earlier version mirror 2, notes and answers to exercises)
  • Rightist right-perfect trees (mirror)
    • earlier version, earlier version mirror, earlier version mirror 2
    • even earlier version, even earlier version mirror, even earlier version mirror 2
• Red-black trees (a paper, code for that paper), AVL trees (mirror, mirror 2)
• Square matrices, triangular matrices (in various works by Ralph Matthes), Toeplitz matrices, rectangular matrices (see "Manufacturing Datatypes", above)
• Efficient-merge heaps (see Okasaki's thesis & book, above), Braun trees, left-complete trees (see "Manufacturing Datatypes", above)
• Binomial queues (mirror, mirror 2)
• Tries (mirror, mirror 2, code, code mirror, old version, old version mirror) (See also Okasaki's thesis & book)
• Well-formed terms in the locally-nameless lambda calculus (mirror)

Finally, here are 3.5 examples of nested types I haven't seen elsewhere. See if you can figure out what they do.

> data A x y = B (x y)
>            | C (A (D x) (x y))
> newtype D x y = D (y,x y)
> newtype K x = K x
> type QuestionOne = A K
>
> data E x = F x x
>          | G x (E x)
> data QuestionTwo x = Q2 (E (E x))
>
> data H x y = I
>            | J y x x (H (y,x) y)
> type L = H ()
> data QuestionThreePartA x = Q3a (L x) (L x) (L x)
> data QuestionThreePartB x = Q3b (L x) (QuestionThreePartA x)

Leibniz and Liskov

Leibniz equality of two types a and b is the proposition that in any context, one can be substituted for the other:

f a -> f b

A value of this type brings to the value level the proof that two types are equal. The only value of this type is the identity function.

The Liskov substitution principle is very similar to Leibniz equality, but only in the contravariant position: If a function takes an argument of type b and a is a subtype of b, then the function must accept an argument of type a. If f is a type constructor that uses its argument only negatively, then a is a subtype of b if there is a value of type

f b -> f a

For example, λx . x -> b uses x negatively, and any b -> b is also trivially an a -> b when a is a subtype of b. The only value of type f b -> f a is the cast function.

Let's write the kind for type constructors that use their argument negatively as * -(-)-> * rather than just * -> *, and the kind for type constructors that use their argument positively as * -(+)-> *. Then, the following terms should validate our understanding that supertyping is dual to subtyping:

dual : ∀ a:* . ∀ b:* . ∀ g: * -(+)-> * . (∀ f: * -(-)-> * .  f b -> f a) -> g a -> g b
dual |a |b |g less bot = less [λx:* . g x -> g b] (λy:g b . y:g b) bot

dual' : ∀ a:* . ∀ b:* . ∀ f: * -(-)-> * . (∀ g: * -(+)-> * . g a -> g b) -> f b -> f a
dual' |a |b |f more top = more [λx:* . f x -> f a] (λy:f a . y:f a) top

So subtyping, like type equality, can be brought to the value domain. I now have two questions:

1. Is there an analogue of F_C (mirror) for F_<: (mirror 1, mirror 2, mirror 3)?
2. Is there a problem similar to decomposition for Liskov substitutability?

Extra type safety using polymorphic types as first-level refinements

This post is literate Haskell.

I will demonstrate a new technique for using polytypes as first-level refinement types. (mirror). The goal, as usual, is for types to better express program invariants and ensure programs are safe.

I'm going to demonstrate using the risers function, as presented in Dana N. Xu's ESC/Haskell (mirror), which references Neil Mitchell's Catch.

> {-# OPTIONS -fglasgow-exts #-}
> -- The LANGUAGE pragma is usually a pain for exploratory programming.

Below are the risers functions as presented by Xu and Mitchell. They are the same function, though slightly syntacticly different. risers returns the sorted sublists of a list.

Risers has two properties that we are going to discuss:

1. None of the lists in the returned value are empty
2. If the argument is non-empty, the return value is also non-empty.

> risersXu :: (Ord t) => [t] -> [[t]]
> risersXu [] = []
> risersXu [x] = [[x]]
> risersXu (x:y:etc) =
>     let ss = risersXu (y : etc)
>     in case x <= y of
>          True -> (x : (head ss)) : (tail ss)
>          False -> ([x]) : ss
> 
> risersMitchell :: Ord a => [a] -> [[a]]
> risersMitchell [] = []
> risersMitchell [x] = [[x]]
> risersMitchell (x:y:etc) = if x <= y
>                            then (x:s):ss
>                            else [x]:(s:ss)
>     where (s:ss) = risersMitchell (y:etc)

Neither one of these functions is obviously safe. Xu uses head and tail and ESC/Haskell to create a proof of their safety. The unsafe part of Mitchell's code is the where clause, and Mitchell also presents a tool to prove this safe.

Our goal will be to write this function in a safe way, with a type signature that ensures the two properties we expect from the function. We also aim to do this without having to change the shape of the code, only the list implementation we are using.

The present unsafe operations in risersXu and risersMitchell depend on the second property of the function: non-null inputs generate non-null outputs. We could write a type for this functions using a trusted library with phantom types for branding (paper mirror). This technique (called lightweight static capabilities) can do this and much else as well, but since clients lose all ability to pattern match (even in case), risers becomes much more verbose. We could also write a type signature guaranteeing this by using GADTs. Without using one of these, incomplete pattern matching or calling unsafe head and tail on the result of the recursive call seems inevitable.

Here's another way to write the function which does away with the need for the second property on the recursive call, substituting instead the need for the first property that no lists in the return value are empty:

> risersAlt :: (Ord t) => [t] -> [[t]]
> risersAlt [] = []
> risersAlt (x:xs) = 
>     case risersAlt xs of
>       [] -> [[x]]
>       w@((y:ys):z) -> 
>           if x <= y
>           then (x:y:ys):z
>           else ([x]):w
>       ([]:_) -> error "risersAlt"

The error is never reached.

Though ensuring the second property with our usual types seems tricky, ensuring the first is not too tough:

> type And1 a = (a,[a])
> 
> risersAlt' :: Ord a => [a] -> [And1 a]
> risersAlt' [] = []
> risersAlt' (x:xs) = 
>     case risersAlt' xs of
>       [] -> [(x,[])]
>       w@(yys:z) -> 
>           if x <= fst yys
>           then (x,fst yys : snd yys):z
>           else (x,[]):w

It is now much easier to see that risers is safe: There is one pattern match and one case, and each is simple. No unsafe functions like head or tail are called. It does have three disadvantages, however.

First, the second property is still true, but the function type does not enforce it. This means that any other callers of risers may have to use incomplete pattern matching or unsafe functions, since they may not be so easy to transform. It is my intuition that it is not frequently the case that these functions are tricky to transform, but perhaps Neil Mitchell disagrees.

We could fix this by writing another risers function with type And1 a -> And1 (And1 a), but this brings us to the second problem: And1 a is not a subtype of [a]. This means that callers of our hypothetical other risers function (as well as consumers of the output from risersAlt') must explicitly coerce the results back to lists.

Finally, if we are wrong about the first property, and risers does return an empty list for some non-empty input i, then for any x, risers (x:i) is _|_, while risersAlt' (x:i) is [(x,[])]. Thus, the equivalence of these two function definitions depends on the truth of the second property on the first function, which is something we were trying to get out of proving in the first place! Of course, if we're interested in the correctness of risersAlt', rather than its equivalence with risersXu or risersMitchell, then it is not to difficult to reason about. But part of the point of this was to get they compiler to do some of this reasoning for us, without having to change the shape of the code.

Let's write more expressive signatures using something we may have noticed when using GHCi. The only value of type forall a. [a] (excluding lists of _|_s) is []. Every value of type forall a . Maybe a is Nothing, and every forall a . Either a Int has an Int in Right. Andrew Koenig noticed something similar when learning ML (archived), and the ST monad operates on a similar principle. (paper with details about ST, mirror)

> data List a n = Nil n
>               | forall r . a :| (List a r)

The only values of type forall a . List a n use the Nil constructor, and the only values of type forall n . List a n use the :| constructor.

> infixr :|
> 
> box x = x :| Nil ()
> 
> type NonEmpty a = forall n . List a n
> 
> onebox :: NonEmpty Int
> onebox = box 1
> 
> onebox' :: List Int Dummy
> onebox' = onebox
> 
> data Dummy
> 
> -- This doesn't compile
> -- empty :: NonEmpty a
> -- empty = Nil ()

NonEmpty a is a subtype of List a x for all types x.

> data Some fa = forall n . Some (fa n)
> 
> safeHead :: NonEmpty a -> a
> safeHead x = unsafeHead x where
>     unsafeHead (x :| _) = x
> 
> safeTail :: NonEmpty a -> Some (List a)
> safeTail x = unsafeTail x where
>     unsafeTail (_ :| xs) = Some xs

Unfortunately, we'll be forced to Some and un-Some some values, since Haskell does not have first-class existentials, and it takes some thinking to see that safeHead and safeTail are actually safe.

Here is a transformed version of Mitchell's risers:

> risersMitchell' :: Ord a => List a n -> List (NonEmpty a) n
> risersMitchell' (Nil x) = (Nil x)
> risersMitchell' (x :| Nil _) = box (box x)
> risersMitchell' ((x {- :: a -}) :| y :| etc) =
>     case risersMitchell' (y :| etc) {- :: NonEmpty (NonEmpty a) -} of
>       Nil _ -> error "risersMitchell'"
>       s :| ss -> if x <= y
>                  then (x :| s) :| ss
>                  else (box x) :| s :| ss

Since we can't put the recursive call in a where clause, we must use a case with some dead code. The type annotations are commented out here to show they are not needed, but uncommenting them shows that the recursive call really does return a non-empty lists, and so the Nil case really is dead code.

This type signature ensures both of the properties listed when introducing risers. The key to the non-empty-arguments-produce-non-empty-results property is that the variable n in the signature is used twice. That means applying risersMitchell' to a list with a fixed (or existential) type as its second parameter can't produce a NonEmpty list.

> risersXu' :: Ord a => List a r -> List (NonEmpty a) r
> risersXu' (Nil x) = Nil x
> risersXu' (x :| Nil _) = box (box x)
> risersXu' (((x :: a) :| y :| etc) :: List a r) = 
>     let ss = risersXu' (y :| etc)
>     in case x <= y of
>          True -> case safeTail ss of
>                    Some v -> (x :| (safeHead ss)) :| v
>          False -> (box x) :| ss

Here we see that the type annotation isn't necessary to infer that risers applied to a non-empty list returns a non-empty list. The value ss isn't given a type signature, but we can apply safeHead and safeTail. The case matching on safeTail is the pain of boxing up existentials.

This is the first version of risers with a type signature that gives us the original invariant Xu and Mitchell can infer, as well as calling no unsafe functions and containing no incomplete case or let matching. It also returns a list of lists, just like the original function, and has a definition in the same shape.

With first-class existentials, this would look just like Xu's risers (modulo built-in syntax for lists). With let binding for polymorphic values, risersMitchell' would look just like Mitchell's original risers, but be safe by construction. Let binding for polymorphic values would also allow non-trusted implementations of safeTail and safeHead to be actually safe.

For contrast, here is a GADT implementation of risers:

> data GList a n where
>     GNil :: GList a IsNil
>     (:||) :: a -> GList a m -> GList a IsCons
> 
> infixr :||
> 
> data IsNil
> data IsCons
> 
> gbox x = x :|| GNil
> 
> risersMitchellG :: Ord a => GList a n -> GList (GList a IsCons) n
> risersMitchellG GNil = GNil
> risersMitchellG (c :|| GNil) = gbox $ gbox c
> risersMitchellG (x :|| y :|| etc) =
>     case risersMitchellG (y :|| etc) of
> --    GHC complains, "Inaccessible case alternative: Can't match types `IsCons' and `IsNil'
> --    In the pattern: GNil"
> --    GNil -> error "risers" 
>       s :|| ss ->
>           if x <= y
>           then (x :|| s) :|| ss
>           else (gbox x) :|| s :|| ss

This is safe and has its safety checked by GHC. It also does not require existentials, though when using this encoding, many other list functions (such as filter) will.

Now here is a lightweight static capabilities version of risers:

> -- module Protected where
> 
> -- Export type constructor, do not export value constructor
> newtype LWSC b a = LWSC_do_not_export_me [a]
> 
> data Full
> type FullList = LWSC Full
> 
> data Any
> 
> lnil :: LWSC Any a
> lnil = LWSC_do_not_export_me []
> 
> lcons :: a -> LWSC b a -> FullList a
> lcons x (LWSC_do_not_export_me xs) = LWSC_do_not_export_me (x:xs) 
> 
> lwhead :: FullList a -> a
> lwhead (LWSC_do_not_export_me x) = head x
> 
> data Some' f n = forall a . Some' (f a n)
> 
> lwtail :: FullList a -> Some' LWSC a
> lwtail (LWSC_do_not_export_me a) = Some' (LWSC_do_not_export_me (tail a))
> 
> deal :: LWSC b a -> LWSC Any c -> (FullList a -> FullList c) -> LWSC b c
> deal (LWSC_do_not_export_me []) _ _ = LWSC_do_not_export_me []
> deal (LWSC_do_not_export_me x) _ f = 
>     case f (LWSC_do_not_export_me x) of
>       LWSC_do_not_export_me z -> LWSC_do_not_export_me z
> 
> nullcase :: LWSC b a -> c -> (FullList a -> c) -> c
> nullcase (LWSC_do_not_export_me []) z _ = z
> nullcase (LWSC_do_not_export_me x) _ f = f (LWSC_do_not_export_me x)
> 
> -- module Risers where
> 
> lbox x = lcons x lnil
> 
> risersXuLW :: Ord a => LWSC b a -> LWSC b (FullList a)
> risersXuLW x = 
>     deal x
>     lnil
>     (\z -> let x = lwhead z
>            in case lwtail z of
>                 Some' rest -> 
>                     nullcase rest
>                     (lbox (lbox x))
>                     (\yetc -> 
>                          let y = lwhead yetc
>                              etc = lwtail yetc
>                              ss = risersXuLW yetc
>                          in if x <= y
>                             then case lwtail ss of
>                                    Some' v -> lcons (lcons x $ lwhead ss) v
>                             else lcons (lbox x) ss))

There is a good bit of code that must go in the protected module, including two different functions for case dispatch. These functions are used instead of pattern matching, and make the definition of risers much more verbose, though I may not have written it with all the oleg-magic possible to make it more usable.

Out of the three, I think GADTs are still the winning approach, but it's fun to explore this new idea, especially since Haskell doesn't have traditional subtyping.

POPL 2008 and affiliated events

This week is POPL and affiliated events. I'll be at the first and third days of VMCAI, the Coq tutorial, and POPL itself. Unfortunately, I'll have to miss PEPM.