在Haskell中对幺半群相干建模

html5 • • 问答

通常，每当在 Haskell（或任何其他语言）中使用幺半群运算符时，我发现自己在问“如果语言本身支持幺半群运算的规范化会不会很方便？允许我们在某些东西上工作像一个严格的幺半群？”

最近，我有一个想法，可以通过使用类型系列在 Haskell 中实现与此类似的东西（尽管并不完全相同，因为 ex((), a)并且a仍然是不同的类型。要了解我的意思，请考虑以下类型：

-- From Control.Arrow
(***) :: a b c -> a b' c' -> a (b, b') (c, c')

x :: MyArrow () Int
y :: MyArrow String Int

目前，这个API，结合x和y与***收益率：

x *** y :: MyArrow ((),String) (Int,Int)

但是从“幺半群”的角度来看，我真正想看到的类型是同构的：

x *** y :: MyArrow String (Int,Int)

然而，要使用标准箭头组合器实际实现这一点，需要编写：

(x -> ((), x)) ^>> (x *** y) :: MyArrow String (Int,Int)

现在，为了绕过这个样板（假设我们不想处理这种将幺半群类型简化为正常形式的簿记），我的想法是使用类型族：

type family Reduce (pi :: * -> * -> *) (u :: *) (x :: *) :: * where
  Reduce pi u (pi u x) = Reduce pi u x
  Reduce pi u (pi x u) = Reduce pi u x
  Reduce pi u (pi (pi x y) z) = Reduce pi u (pi 
    (Reduce pi u x) 
    (pi 
       (Reduce pi u y) 
       (Reduce pi u z)
    )
   )
  Reduce pi u x = x

type family Reduce (pi :: * -> * -> *) (u :: *) (x :: *) :: * where
  Reduce pi u (pi u x) = Reduce pi u x
  Reduce pi u (pi x u) = Reduce pi u x
  Reduce pi u (pi (pi x y) z) = Reduce pi u (pi 
    (Reduce pi u x) 
    (pi 
       (Reduce pi u y) 
       (Reduce pi u z)
    )
   )
  Reduce pi u x = x

在 ghci repl 上尝试一下，这似乎给了我正确的“标准化”幺半群类型：

伟大的！因此，我们的想法是重写任何引入幺半群运算的组合器，以便它应用Reduce类型系列：

-- My version
(***) :: a b c -> a b' c' -> a (Reduce (,) () (b, b')) (Reduce (,) () (c, c'))

x :: MyArrow () Int
y :: MyArrow String Int
x *** y :: MyArrow String (Int, Int)

-- My version
(***) :: a b c -> a b' c' -> a (Reduce (,) () (b, b')) (Reduce (,) () (c, c'))

x :: MyArrow () Int
y :: MyArrow String Int
x *** y :: MyArrow String (Int, Int)

现在的问题是，我如何编写我的版本(***)？我需要对类型进行“模式匹配”之类的操作。那不好。因此，接下来我尝试使用具有关联类型的类型类。

> let x :: Reduce (,) () (((), Int), String) = undefined
> :t x
x :: (Int, [Char])

好的，现在我们有一个关联的Reduce类型来将幺半群归一化应用于我们的类型，但还有一些操作来实际将函数写入减少的重新表示。接下来，我编写了一个实用程序Monoidal类型类，提供幺半群相干同构以促进实现Reducible类型类：

现在问题来了。我定义了与减少幺半群单位的情况相对应的前两个实例......

instance (Monoidal pi u, Reducible pi u x) => Reducible pi u (pi u x) where
  type Reduce (pi u x) = x
  reduce x = lambdaR x
  unReduce x = lambdaRi x

instance (Monoidal pi u, Reducible pi u x) => Reducible pi u (pi x u) where
  type Reduce (pi x u) = x
  reduce x = lambdaL x
  unReduce x = lambdaLi x

...GHC 告诉我：

main.hs:18:8: error:
    Conflicting family instance declarations:
      Reduce (pi u x) = x -- Defined at main.hs:18:8
      Reduce (pi x u) = x -- Defined at main.hs:23:8
   |
18 |   type Reduce (pi u x) = x
   |

现在，这里的问题似乎是开放式和封闭式系列之间的区别。据我了解，关联类型就像开放类型系列，我之前写的是封闭类型系列，而开放类型系列有重叠限制（很像类型类）。

我发现了一个未解决的GHC 问题，我认为该问题可能与此处相关，但除此之外（因为尚不清楚是否/何时实施）——是否有任何解决此问题的方法可以让我定义我的Reduce类型类reduce和unReduce函数发布的 GHC 版本？

以上是在Haskell中对幺半群相干建模的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>