NoRedInk / haskell-verify-examples

WIP
BSD 3-Clause "New" or "Revised" License
0 stars 0 forks source link

Experiment: Help todo #27

Closed stoeffel closed 3 years ago

stoeffel commented 3 years ago
-- | Fold over the key-value pairs in a dictionary from highest key to lowest key.
--
-- @
-- import qualified Dict
--
-- data User = User { age :: Int }
--
-- getAges :: Dict.Dict Int User -> List Int
-- getAges users =
--   Dict.foldr addAge [] users
--
-- addAge :: Int -> User -> List Int -> List Int
-- addAge _ user ages =
--   age user : ages
-- @
--
-- The users
--
-- @
-- users :: Dict.Dict Int User
-- users = Dict.fromList [(1,  User 28 ), (2,  User 19 ), (3, User 32 )]
-- @
--
-- ? getAges users

The comment above will output:

nri-prelude/src/Dict.hs:222
  217: -- @
  218: -- users :: Dict.Dict Int User
  219: -- users = Dict.fromList [(1,  User 28 ), (2,  User 19 ), (3, User 32 )]
  220: -- @
  221: --
✗ 222: -- ? getAges users
  223: foldr :: (k -> v -> b -> b) -> b -> Dict k v -> b
  224: foldr = Data.Map.Strict.foldrWithKey
  225:
  226: -- | Keep only the key-value pairs that pass the given test.
  227: filter :: (comparable -> v -> Bool) -> Dict comparable v -> Dict comparable v
This example evaluates to the following value
"[28,19,32]"
stoeffel commented 3 years ago

@micahhahn I've made a little experiment. What do you think?

micahhahn commented 3 years ago

I like this! It's maybe a little awkward having this as a binary operator ==? when we only care about one of the sides... perhaps we could use a prefix instead. Something like

>? getAges users

stoeffel commented 3 years ago

oh, yes I like this! how about we just make >? syntactic sugar for ==? (). Because I think we need to know the resulting type in order to render it properly. https://hackage.haskell.org/package/hint-0.9.0.4/docs/Language-Haskell-Interpreter.html

micahhahn commented 3 years ago

Sure, I don't know if it could strictly be syntax sugar for ==? () because that would mean >? getAges users would desugar to ==? () getAges users right?

Could we just have something in the runtime like the following?

helpTodo :: (Prelude.Show a) => a -> Verified

And then have >? getAges users desugar to helpTodo $ getAges users?