Haskell Sections in Agda

4
votes

In Haskell we can section a binary operation ⊕ to obtain two functions (x ⊕) and (⊕ y). As far as I know, we can mimic the first section by writing _⊕_ x but can we do so cleanly for the second section?

Example Here I define an already sectioned version of Agda library's Function._$_ to perform the second section as mentioned above. However, it does not work in my desired case below and I do not know why. Any insight is welcome!

$ : ∀ {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

Thank-you :-)

1
haskellagda
Note that whatever you end up using for sections, you won't be able to use it with operators where the second argument's type depends on the first value. - Cactus

1 Answers

6
votes

The development version of Agda (2.4.3) has sections:

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