Ch 5: Sparse's 'fromList' works even if it just returns Nothing

[mpdairy]

I have the Sparse datatype and I made a fromList conversion function (named sparseFromList) that works in Haskell and passes the check with Liquid Haskell:

data Sparse a = SP { spDim   :: Int
                   , spElems :: [(Int, a)] }
                deriving (Eq, Ord, Show)

{-@ data Sparse a = SP { spDim :: Nat, spElems :: [(Btwn 0 spDim, a)] } @-}

{-@ type SparseN a N = {sp:Sparse a | spDim sp == N} @-}

sparseFromList :: Int -> [(Int, a)] -> Maybe (Sparse a)
sparseFromList dim elts = SP dim <$> traverse f elts
  where
    f (i, x)
      | i >= 0 && i < dim = Just (i, x)
      | otherwise = Nothing

{-@ test1 :: SparseN String 3 @-}
test1     = fromJust $ sparseFromList 3 [(0, "cat"), (2, "mouse")]

But then, just to make sure it was actually checking sparseFromList, I made it always return Nothing and LH still said it was OK.

Then I decided to make my own fromJust instead of importing it, with a LH check that it's actually a Just:

{-@ measure isJust @-}
isJust :: Maybe a -> Bool
isJust (Just _) = True
isJust Nothing = False

{-@ fromJust :: {m:Maybe a | isJust m} -> a @-}
fromJust :: Maybe a -> a
fromJust (Just a) = a
fromJust Nothing = die "fromJust Nothing"

And now I get a LH error that makes it look like it can't figure out that sparseFromList returns a Just in this case.

197 | test1     = fromJust $ sparseFromList 3 [(0, "cat"), (2, "mouse")]
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : (GHC.Maybe.Maybe (Blaze.Liquid.Ex5.Sparse [GHC.Types.Char]))

   not a subtype of Required type
     VV : {VV : (GHC.Maybe.Maybe (Blaze.Liquid.Ex5.Sparse [GHC.Types.Char])) | isJust VV}

[ranjitjhala]

This is because your output type for sparseFromList does not specify that the result is indeed a Just; to do so, you may want to refine the spec to something like:

{-@ sparseFromList :: Int -> [(Int, a)] -> {v:Maybe (Sparse a) | isJust v} @-}

On Tue, Sep 10, 2019 at 7:51 PM Matt Parker notifications@github.com wrote:

I have the Sparse datatype and I made a fromList conversion function (named sparseFromList) that works in Haskell and passes the check with Liquid Haskell:

data Sparse a = SP { spDim :: Int , spElems :: [(Int, a)] } deriving (Eq, Ord, Show)

{-@ data Sparse a = SP { spDim :: Nat, spElems :: [(Btwn 0 spDim, a)] } @-}

{-@ type SparseN a N = {sp:Sparse a | spDim sp == N} @-}

sparseFromList :: Int -> [(Int, a)] -> Maybe (Sparse a) sparseFromList dim elts = SP dim <$> traverse f elts where f (i, x) | i >= 0 && i < dim = Just (i, x) | otherwise = Nothing

{-@ test1 :: SparseN String 3 @-} test1 = fromJust $ sparseFromList 3 [(0, "cat"), (2, "mouse")]

But then, just to make sure it was actually checking sparseFromList, I made it always return Nothing and LH still said it was OK.

Then I decided to make my own fromJust instead of importing it, with a LH check that it's actually a Just:

{-@ measure isJust @-} isJust :: Maybe a -> Bool isJust (Just _) = True isJust Nothing = False

{-@ fromJust :: {m:Maybe a | isJust m} -> a @-} fromJust :: Maybe a -> a fromJust (Just a) = a fromJust Nothing = die "fromJust Nothing"

And now I get a LH error that makes it look like it can't figure out that sparseFromList returns a Just in this case.

197 | test1 = fromJust $ sparseFromList 3 [(0, "cat"), (2, "mouse")] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Inferred type VV : (GHC.Maybe.Maybe (Blaze.Liquid.Ex5.Sparse [GHC.Types.Char]))

not a subtype of Required type VV : {VV : (GHC.Maybe.Maybe (Blaze.Liquid.Ex5.Sparse [GHC.Types.Char])) | isJust VV}

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/85?email_source=notifications&email_token=AAMS4OHE5QTDM5JSQ6RHPQ3QJBMJPA5CNFSM4IVOTBH2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HKTE4BQ, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4ODPFZHTXL7JGIX7LLLQJBMJPANCNFSM4IVOTBHQ .

[mpdairy]

Ok, I figured out how to do it where sparseFromList can return a Just or Nothing and it's still specified in the type signature. But I guess since you'd only ever call sparseFromList on data received dynamically, it was sort of pointless to make it be able to check at compile time. At least I learned a lot :slightly_smiling_face:

data SparseElems a = SENil
                   | SECons Int a (SparseElems a)
                   deriving (Eq, Ord, Show)

{-@ measure maxIndex @-}
maxIndex :: SparseElems a -> Int
maxIndex SENil = 0
maxIndex (SECons i _ xs) = let m = maxIndex xs in
  if m > i then m else i

{-@ measure minIndex @-}
minIndex :: SparseElems a -> Int
minIndex SENil = 0
minIndex (SECons i _ xs) = let m = minIndex xs in
  if m < i then m else i

{-@ sparseElemsToList :: se:SparseElems a -> [({n:Int | n <= maxIndex se && n >= minIndex se}, a)] @-}
sparseElemsToList :: SparseElems a -> [(Int, a)]
sparseElemsToList SENil = []
sparseElemsToList (SECons i a xs) = (i,a):sparseElemsToList xs

{-@ sparseFromList :: d:Nat -> elems:SparseElems a
                   -> {v:Maybe (SparseN a d) | isJust v <=> (maxIndex elems < d && minIndex elems >= 0) }
@-}
sparseFromList :: Int -> SparseElems a -> Maybe (Sparse a)
sparseFromList dim elts
  | maxIndex elts < dim && minIndex elts >= 0= Just $ SP dim (sparseElemsToList elts)
  | otherwise = Nothing