如何思考法律缺失问题

Question

如何思考法律缺失问题

8

我是一位数学家，经常使用范畴论进行工作。我使用Haskell进行某些计算等方面的工作，但我绝对不是程序员。我非常喜欢Haskell，并希望变得更加熟练，特别是在编写程序时，我发现类型系统非常有用。

然而，最近我尝试实现范畴论相关内容时遇到了问题，这是因为在Haskell中似乎无法使用类方法约束。以防我的术语使用不正确，我所指的是可以这样写：

class Monoid c where
    id :: c -> c
    m :: c -> c -> c

但是我无法按照以下的法律条款进行编写：

m (m x y) z ==  m x $ m y z

据我所知，这是由于Haskell中缺乏依赖类型，但我不确定这到底是怎么回事（现在已经读了一些关于依赖类型的内容）。另外，惯例就是将这些定律放在注释中，并希望您不会意外地创建出不能满足这些定律的实例。

1. 我应该如何改变我的Haskell方法来解决这个问题？是否有一个漂亮的数学/类型理论解决方案（例如，要求存在一个是同构的结合器（但问题是，我们如何编码没有法则的同构））；是否有一些“hack”（使用扩展，例如DataKinds）；我是否应该彻底转向使用类似Idris的东西；还是最好的反应就是改变我思考使用Haskell的方式（即接受这些定律无法以Haskelly方式实现）？

2. （附加题）缺少定律具体是如何与不支持依赖类型有关的？

- Tim

3

表达简单的规则并不需要依赖类型。需要使用证明检查器。几乎所有实现任意证明的语言都是依赖类型的，因为当你走得那么远时，也可以通过允许依赖类型来扩展允许的证明范围。 - Carl

关于第一点，人们可能会问的另一件事是如何处理Python/Java中类型系统的缺乏或不足。 - Dan Robertson

2

一种方法是将代码翻译成像Coq这样的语言，并在那里进行验证。https://github.com/antalsz/hs-to-coq http://hackage.haskell.org/package/containers-verified 另一种方法是放弃正式证明，使用生成测试来尝试找到属性的反例。http://austinrochford.com/posts/2014-05-27-quickcheck-laws.html - danidiaz

1

扩展 @danidiaz 的评论：hs-to-coq 项目实际上定义了一个“Monoid”合法的含义，并且后来证明了 Set 实例：https://github.com/antalsz/hs-to-coq/blob/d875d8ffe59b62e453dc8dd8b45af1842d03bdc5/base-thy/GHC/Base.v#L309 - Joachim Breitner

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Dan Robertson · Accepted Answer

您想要求：

m (m x y) z = m x (m y z)        -- (1)

但是要求这个，你需要一种检查的方式。因此，你或者你的编译器（或证明助手）需要构建一个证明。问题是，证明（1）的类型是什么？

可以想象一些“Proof”类型，但是也许你只能构造一个证明“0 = 0”，而不是证明（1），两者都有类型“Proof”。因此，你需要更通用的类型。我无法决定如何分解其余的问题，所以我将简要解释Curry-Howard同构，然后解释如何证明两个相等的事物以及依赖类型的相关性。

Curry-Howard同构说命题同构于类型，证明同构于程序：类型对应于命题，证明该命题对应于构造值的程序。忽略了多少命题可能被表达为类型，例如，类型“A * B”（在Haskell中写作“(A, B)”）对应于命题“A和B”，而类型“A + B”（在Haskell中写作“Either A B”）对应于命题“A或B”。最后，类型“A->B”对应于“如果A，则B”，因为这个证明是一个程序，它接受A的证据并给出B的证据。应该注意的是，没有一种方法可以表达“not A”，但是可以想象添加一个类型“Not A”，其中内置类型为“Either a (Not a)”（排中律），以及“Not (Not a)->a”，以及“a * Not a->Void”（其中“Void”是一种不能被占用的类型，因此对应于false），但是然后无法运行这些程序以获得建设性证明。

现在我们将忽略Haskell的某些现实并想象没有绕过这些规则的方法（特别是“undefined :: a”表示一切都是真的，“unsafeCoerce :: a-> b”表示任何事物都意味着其他任何事物，或者只是其他函数不返回它们的存在不意味着相应的证明）。

所以我们知道如何组合命题，但是命题可能是什么？好吧，一个命题可以是说两种类型相等。在Haskell中，这对应于GADT。

data Eq a b where Refl :: Eq c c

这个构造函数对应于等式的自反性质。

[附注：如果你对“同伦类型理论”感兴趣，可以查找Voevodsky的单价基础知识。]

那么现在我们能证明什么吗？等式的传递性如何：

trans :: Eq a b -> Eq b c -> Eq a c
trans x y =
  case x of
  Refl -> -- by this match being successful, the compiler now knows that a = b
    case y of
    Refl -> -- and now b = c and so the compiler knows a = c
      Refl -- the compiler knows that this is of type Eq d d, and as it knows a = c, this typechecks as Eq a c

这个感觉好像并没有真正证明任何东西（尤其是因为这主要依赖于编译器知道传递性和对称性），但当你在逻辑中证明简单的事情时，也会有相似的感受。

那么现在该如何证明原命题（1）呢？假设我们想让类型 c 成为一个幺半群，那么我们还应该证明 $\forall x,y,z:c, m (m x y) z = m x (m y z).$，所以我们需要一种方式来表达类型 m (m x y) z。严格地说，这不是依赖类型（可以使用 DataKinds 来提升值和类型族代替函数来实现）。但是你确实需要依赖类型来使类型依赖于值。具体而言，如果你有自然数类型 Nat 和长度固定的向量类型族 Vec :: Nat -> *（* 是所有类型的种类（读作类型）），你可以定义一个依赖类型函数 mkVec :: (n::Nat) -> Vec n。注意到输出类型依赖输入的值。

因此，你的定律需要将函数提升到类型级别（跳过如何定义类型相等性和值相等性的问题），以及依赖类型（虚构的语法）。

class Monoid c where
  e :: c
  (*) :: c -> c -> c
  idl :: (x::c) -> Eq x (e * x)
  idr :: (x::c) -> Eq x (x * e)
  assoc :: (x::c) -> (y::c) -> (z::c) -> Eq ((x * y) * z) (x * (y * z))

观察一下在依赖类型和证明中如何使类型变得更大。在缺少类型类的语言中，可以将这些值放入记录中。

关于依赖类型理论及其与柯里-霍华德同构之间的关系的最终说明。

依赖类型可以被认为是对以下问题的回答：哪些类型对应于命题 $\forall x\in S\quad P(x)$ 和 $\exists y\in T\quad Q(y)?$。

答案是你可以创建新的方式来制作类型：依赖积和依赖和（余积）。依赖积表示“对于类型 $S$ 的所有值 $x$，都有类型为 $P(x)$ 的值。”普通积是一个具有 $S=2$ 的依赖积，它是由两个值占据的类型。依赖积可以写成 (x:T) -> P x。依赖和则表示“类型为 $T$ 的某些值 $y$，与类型为 $Q(y)$ 的值配对。”它可以写成 (y:T) * Q y。

可以将这些视为从集合到一般范畴的任意索引（余）积的概括，其中人们可能会合理地编写例如 $\prod_\Lambda X(\lambda)$ 这样的符号，并且有时在类型理论中使用此类符号。