search

ucsd-progsys / liquidhaskell-tutorial

Tutorial for LiquidHaskell
https://ucsd-progsys.github.io/liquidhaskell-tutorial/
MIT License
75 stars 27 forks source link

Fix bool value on chapter 6 #118

Closed f7deleon closed 1 year ago

f7deleon commented 2 years ago

In the following section:

<div class="hwex" id="Safe Head">
Write down a specification for `null` such that `safeHead`
is verified. Do *not* force `null` to only take non-empty inputs,
that defeats the purpose. Instead, its type should say that it
works on *all* lists and returns `True` *if and only if* the input
is non-empty.
</div>

\hint You may want to refresh your memory about implies `==>`
and `<=>` from the [chapter on logic](#semantics).

\begin{code}
safeHead      :: [a] -> Maybe a
safeHead xs
  | null xs   = Nothing
  | otherwise = Just $ head xs

{-@ null      :: [a] -> Bool @-}
null []       =  True
null (_:_)    =  False
\end{code}

I think that "all list and return True" should be "all list and returns False" given the current definition of null

ranjitjhala commented 2 years ago

Oops thanks for catching that! Wouldn’t it be simpler to replace “non-empty” with “empty”?

On Sun, Mar 13, 2022 at 12:08 PM Felipe de León @.***> wrote:

In the following section:

Write down a specification for `null` such that `safeHead` is verified. Do *not* force `null` to only take non-empty inputs, that defeats the purpose. Instead, its type should say that it works on *all* lists and returns `True` *if and only if* the input is non-empty.

\hint You may want to refresh your memory about implies ==>and <=> from the chapter on logic. \begin{code}safeHead :: [a] -> Maybe a safeHead xs | null xs = Nothing | otherwise = Just $ head xs

{-@ null :: [a] -> Bool @-}null [] = Truenull (:) = False\end{code}

I think that "all list and return True" should be "all list and returns False" given the current definition of null

You can view, comment on, or merge this pull request online at:

https://github.com/ucsd-progsys/liquidhaskell-tutorial/pull/118 https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell-2Dtutorial_pull_118&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=_iNsePBRcSxdR3sI4PVJYa4PWLfUJOHWmPPTkiSwhbLizLCxxEKPYhRgWgYZ7QL0&s=Uo-hEzxUqawAIQcPQsdKEQNVVlIZ6WO9Si1ieIV634A&e= Commit Summary

File Changes

(1 file https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell-2Dtutorial_pull_118_files&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=_iNsePBRcSxdR3sI4PVJYa4PWLfUJOHWmPPTkiSwhbLizLCxxEKPYhRgWgYZ7QL0&s=N80e1wlVQ5m92xbNITlwY1uBuHMRx97gvBoxcS7HuOM&e= )

Patch Links:

— Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell-2Dtutorial_pull_118&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=_iNsePBRcSxdR3sI4PVJYa4PWLfUJOHWmPPTkiSwhbLizLCxxEKPYhRgWgYZ7QL0&s=Uo-hEzxUqawAIQcPQsdKEQNVVlIZ6WO9Si1ieIV634A&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OAHW3HKB44U3U3KR43U7Y4MDANCNFSM5QTXANHQ&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=_iNsePBRcSxdR3sI4PVJYa4PWLfUJOHWmPPTkiSwhbLizLCxxEKPYhRgWgYZ7QL0&s=6WVXhYefx9L3i-fClw8zGOdptZjj5cdXt4lVxtDCdHc&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=_iNsePBRcSxdR3sI4PVJYa4PWLfUJOHWmPPTkiSwhbLizLCxxEKPYhRgWgYZ7QL0&s=IwqM5esAuVA_7XzXz2WQS0w53YlXBQWuguT9YdXzSJ0&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=_iNsePBRcSxdR3sI4PVJYa4PWLfUJOHWmPPTkiSwhbLizLCxxEKPYhRgWgYZ7QL0&s=WPy5XQHh-aM63FmpeQw8ShOeDU-4Vi6YC2N6ebREuOE&e=.

You are receiving this because you are subscribed to this thread.Message ID: @.***>