Agda中的Haskell部分

在Haskell中,我们可以对二进制操作?进行分区以获得两个函数 (x ?)和(? y).据我所知,我们可以通过写作来模仿第一部分,_?_ x但我们可以干净利落地完成第二部分吗？

示例 这里我定义了已经分段的Agda库版本,Function._$_以执行上面提到的第二部分.但是,它在下面我想要的情况下不起作用,我不知道为什么.欢迎任何见解!

$ : ? {a b} {A : Set a} {B : A ? Set b} ? (x : A) ? ((y : A) ? B y) ? B x
$ x = ? f ? f x

success-usage : ?{a b}{A : Set a}{B : Set b} ? A ? (A ? B) ? B
success-usage x = $ x

failed-usage : ?{A : Set} ? (?{B : Set} ? B) ? (?{B : Set} ? B ? A) ? A
failed-usage {A} bs = $ (bs {A})
-- works : ? {A} bs f ? $ (bs {A}) f

谢谢 :-)

Agda(2.4.3)的开发版本有以下部分:

open import Function

ok? : ?{a b}{A : Set a}{B : Set b} ? A ? (A ? B) ? B
ok? x = _$ x

ok? : ?{A : Set} ? (?{B : Set} ? B) ? (?{B : Set} ? B ? A) ? A
ok? {A} bs = _$ (bs {A})

ok? : ?{a b}{A : Set a}{B : Set b} ? (A ? B) ? A ? B
ok? f = f $_