syntactic-sugar - Idris のイディオム ブラケットで条件ステートメントを使用することは可能ですか?

Question

次のような式は、Idris では完全に有効です。

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

誰か次のような式を書いてくれませんか?

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

私はそれをコンパイルすることができないようです。

Answer 1

2つの問題に対処することで、これを機能させることができました。

1. if _ then _ else _イディオムブラケットをその部分式に伝播していないようです

2. のデフォルトの定義if _ then _ else _は (もちろん) 2 つのブランチで怠惰であり、Lazy' LazyEvalインスタンスを持ち上げないようです。

これら 2 つが回避されると、イディオム ブラケットで動作させることができました。ただし、これは、両方の分岐を取ると目に見える効果があるアプリケーションでは機能しないことに注意してください。

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 |]