On Jan 4, 2008 5:15 AM, Simon Peyton-Jones wrote:

| > The following won't compile for me | > | > isnull :: (forall a . [a]) -> Bool | > isnull ([] :: forall b . [b]) = True | > | > Couldn't match expected type `forall b. [b]' | > against inferred type `[a]' | > In the pattern: []

This is a pretty strange thing to do, to match a polymorphic argument against a data constructor. I guess you'd expect this to work too, perhaps?

f :: forall a. (forall b. Either a b) -> a f (Left x) = x

I grant that arguably these should work, but I think it'd be quite tricky to make it do so, because it'd involve re-generalising in the pattern. Furthermore, I can't see any use for it. Just remove the type signature from the pattern.

One could argue that it's a bad sign that the pattern typechecker should have difficulty with this. But until it turns out to be important I'm not going to lose sleep over it!

This is literate Haskell. It's in the LaTeX style, since my mail reader won't change the quoting mark from '>'. It is not a valid LaTeX file. My reason for wanting pattern matching on values of polymorphic types is a kind of first-level refinement types. I'm going to demonstrate using the "risers" function, as presented in Dana N. Xu's ESC/Haskell (http://research.microsoft.com/Users/simonpj/papers/verify/escH-hw.ps or http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps ), which references Neil Mitchell's Catch (http://www-users.cs.york.ac.uk/~ndm/catch/ ). I'll also be referencing an example from Tim Freeman's thesis on refinement types for ML (http://www.cs.ucla.edu/~palsberg/tba/papers/freeman-thesis94.pdf ) \begin{code} {-# OPTIONS -fglasgow-exts #-} -- The LANGUAGE pragma is usually a pain for exploratory programming. \end{code} This is the risers function, as presented by Xu. It returns the sorted sublists of a list. None of the lists in the return value are empty, and if the argument is non-empty, the return value is also non-empty. \begin{code} 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 \end{code} Xu uses head and tail. These are safe here by a proof created by ESC/Haskell. Here is the risers function according to Mitchell: \begin{code} 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) \end{code} The unsafe part here is the pattern in the where clause. Mitchell presents a tool to prove this safe. These unsafe operations 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 (http://okmij.org/ftp/Computation/lightweight-dependent-typing.html ). This technique (called lightweight static capabilities) can do this and much else, as well, but clients lose all ability to pattern match (even in case). We could also write a type signature guaranteeing this by using GADTs. Without either 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 second property on the recursive call, substituting instead the need for the first property, that no lists in the return value are empty: \begin{code} 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" \end{code} The error is never reached. Though ensuring the second property with our usual types seems tricky, ensuring the first is not too tough: \begin{code} 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 \end{code} 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 two disadvantages. 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. Let's write more expressive signatures using the principle from my original question. \begin{code} data List a n = Nil n | forall r . a :| (List a r) \end{code} [] is the only value of type forall a . [a], assuming no values of type forall a . a. Similarly, 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. \begin{code} 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 () \end{code} NonEmpty a is a subtype of List a x for all types x. Now we get to the disappointing part of the show in which I pine for first-class existentials and pattern matching on polymorphic values. \begin{code} data Some f a = forall n . Some (f a 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 \end{code} Unfortunately, we'll be forced to Some and un-Some some values, and it takes some thinking to see that safeHead and safeTail are actually safe. \begin{code} 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 \end{code} 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. \begin{code} risersXu' :: Ord a => List a r -> List (NonEmpty a) r risersXu' (Nil x) = Nil x risersXu' (x :| Nil _) = box (box x) risersXu' (x :| y :| etc) = 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 \end{code} 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. With first-class existentials, this would look just like Xu's risers (modulo built-in syntax for lists). With pattern matching for polymorphic values, risersMitchell' would look just like Mitchell's original risers, but be safe by construction. Pattern matching for polymorphic values would also allow non-trusted implementations of safeTail and safeHead to be actually safe. Since GADTs and lightweight static capabilities are already available, I do not know how compelling this example is. I think there are much more compelling examples for first-class existentials. In any case, here's one more example, this one from Freeman's thesis on refinement types. We create a type of boolean expressions with variables. We can evaluate terms without any free variables, so we distinguish them using the trick above. Unfortunately, this time the constructor restriction isn't just at the top level, but all the way down. We must, therefore, parameterize the recursion in the data type. \begin{code} data BoolExp' a r = And r r | Or r r | Not r | Tru | Fals | Var a String newtype Mu' f = Mu' (forall a . f a (Mu' f)) type Ground = Mu' BoolExp' data Mu f = forall a . Mu (f a (Mu f)) type BoolExp = Mu BoolExp' type Base = forall a r . BoolExp' a r eval :: Ground -> Base eval (Mu' x) = case x of And y z -> case (eval y,eval z) of (Tru,x) -> x _ -> Fals Or y z -> case (eval y,eval z) of (Fals,x) -> x _ -> Tru Not y -> case eval y of Tru -> Fals _ -> Tru Tru -> Tru Fals -> Fals _ -> error "eval" \end{code} The error in eval is never reached. Unfortunately, Ground is not a subtype of BoolExp, so this seems like a less compelling example.

On Jan 7, 2008 1:37 AM, Simon Peyton-Jones wrote:

Sadly, it's not true in Haskell, is it? (error "urk") : [] also has type (forall a. [a]).

It is a bit sad, but I think that's The Curse of The _|_, which infects any attempt to add static assurance.

It's nicer if static properties have static witnesses, and involve no runtime activity.

Maybe The Curse doesn't infect everything. What methods of assuring static properties in GHC have static witnesses? I think no: GADTs, lightweight static capabilities, forall a . [a] trick, nested/non-regular types I think yes: associated types, class constraints

You have a type (NonEmpty (NonEmpty a)). If you expand that out, I think you get a forall n1. List (forall n2. List a n2) n1 So you're instantiating the element type of the outer list with a polytype, which requires impredicativity too, not just existentials!

It's true, but that seems to work without a hiccup right now Jim