如何理解"引理"功能的一般类型？

Question

也许这是一个愚蠢的问题.下面是一个报价的Hasochism纸:

解决此问题的一种方法是将由参数化方程给出的引理编码为Haskell函数.通常,这种引理可以编码为类型的函数:

? x1 ... xn. Natty x1 ? ... ? Natty xn ? ((l ~ r) ? t) ? t

我以为我理解了RankNTypes,但我无法理解这个命题的最后部分.我正在非正式地阅读它"给出一个需要的术语l ~ r,返回那个术语".我确信这种解释是错误的,因为它似乎导致了循环:我们l ~ r直到证明本身的结论才知道,那么我怎么能期望作为证据的假设提供一个需要的术语呢？

我本来期望一个等式证明有一个更像这样的类型:

Natty x1 ? ... ? Natty xn ? l :~: r

非正式地,"给定一堆Nattys,返回命题证明l并且r相等"(使用GHC的Data.Type.Equality).这对我来说更有意义,并且似乎与你在其他依赖类型系统中所说的一致.我猜它相当于论文中的版本,但我正在努力精神上消除这两个版本.

总之,我很困惑.我觉得我错过了一个关键的洞察力.我该怎么读这个类型((l ~ r) => t) -> t？

Answer 1

我正在读它"给出一个需要的术语l ~ r,返回那个术语"

它是"给定一个类型包含的术语l,返回该术语,所有ls被类型中的s替换r"(或在另一个方向r -> l).这是一个非常巧妙的方法,它允许你所有的委托cong,trans,subst和类似的东西GHC.

这是一个例子:

{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeFamilies, TypeOperators, RankNTypes #-}

data Nat = Z | S Nat

data Natty n where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

data Vec a n where
    Nil  :: Vec a Z
    Cons :: a -> Vec a n -> Vec a (S n)

type family (n :: Nat) :+ (m :: Nat) :: Nat where
    Z     :+ m = m
    (S n) :+ m = S (n :+ m)

assoc :: Natty n -> Natty m -> Natty p -> (((n :+ m) :+ p) ~ (n :+ (m :+ p)) => t) -> t
assoc  Zy     my py t = t
assoc (Sy ny) my py t = assoc ny my py t

coerce :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p))
coerce ny my py xs = assoc ny my py xs

UPDATE

专业化是有益的assoc:

assoc' :: Natty n -> Natty m -> Natty p ->
            (((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p)))
                                               -> Vec a (n :+ (m :+ p))
assoc'  Zy     my py t = t
assoc' (Sy ny) my py t = assoc ny my py t

coerce' :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p))
coerce' ny my py xs = assoc' ny my py xs

Daniel Wagner在评论中解释了正在发生的事情:

或者,换句话说,你可以阅读((l~r)=> t) - > t as,"给定一个类型很好的术语,假设l~r,从我们拥有的上下文中返回相同的术语证明了l~r并解除了这个假设".

让我们详细说明证明部分.

在assoc' Zy my py t = t情况下,n等于Zy,因此我们有

((Zy :+ m) :+ p) ~ (Zy :+ (m :+ p))

减少到

(m :+ p) ~ (m :+ p)

这显然是身份,因此我们可以解除这个假设并返回t.

在每个递归步骤,我们保持

((n :+ m) :+ p) ~ (n :+ (m :+ p))

方程.所以,当assoc' (Sy ny) my py t = assoc ny my py t方程变为

((Sy n :+ m) :+ p) ~ (Sy n :+ (m :+ p))

减少到

 Sy ((n :+ m) :+ p) ~ Sy (n :+ (m :+ p))

由于定义(:+).因为构造函数是单射的

constructors_are_injective :: S n ~ S m => Vec a n -> Vec a m
constructors_are_injective xs = xs

等式成为

((n :+ m) :+ p) ~ (n :+ (m :+ p))

我们可以assoc'递归调用.

最后在coerce'这两个术语的召唤中统一:

 1. ((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p))
 2.                                      Vec a ((n :+ m) :+ p)

显然Vec a ((n :+ m) :+ p)是Vec a (n :+ (m :+ p))在假设的情况下((n :+ m) :+ p) ~ (n :+ (m :+ p)).