!-notation and if result in unexpected behavior

[kevinboulain]

Hi,

I did a quick search in the existing issues and I couldn't find anything (maybe because I'm lacking the correct terms?), so sorry if it has already been reported.

In the following example (that has been reduced as much as I could), a function bX has been implemented in four different but equivalent ways. It does a simple search of the "b" string in a list of strings and if found, return it wrapped in a Maybe.

b1 & b2 pattern match on the list constructor to test for "b" and use the do-notation and the !-notation respectively. b3 & b4 use the if ... then ... else syntax to test for "b" and use the do-notation and the !-notation respectively.

Unfortunately, b4 returns Nothing and looks like a bug to me (or am I missing something obvious? :)).

The test program:

b1 : List String -> Maybe String
b1 []            = Nothing
b1 (x@"b" :: xs) = Just x
b1 (x :: xs)     = do y <- b1 xs
                      pure y

b2 : List String -> Maybe String
b2 []            = Nothing
b2 (x@"b" :: xs) = Just x
b2 (x :: xs)     = let y = !(b2 xs)
                   in Just y

b3 : List String -> Maybe String
b3 []        = Nothing
b3 (x :: xs) = if "b" == x
                  then Just x
                  else do y <- (b3 xs)
                          pure y

b4 : List String -> Maybe String
b4 []        = Nothing
b4 (x :: xs) = if "b" == x
                  then Just x
                  else let y = !(b4 xs)
                       in Just y

testb : String -> (List String -> Maybe String) -> IO ()
testb name b = do putStrLn name
                  putStrLn $ show $ b ["a", "b", "c"]

main : IO ()
main = do testb "b1" b1
          testb "b2" b2
          testb "b3" b3
          testb "b4" b4

And its output:

b1
Just "b"
b2
Just "b"
b3
Just "b"
b4
Nothing

Tested with the following idris --version:

• 1.2.0
• 1.2.0-git:ab9a0fd4

Regards.

[melted]

Hmmm... looks like it's lifted out of the if.

[david-christiansen]

Right, it gets lifted to the nearest enclosing binder. This is a bit of a confusing thing sometimes!

On Fri, Mar 30, 2018, 13:51 Niklas Larsson notifications@github.com wrote:

Hmmm... looks like it's lifted out of the if.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/idris-lang/Idris-dev/issues/4395#issuecomment-377620301, or mute the thread https://github.com/notifications/unsubscribe-auth/AAHCgjZ4mEIxUTk8Wv_I-Mvl-V2yiCPTks5tjprDgaJpZM4S9rd8 .

[kevinboulain]

I can definitely understand it better under this form:

b4 : List String -> Maybe String
b4 []        = Nothing
b4 (x :: xs) = if "b" == x
                  then Just x
                  else Just !(b4 xs)

b5 : List String -> Maybe String
b5 []        = Nothing
b5 (x :: xs) = ifThenElse ("b" == x) (Just x) (Just !(b5 xs))

b6 : List String -> Maybe String
b6 []        = Nothing
b6 (x :: xs) = ifThenElse ("b" == x) (Just x) (do pure !(b6 xs))

--dumpcases gives the same output for both b4 & b5 because if ... then ... else is merely some syntactic sugar for ifThenElse:

Main.b5 {arg_0} =
  case ({arg_0}) of
  | Prelude.List.::({in_1}, {in_2}) => case (Main.b5({in_2})) of
  .   | Prelude.Maybe.Just({in_4}) => case (LStrEq("b", {in_1})) of
  .   .   | 0 => Prelude.Maybe.Just({in_4})
  .   .   | _ => Prelude.Maybe.Just({in_1})
  .   | Prelude.Maybe.Nothing() => Prelude.Maybe.Nothing()
  | Prelude.List.Nil() => Prelude.Maybe.Nothing()

Maybe a simple warning in the documentation regarding mixing syntax extensions (which don't have scopes?) and !-notation will be good enough? Since it already tell a subexpression !expr will lift expr as high as possible within its current scope.

I must admit it feels obvious once you know it (feel free to close this issue if you think so too) :)