该比赛已结束，您无法在比赛模式下递交该题目。您可以点击“在题库中打开”以普通模式查看和递交本题。

本题暂时只支持 lean4。

有个东西叫作柯里化。

比如在大家比较熟悉的 C++ python 中，大部分函数都是"非柯里化"（uncurried）的—— 调用时一次把全部参数给齐：

int add(int a, int b) { return a + b; }
add(1, 2); // 一次给两个参数，返回 3

def add(a, b):
    return a + b

add(1, 2)  # 一次给两个参数，返回 3

这样写没什么问题。但有时候你只想先固定一部分参数，把剩下的参数"留到以后再给" （partial application / 部分求值）。比如想做一个"加一函数"，非柯里化语言里 就得绕一下：

#include <functional>
auto add1 = std::bind(add, 1, std::placeholders::_1);
add1(2); // 3

from functools import partial
add1 = partial(add, 1)
add1(2)  # 3

而"柯里化"（currying）就是把 add 改写成"一次只吃一个参数、返回一个新函数" 的形式：

auto add_c = [](int a) { return [a](int b) { return a + b; }; };
add_c(1)(2); // 3

def add_c(a):
    return lambda b: a + b

add_c(1)(2)  # 3

柯里化之后，"部分求值"就是免费的：add_c(1) 本身就是一个合法的"加一函数"， 不需要 bind / partial 之类的额外包装。

在很多编程语言中，柯里化和反柯里化是可以对任何二元函数进行的（也就是高阶函数），比如在 haskell 和 lean 中：

curry :: ((a, b) -> c) -> a -> b -> c
curry f x y = f (x, y)

uncurry :: (a -> b -> c) -> (a, b) -> c
uncurry f (x, y) = f x y

def curry {α β γ : Type} (f : α × β → γ) (x : α) (y : β) : γ := f (x, y)

def uncurry {α β γ : Type} (f : α → β → γ) (p : α × β) : γ := f p.1 p.2

看，curry 把一个"吃二元组的函数"变成"吃一个参数、再吃一个参数"的柯里化 函数，uncurry 则是反方向。

那么问题来了，以上代码是针对二元函数的，三元函数呢？

把二元组换成三元组、把套一层换成套两层，手写一个 curry3 并不难：

curry3 :: ((a, b, c) -> d) -> a -> b -> c -> d
curry3 f x y z = f (x, y, z)

uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 f (x, y, z) = f x y z

def curry3 {α β γ δ : Type} (f : α × β × γ → δ) (x : α) (y : β) (z : γ) : δ := f (x, y, z)

def uncurry3 {α β γ δ : Type} (f : α → β → γ → δ) (p : α × β × γ) : δ := f p.1 p.2.1 p.2.2

四元函数呢？再套一层。五元？再套一层……

N元函数呢？

我们发现好像在类型层面并不容易写出这个东西的 “类型”

• 疑问一：N 元的 curry 函数是由很多个箭头拼出来的，如何“定位”到最后一个箭头？
• 疑问二：对于 uncurried 的函数，这个“参数列表”是什么？ 是 N 元的 tuple 吗？还是别的？

因为疑问二的存在，不要求使用唯一的“数据结构”来装这个“参数列表”，我们会使用一些更灵活的方式测试。

这时候有人要说了，我可以使用 templeteHaskell !

没错，这个 curryN 常常被用作 templeteHaskell 的某种例题。

但是呢，我们希望你使用纯类型的方法，来“寻觅” curryN 的定义。

那么怎么评测呢？

来讲一个小小的故事。

从前有一天，出题人在写 haskell，他的程序出现了（类似）这样的几个函数：

如果你不会 haskell 只会lean 可以让 ai 把下面这段的代码翻译成 lean4.

concat3 a b c = a ++ b ++ c 
add4 a b c d = a + b + c + d
append arr a = arr ++ [a]

他当时想要这么一个函数， f，满足一下条件：

-- show 是把任何一个可表示的类型转化成一个 string 的函数\

f concat3 == \a b c -> "<" ++ (show (a ++ b ++ c)) ++">"
f add4 == \a b c d -> "<" ++ (show (a + b + c + d)) ++">"
f append == \arr a -> "<" ++ (show (arr ++ [a])) ++">"

