Можно ли использовать условный оператор в Idiom Bracket в Idris?

Question

Выражение вроде следующего вполне допустимо в Идрис:

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

я смог получить эту работу, заботясь о двух проблемах:

1. if _ then _ else _, кажется, не распространяются на идиомы кронштейн его подвыражения

2. определение по умолчанию if _ then _ else _ является (конечно) ленив в своих двух ветвях, а Lazy' LazyEval, похоже, не поднимает экземпляры.

После того, как эти две части были обработаны, я смог заставить его работать в скобке идиомы. Обратите внимание, однако, что это не сработало бы для аппликативного применения, когда взятие обеих ветвей имеет наблюдаемый эффект.

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