Haskell类型类的约束,用于定义组

Question

我想出了一个Group的类型类定义,但是我找到了一个实际上并不是一个组的反例类型.

这是类定义和一个实例,即组ℤ2:

class Group g where
  iden :: g
  op :: g -> g -> g
  inv :: g -> g

data Z2T = Z0 | Z1

instance Group Z2T where
  iden = Z0
  Z0 `op` Z0 = Z0
  Z0 `op` Z1 = Z1
  Z1 `op` Z0 = Z1
  Z1 `op` Z1 = Z0
  inv Z0 = Z1
  inv Z1 = Z0

但是,那些类型的签名Group是必要的,但不足以使一个类型真正成为一个组,这是我的反例编译:

data NotAGroup = N0 | N1

instance Group NotAGroup where
  iden = N0
  N0 `op` N0 = N0
  N1 `op` N0 = N0
  N0 `op` N1 = N0
  N1 `op` N1 = N0
  inv N0 = N0
  inv N1 = N0

如何将类型的足够规则编码为GroupHaskell 中类型类中的组？

Answer 1

你是对的,可以编写Group违反集团法的类型类的实例,因为实际上代码中没有任何内容实际说明它们.

例如,对于Monad类,其中monadic法则不以任何方式编写或执行,这种情况也是如此.您可以编写非法Monad实例,因为您可以编写非法Group实例.

这实际上是你在Haskell中可以获得的最好的,至少不会过多地增加类型签名的复杂性.事实上,要表达类型中的组定律,您可能需要一种完全依赖类型的语言,而Haskell则不然.

在这种情况下,法律通常写在评论中,可能表示为重写规则,程序员通常具有足够的纪律来尊重它们.