Haskell Agda 中的部分

Question

在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

谢谢你:-)

Answer 1

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 $_

Haskell Agda 中的部分

Haskell Sections in Agda

haskell

agda