Search code examples
syntactic-sugarapplicativeidris

Is it possible to use a conditional statement in an Idiom Bracket in Idris?

An expression like the following is perfectly valid in Idris:

 let x = Just 5 in let y = Just 6 in [|x / y|]

Could someone write an expression like the following?

let x = Just 5 in let y = Just 6 in [| if x == 0 then 0 else y|]

I can't seem to get it to compile.

Solution

  • I was able to get this working by taking care of two problems:

    1. if _ then _ else _ doesn't seem to propagate the idiom bracket to its subexpressions

    2. The default definition of if _ then _ else _ is (of course) lazy in its two branches, and Lazy' LazyEval doesn't seem to lift instances.

    Once these two were worked around, I was able to get it working in an idiom bracket. Note however that this wouldn't work for an applicative where taking both branches has an observable effect.

    strictIf : Bool -> a -> a -> a
strictIf True t e = t
strictIf False t e = e

syntax "if" [b] "then" [t] "else" [e] = strictIf b t e

test : Maybe Float
test = let x = Just 5 
           y = Just 6
       in [| if [| x == pure 0 |] then [|0|] else y |]