haskell - 如何看待法律缺失

Question

我是一名数学家，经常使用范畴论，并且我已经使用 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 中缺少依赖类型，但我不确定具体情况如何(现在已经阅读了一些关于依赖类型的内容)。似乎公约只是在评论中包含这样的法律，并希望您不要不小心编造一些不满足它们的实例。

我应该如何改变我对 Haskell 的处理方式来处理这个问题？是否有一个很好的数学/类型理论解决方案(例如，需要存在一个同构的关联器(尽管问题是，我们如何在没有定律的情况下对同构进行编码？))；是否有一些“黑客”(使用诸如 DataKinds 之类的扩展名)；我是不是应该大刀阔斧地改用 Idris 之类的东西？或者是改变我对使用 Haskell 的看法的最佳回应(即接受这些法律不能以 Haskelly 的方式实现)？

(奖金)缺乏法律究竟是如何来自不支持依赖类型？

Answer 1

你想要求:

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

但是要要求这样做，您需要一种方法来检查它。因此，您或您的编译器(或证明助手)需要为此构建一个证明。问题是，什么类型是(1)的证明？

人们可以想象一些Proof输入但也许你可以构建一个证明 0 = 0而不是 (1) 的证明，两者都有类型 Proof .所以你需要一个更通用的类型。我无法决定如何分解问题的其余部分，因此我将对 Curry-Howard 同构进行 super 简要的解释，然后解释如何证明两件事相等以及依赖类型如何相关。

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))

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

关于依赖类型理论的最后说明以及它们如何对应于 curry 霍华德同构。

依赖类型可以被认为是这个问题的答案:什么类型对应于命题 $\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 .

人们可以将这些视为从 Set 到一般类别的任意索引(共)产品的概括，在其中可以明智地编写例如$\prod_\Lambda X(\lambda),$ 有时在类型理论中使用这种符号。