idris-lang / Idris2

A purely functional programming language with first class types

https://idris-lang.org/

Other

2.46k stars 368 forks source link

dont execute effect in toMaybeT if condition is not met #3274

Closed joelberkeley closed 2 months ago

joelberkeley commented 2 months ago

Description

I'm not sure about this, but is it a bug that

toMaybeT : Functor m => Bool -> m a -> MaybeT m a
toMaybeT b m = MkMaybeT $ map (\a => toMaybe b a) m

always executes its m effect.

If so, this fixes that.

See also

toMaybe : Bool -> Lazy a -> Maybe a
toMaybe True  j = Just j
toMaybe False _ = Nothing

Should this change go in the CHANGELOG?

[x] If this is a fix, user-facing change, a compiler change, or a new paper implementation, I have updated CHANGELOG_NEXT.md (and potentially also CONTRIBUTORS.md).

joelberkeley commented 2 months ago

I think it was right before, but I'll change the docstring to explain why