Search code examples
haskellrefinement-typeliquid-haskell

Liquid Haskell error with binary search tree deletion

I am learning liquid haskell by following this tutorial: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_05_Datatypes.html . I am currently implementing my own binary search tree deletion based on the tutorial:

data BST a = Leaf
           | Node { root  :: a
                  , left  :: BST a
                  , right :: BST a }

{-@ data BST a    = Leaf
                  | Node { root  :: a
                         , left  :: BSTL a root
                         , right :: BSTR a root } @-}

{-@ type BSTL a X = BST {v:a | v < X}             @-}
{-@ type BSTR a X = BST {v:a | X < v}             @-}
one   :: a -> BST a
one x = Node x Leaf Leaf

add                  :: (Ord a) => a -> BST a -> BST a
add k' Leaf          = one k'
add k' t@(Node k l r)
  | k' < k           = Node k (add k' l) r
  | k  < k'          = Node k l (add k' r)
  | otherwise        = t
-- My BST deletion implementation
del                   :: (Ord a) => a -> BST a -> BST a
del _ (Node _ Leaf Leaf) = Leaf
del _  Leaf           = Leaf
del x (Node k l r)
  | x < k     = Node k (del x l) r
  | x > k     = Node k l (del x r)
  | otherwise = case r of
                  Leaf -> l
                  _    -> Node k' l r'
                    where
                      k' = minKey r
                      r' = del k' r
  where
    {-@ minKey :: {v:BST a | v /= Leaf} -> a @-}
    minKey (Node key Leaf _) = key
    minKey (Node _ l _)      = minKey l

However, I get this error:

