依赖对的 Church 编码

Question

可以像这样轻松地对 Church-encode 对进行编码：

Definition prod (X Y:Set) : Set := forall (Z : Set), (X -> Y -> Z) -> Z.

Definition pair (X Y:Set)(x:X)(y:Y) : prod X Y := fun Z xy => xy x y.

Definition pair_rec (X Y Z:Set)(p:X->Y->Z) (xy : prod X Y) : Z := xy Z p.

Definition fst (X Y:Set)(xy:prod X Y) : X := pair_rec X Y X (fun x y => x) xy.

Definition snd (X Y:Set)(xy:prod X Y) : Y := pair_rec X Y Y (fun x y => y) xy.

然后很容易将其推广到像这样的依赖对：

Definition dprod (X:Set)(Y:X->Set) : Set :=
forall (Z : Set), (forall (x:X),Y x->Z)->Z.

Definition dpair (X:Set)(Y:X->Set)(x:X)(y:Y x) : dprod X Y :=
fun Z xy => xy x y.

Definition dpair_rec (X:Set)(Y:X->Set)(Z:Set)(p:forall (x:X),Y x->Z)
(xy : dprod X Y) : Z := xy Z p.

Definition dfst (X:Set)(Y:X->Set)(xy:dprod X Y) : X :=
dpair_rec X Y X (fun x y => x) xy.

Definition dsnd (X:Set)(Y:X->Set)(xy:dprod X Y) : Y (dfst X Y xy) :=
dpair_rec X Y (Y (dfst X Y xy)) (fun x y => y) xy.

但是最后一个定义失败并显示错误消息：

In environment
X : Set
Y : X -> Set
xy : dprod X Y
x : X
y : Y x
The term "y" has type "Y x"
while it is expected to have type 
"Y (dfst X Y xy)".

我明白这里的问题了。但是解决办法是什么？换句话说，如何对依赖对进行Church-encode？

Answer 1

无法在 Coq 或 Agda 中对依赖对进行 Church 编码。

Ok, when we think of homogenous tuples AxA then this can also be understood as a function 2 -> A. This also works for heterogenous tuples like AxB using dependent functions Pi x:2.if x then A else B. However the next logical step is Sigma x:A.B x, which have no good representations as functions (unless we accept very dependent functions which in my mind goes against the spirit of type theory). For this reason it seems to me that the generalisation from -> to Pi and from x to Sigma is the primary one, and the fact that tuples can be represented as functions is secondary. -- Dr Thorsten Altenkirch, somewhere on the Agda mailing list

可以找到 Thorsten 提到的非常依赖的函数编码 here（请注意，这不是有效的 Agda，只是 "insanely dependent" 类型理论的类似 Agda 的语法）。

Answer 2

首先，让我们弄清楚术语。

你所说的dprod实际上是一个“依赖和”，而“依赖积”是你可能会想称之为“依赖函数”的东西。原因是依赖函数泛化了正则积，你只要巧妙地使用Bool:

prod : Set -> Set -> Set
prod A B = (b : Bool) -> case b of { True -> A; False -> B; }
{-
The type-theoretic notation would be:
prod A B = Π Bool (\b -> case b of { True -> A; False -> B; })
-}

mkPair : (A B : Set) -> A -> B -> prod A B
mkPair A B x y = \b -> case b of { True -> x; False -> y; }

elimProd : (A B Z : Set) -> (A -> B -> Z) -> prod A B -> Z
elimProd A B Z f p = f (p True) (p False)

本着同样的精神，依赖对（通常表示为Σ）概括了正则和：

sum : Set -> Set -> Set
sum A B = Σ Bool (\b -> case b of { True -> A; False -> B; })

mkLeft : (A B : Set) -> A -> sum A B
mkLeft A B x = (True, x)

mkRight : (A B : Set) -> B -> sum A B
mkRight A B y = (False, y)

elimSum : (A B Z : Set) -> (A -> Z) -> (B -> Z) -> sum A B -> Z
elimSum A B Z f _ (True, x) = f x
elimSum A B Z _ g (False, y) = g y

这可能会造成混淆，但另一方面，Π A (\_ -> B) 是正则函数的类型，而 Σ A (\_ -> B) 是正则对的类型（例如，参见 here).

所以，再一次：

依赖产品 = 依赖函数的类型
依赖总和 = 依赖对的类型

您的问题可以用以下方式重新表述：

Does there exist a Church-encoding for dependent sums via dependent products?

之前在 Math.StackExchange 上已经有人问过这个问题，这里 an answer 给出的编码与您的基本相同。

但是，看了这个答案的评论，你会发现它显然缺乏预期的归纳原理。还有一个类似的问题，但关于自然数的 Church-encoding 和 this answer (in particular the comments) sort of explains why Coq or Agda is not enough to derive the induction principle, you need additional assumptions, such as parametricity. There is yet another similar question on MathOverflow，虽然对于 Agda/Coq 的特定情况，答案没有给出明确的“是”或“否”，但它们暗示这很可能是不可能的。

最后，我不得不提的是，与当今许多其他类型论问题一样，显然 HoTT is the answer。引用 Mike Shulman 博客 post 的开头：

In this post I will argue that, improving on previous work of Awodey-Frey-Speight, (higher) inductive types can be defined using impredicative encodings with their full dependent induction principles — in particular, eliminating into all type families without any truncation hypotheses — in ordinary (impredicative) Book HoTT without any further bells or whistles.

（虽然你将得到的（命令式）编码很难称为教会编码。）

依赖对的 Church 编码

Church encoding of dependent pair

coq

agda

dependent-type

church-encoding