Currying with dependent types in agda

Question

I assumed you could curry any function in Agda. So that you can always swap the order of the inputs.

and a theorem expressing that even compiles:

curry : {A : Set} -> {B : Set} -> {C : Set} -> ( A -> B -> C) -> (B -> A -> C)
curry f b a = f a b

However, Agda has dependent types and something like

curry' : {A : Set} -> {B : ( A -> Set ) } -> { C : ( A -> Set ) } -> ( (a : A) -> B a -> C a) -> ( B a -> (a : A) -> C a) 

doesn't even compile.

Since (a : A) -> B a -> C a is just as valid as A -> B -> C I'm starting tho think that you cannot curry in general. Though nothing seems particularly awful about handing a function B a before a : A.

Is there some trick to perform currying in general? or is it not possible in Agda?

Answer 1

What you describe is not currying. It's a simple swapping of arguments.

Here's how currying looks like:

open import Data.Product
  hiding (curry)

-- non-dependent version
curry′ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
         (A × B → C) → (A → B → C)
curry′ f a b = f (a , b)

-- dependent version
curry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Set c} →
        (Σ A B → C) → ((a : A) → B a → C)
curry f a b = f (a , b)

C could also depend on A and B; fully dependent version can be found in Data.Product.

Anyways, that's besides the point. The operation you want (that is depenent swap) cannot be implemented in Agda - and also in most other dependent type theories.

Answer 2

You can do something like this:

open import Level
open import Function hiding (id)
open import Data.Nat
open import Data.Vec

data Id {α : Level} {A : Set α} : A -> Set α where
  id : (x : A) -> Id x

flip-id : {α β γ : Level} {A : Set α} {B : A -> Set β} {C : (x : A) -> B x -> Set γ} {x : A}
       -> ((x : A) -> (y : B x) -> C x y) -> (y : B x) -> Id x -> C x y
flip-id f y (id x) = f x y

test-func : (n : ℕ) -> Vec ℕ n -> ℕ
test-func n _ = n

{-error : ℕ
error = flip test-func (0 ∷ 0 ∷ []) 2-}

ok : ℕ
ok = flip-id test-func (0 ∷ 0 ∷ []) (id 2)

There is also symmetric function:

id-flip : {α β γ : Level} {A : Set α} {B : A -> Set β} {C : (x : A) -> B x -> Set γ}
      -> ({x : A} -> (y : B x) -> Id x -> C x y) -> (x : A) -> (y : B x) -> C x y
id-flip f x y = f y (id x)

Answer 3

It could be defined if you use the same a : A in both functions, i.e.

foo : {A : Set} {B C : A → Set}(a : A) →
      (A → B a → C a) →
      (B a → A → C a)
foo a f Ba _ = f a Ba