我是一位数学家,经常使用范畴论进行工作。我使用Haskell进行某些计算等方面的工作,但我绝对不是程序员。我非常喜欢Haskell,并希望变得更加熟练,特别是在编写程序时,我发现类型系统非常有用。
然而,最近我尝试实现范畴论相关内容时遇到了问题,这是因为在Haskell中似乎无法使用类方法约束。以防我的术语使用不正确,我所指的是可以这样写:
据我所知,这是由于Haskell中缺乏依赖类型,但我不确定这到底是怎么回事(现在已经读了一些关于依赖类型的内容)。另外,惯例就是将这些定律放在注释中,并希望您不会意外地创建出不能满足这些定律的实例。
1. 我应该如何改变我的Haskell方法来解决这个问题?是否有一个漂亮的数学/类型理论解决方案(例如,要求存在一个是同构的结合器(但问题是,我们如何编码没有法则的同构));是否有一些“hack”(使用扩展,例如DataKinds);我是否应该彻底转向使用类似Idris的东西;还是最好的反应就是改变我思考使用Haskell的方式(即接受这些定律无法以Haskelly方式实现)?
2. (附加题)缺少定律具体是如何与不支持依赖类型有关的?
然而,最近我尝试实现范畴论相关内容时遇到了问题,这是因为在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. (附加题)缺少定律具体是如何与不支持依赖类型有关的?
hs-to-coq
项目实际上定义了一个“Monoid”合法的含义,并且后来证明了Set
实例:https://github.com/antalsz/hs-to-coq/blob/d875d8ffe59b62e453dc8dd8b45af1842d03bdc5/base-thy/GHC/Base.v#L309 - Joachim Breitner