Liquid Type Mismatch
    .
    Liquid Type Mismatch
    .
    .
    The inferred type
      VV : a
      VV : a
    .
    is not a subtype of the required type
      VV : {VV : a | k'##a1Jp9 < VV}
    .
    in the context
      k'##a1Jp9 : {VV : a | $VV##6040##k_ /= $ds_d1JQM##k_
                            && $VV##6040##k_ /= $ds_d1JRr##k_
                            && $VV##6040##k_ > $ds_d1JQM##k_
                            && $VV##6040##k_ > $ds_d1JRr##k_
                            && $VV##6040##k_ >= $ds_d1JQM##k_
                            && $VV##6040##k_ >= $ds_d1JRr##k_
                            && $ds_d1JQM##k_ < $VV##6040##k_
                            && $ds_d1JRr##k_ < $VV##6040##k_
                            && Demo.Example.root $ds_d1JQN##k_ < $VV##6040##k_
                            && Demo.Example.root $lq_anf$##7205759403793208731##d1JZF##k_ < $VV##6040##k_

Why does Liquid Haskell complain about that? What should I do to fix this error?

Solution

  • As per the comments, you need to help LiquidHaskell (LH) prove that k' is the minimum element of r' and, also, that deleting the minimum element via r' = del r k' will produce an r' all of whose elements are greater than k'.

    I can't precisely duplicate your message, but I can generate a similar one by loading your code into GHCi. (The errors I get from compiling come out very different.) Anyway, I think the error message you're seeing is being generated by the line:

    _    -> Node k' l r'
                  ^^

    In the error message, the expression r' is flagged with required type:

    VV : {VV : a | k'##a1Jp9 < VV}

    and inferred type:

    VV : a

    Now, the required type of r' itself is BSTR k' a or equivalently:

    BST {v : a | k' < v}

    so clearly the type in the error message isn't referring to the type of the tree r' but rather the type of its elements:

    {v : a | k' < v}

    The symbol k' has been uniqified as k'##a1Jp9, but it's still talking about the same type here.

    So, all the error is saying is that LH needed a refinement type that ensured all the elements of r' were greater than k', but it couldn't infer that.

    That's because in r' = del k' r, there's nothing in the refinement type of del that tells LH that deleting the minimum element from the tree r will yield a tree whose elements are greater than the deleted element.

    This may be obvious to you and me, but LH needs to be led by explicit refinement types to this conclusion.

    It's difficult to address this by adding a refinement type to del because in general a deletion del x t doesn't guarantee that the elements of t are bigger than x. You could write a new function delMin with the same definition as del but with a refinement type that only accepts the minimum element for deletion and returns a tree that's known to have elements bigger than this minimum. You'd also need to modify the refinement type of minKey since its current refined type has no post-condition on the returned value that provides evidence it's the minimum element.

    But this seems pretty difficult.

    It's actually easier to write a single, recursive function that simultaneously extracts a minimum element and returns the remaining tree, using a refinement type that specifically states the remaining tree's elements are all bigger than the minimum. Normally, this function would have a refined type like:

    {-@ extractMin :: BST a -> Maybe (m::a, BSTR a m) @-}    -- (*)

    where the Maybe here is to allow for extractMin Leaf to return Nothing. (That's easier than trying to use a something like {v : BST a | v /= Leaf}.)

    Unfortunately, the syntax (*) doesn't work due to a bug in LH when dependent tuples and aliases are combined. You'll get some message about a "Sort Error in Refinement" and an "Unbound symbol m".

    Instead, you need to manually expand the alias:

    {-@ extractMin :: BST a -> Maybe (m::a, BST {v:a | m<v}) @-}

    If you write an implementation of extractMin, you can use that to completely replace the minKey/del combo in the definition of del.

    SPOILERS FOLLOW

    .

    .

    .

    .

    With this refinement type, you can define extractMin recursively as:

    {-@ extractMin :: BST a -> Maybe (m::a, BST {v:a | m<v}) @-}
extractMin :: BST a -> Maybe (a, BST a)
extractMin Leaf = Nothing
extractMin (Node k l r) = case extractMin l of
  Nothing     -> Just (k, r)
  Just (m, l') -> Just (m, Node k l' r)

    Now, you can use extractMin in del to replace the minKey/del combination:

    del                   :: (Ord a) => a -> BST a -> BST a
del _ (Node _ Leaf Leaf) = Leaf
del _  Leaf           = Leaf
del x (Node k l r)
  | x < k     = Node k (del x l) r
  | x > k     = Node k l (del x r)
  | otherwise = case extractMin r of
      Nothing -> l
      Just (m, r') -> Node m l r'

    LH should be able to type check that correctly. The full revised code is:

    data BST a = Leaf
           | Node { root  :: a
                  , left  :: BST a
                  , right :: BST a }
             deriving (Show)

{-@ data BST a    = Leaf
                  | Node { root  :: a
                         , left  :: BSTL a root
                         , right :: BSTR a root } @-}

{-@ type BSTL a X = BST {v:a | v < X}             @-}
{-@ type BSTR a X = BST {v:a | X < v}             @-}

one   :: a -> BST a
one x = Node x Leaf Leaf

add                  :: (Ord a) => a -> BST a -> BST a
add k' Leaf          = one k'
add k' t@(Node k l r)
  | k' < k           = Node k (add k' l) r
  | k  < k'          = Node k l (add k' r)
  | otherwise        = t

del                   :: (Ord a) => a -> BST a -> BST a
del _ (Node _ Leaf Leaf) = Leaf
del _  Leaf           = Leaf
del x (Node k l r)
  | x < k     = Node k (del x l) r
  | x > k     = Node k l (del x r)
  | otherwise = case extractMin r of
      Nothing -> l
      Just (m, r') -> Node m l r'

{-@ extractMin :: BST a -> Maybe (m::a, BST {v:a | m<v}) @-}
extractMin :: BST a -> Maybe (a, BST a)
extractMin Leaf = Nothing
extractMin (Node k l r) = case extractMin l of
  Nothing     -> Just (k, r)
  Just (m, l') -> Just (m, Node k l' r)

main = do
  let t = add 6 $ add 4 $ one 5
  print t
  let t4 = del 4 t
      t5 = del 5 t
      t6 = del 6 t
  print (t4, t5, t6)