(==) 这里指 equivalent （数学上等价）

他想，如果把这个函数实现出来该多好！

可惜，他不会构造出这个函数。

但是现在我们有 curryN 和 uncurryN 了！

不妨

ttt :: Show a => a -> String
ttt s = "<" ++ show s ++ ">"

那

curry $ ttt . uncurry concat3 就是 f concat3 啊！

curry $ ttt . uncurry add4 就是 f add4 啊！

curry $ ttt . uncurry append 就是 f append 啊！

你看这不就接近构造出 f 了吗？

基于这个故事，出题人打算这么测试：

你要在 lean4 里面实现 curry 和 uncurry 两个函数（名字固定为 curry / uncurry， 禁止用元编程），然后让形如下面的程序得到正确的结果：

def concat3 (a : String) (b : String) (c : String) := a ++ b ++ c

def add4 (a : Int) (b : Int) (c : Int) (d : Int) := a + b + c + d

def append (arr : List Int) (a : Int) := arr ++ [a]

def ttt [ToString α] (s : α) := "<" ++ ToString.toString s ++ ">"

def mycomp'a := curry $ ttt ∘ uncurry concat3
def mycomp'b := curry $ ttt ∘ uncurry add4
def mycomp'c := curry $ ttt ∘ uncurry append

#eval mycomp'a "Hello, " "World" "!"
#eval mycomp'b 1 2 3 4
#eval mycomp'c [1, 2, 3] 4

也就是说，因为 curryN 和 uncurryN 的非柯里函数的参数表的类型是你们自己定义的，

我打算只测一条行为规范：

∀ f, trans: curry (trans ∘ uncurry f) x₁ … xₙ = trans (f x₁ … xₙ)

我们需要你支持依赖值类型，但不要求支持隐式参数和类型类参数的推导，因为 curryN 可能会阻断 lean4 的某些类型推倒。

出题人会可能在一两天之后添加无须支持依赖值类型的 curryN 部分分

评测

• 你只需要提交 CurryN.lean。
• 公开测试：随题目给出（PublicTests.lean），包含上面这类调用以及依赖 类型的例子（如 (n : Nat) → Fin n → Nat）。你需要把它和 你的 CurryN.lean 拼接后编译。
• 隐藏测试：评测时组织者会加入 Grader.lean,包含一些隐藏测试。
• 限制：禁止元编程（elab / macro / syntax）、unsafe、axiom、 sorry、partial、import；只能使用 Init 自带内容。

PublicTests.lean如下：

section test'sample

def concatMix4 (a:Nat) (b:String) (c:String) (d:Nat) :=
  toString a ++ b ++ c ++ toString d


def ttt s := "<" ++ s ++ ">"

def mycomp4 := curry $ ttt ∘ uncurry concatMix4

#eval mycomp4 1 "a" "b" 2

def concatMix5 (a:Nat) (b:String) (c:String) (d:Nat) (e : Bool):=
  if e then
    toString a ++ b ++ c ++ toString d
  else
    toString d ++ c ++ b ++ toString a

def mycomp5 := curry $ ttt ∘ uncurry concatMix5
#eval mycomp5 1 "a" "b" 2 true
#eval mycomp5 1 "a" "b" 4 false

-- 类型类多态变换 + Int / List 参数
def concat3 (a : String) (b : String) (c : String) := a ++ b ++ c

def add4 (a : Int) (b : Int) (c : Int) (d : Int) := a + b + c + d

def append (arr : List Int) (a : Int) := arr ++ [a]

def ttt2 [ToString α] (s : α) := "<" ++ ToString.toString s ++ ">"

def mycomp'a := curry $ ttt2 ∘ uncurry concat3
def mycomp'b := curry $ ttt2 ∘ uncurry add4
def mycomp'c := curry $ ttt2 ∘ uncurry append

#eval mycomp'a "Hello, " "World" "!"
#eval mycomp'b 1 2 3 4
#eval mycomp'c [1, 2, 3] 4

end test'sample

clarifications

1. 本题评测即编译，通过编译即代表评测成功，编译时会把你提交的代码和评测的代码拼在一起编译