2
像下面的表达式是非常有效的在伊德里斯:是否可以在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|]
我似乎无法得到它编译。
像下面的表达式是非常有效的在伊德里斯:是否可以在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|]
我似乎无法得到它编译。
我能采取的两个问题护理得到这个工作:
if _ then _ else _
似乎并不成语支架传播到其子表达式
的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 |]
哦,天哪!我花了一段时间才弄清楚这实际上是如何工作的。最后一个表达式看起来好像不应该首先编译,但我想我现在明白它的工作原理。 – jedesah
我会把它当作“不是真的”。因为我认为在这一点上Idiom Brackets是不值得的。感谢您花时间回答我的问题! – jedesah