Simplifying pattern matching with do notation

[Srdjan Stipic]

I am learning Idris and I implemented the following function:

total

elemInTree : DecEq a => (x : a) -> (t : Tree a) -> Maybe (ElemTree x t)

elemInTree _ Leaf = Nothing

elemInTree x (Node l y r) with (decEq x y)

  elemInTree x (Node l x r) | Yes _ = Just hereET

  --- I want to simplify the following line ---

  elemInTree x (Node l y r) | No _ = case (elemInTree x l, elemInTree x r) of

    (Nothing, Nothing) => Nothing

    (Just p, _) => Just (leftET p)

    (_, Just p) => Just (rightET p)

Can I simplify the code with do notation or with [| |] brackets?

[David Christiansen]

Hi Srdjan,

> elemInTree x (Node l x r) | Yes _ = Just hereET

Note that the above line may not work in a newer Idris. I think it
exploits a now-fixed bug in the linearity checker, where x occurring
twice didn't need to be justfied by the presence of something whose
type guaranteed their equality. You should have to say "Yes refl" to
the right of the |, I think, to justify the repeated x binding in the
pattern.

Someone please correct me if I'm wrong here!

> --- I want to simplify the following line ---
> elemInTree x (Node l y r) | No _ = case (elemInTree x l, elemInTree x r)
> of
> (Nothing, Nothing) => Nothing
> (Just p, _) => Just (leftET p)
> (_, Just p) => Just (rightET p)
>
> Can I simplify the code with do notation or with [| |] brackets?

I don't think that do notation or idiom brackets are what you want
here, but I believe that you can use the <|> operator from the type
class Alternative to get rid of the case.

Something like:

elemInTree x (Node l y r) | No _ = elemInTree x l <|> elemInTree x r

This is based on the following instance from Prelude.idr:

instance Alternative Maybe where
empty = Nothing

(Just x) <|> _ = Just x
Nothing <|> v = v

Hope this is handy.

/David

[Srdjan Stipic]

Looks useful. Thanks.

> --
> You received this message because you are subscribed to a topic in the Google Groups "Idris Programming Language" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/idris-lang/q6XR7ZEfRco/unsubscribe?hl=en.
> To unsubscribe from this group and all its topics, send an email to idris-lang+...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[Edwin Brady]

On 10 Apr 2013, at 16:42, David Christiansen <da...@davidchristiansen.dk> wrote:

> Hi Srdjan,
>
>> elemInTree x (Node l x r) | Yes _ = Just hereET
>
> Note that the above line may not work in a newer Idris. I think it
> exploits a now-fixed bug in the linearity checker, where x occurring
> twice didn't need to be justfied by the presence of something whose
> type guaranteed their equality. You should have to say "Yes refl" to
> the right of the |, I think, to justify the repeated x binding in the
> pattern.
>
> Someone please correct me if I'm wrong here!

No, that's correct. The above line should never have worked. Sorry folks!

I'll be updating the hackage version soon, now that master builds on Windows again.

Edwin.