Type of `dropWhile`

[NorfairKing]

The type of dropWhile could be more specific:

{-@ measure head :: forall a. { es : [a] | len es >= 1 } -> a @-}
{-@ assume head :: { es : [a] | len es >= 1 } -> { e : a | e == head es } @-}
{-@ assume dropWhile
    :: p : (a -> Bool)
    -> ls : [a]
    -> { o : [a] | len o <= len ls && len o >= 1 ==> not (Prop (p (head o))) }
@-}

This way we can prove the following safe:

main :: IO ()
main =
  if head (dropWhile ((==) 3) [1..3]) == 3
  then return ()
  else error "Not going to happen"

Unfortunately there are two problems:

1. Liquid Haskell complains that es is unbound in the new liquid signature for head.
2. == only works for Eq types, so I'm not sure how to specify e == head es.

Feedback/help is welcome.

[ranjitjhala]

Hi @NorfairKing,

Thanks for this example (& sorry for the delay!)

Unfortunately, dropWhile is rather more complicated, and you can't do it "directly" in this style due to various current implementation limitations.

1. The es thing is (I believe) solved in develop ... earlier you couldn't have refinements in measures...
2. The real hassle is that not (Prop (p (head o))) is currently not supported, primarily as you cannot directly use the higher order predicate p inside the specifications. (In general, you can only use measures + arithmetic in specifications).

So, instead you need to define "lists whose head satisfies some property p" which we can do like so:

{-@ data List a <p :: a -> Prop> = Emp
                                 | (:::) { hd :: a<p>
                                         , tl :: List a }
  @-}

After which, dropWhile looks like

{-@ dropWhile :: forall <p :: a -> Prop, w :: a -> Bool -> Prop>.
                   (Witness a p w) =>
                   (x:a -> Bool<w x>) -> List a -> List <p> a
  @-}
dropWhile :: (a -> Bool) -> List a -> List a
dropWhile f (x:::xs)
  | not (f x)    = x ::: xs
  | otherwise    = dropWhile f xs
dropWhile f Emp  = Emp

{-@ bound witness @-}
witness :: Eq a => (a -> Bool) -> (a -> Bool -> Bool) -> a -> Bool -> a -> Bool
witness p w = \ y b v -> (not b) ==> w y b ==> (v == y) ==> p v

The strange Witness thing says that

• IF predicate f x returns a Bool that is False
• THEN then x satisfies the predicate p

We then have that the output of dropWhile has a head that satisfies p, after which the rest follows.

In short: this is rather clunky It would be much nicer to support a spec like yours; and perhaps we can figure out how to get there...

See this for details

[NorfairKing]

Thank you for the response!