问

Haskell无法统一类型实例方程

纤沙湖之歌发布于 2023-02-13 10:31

function

我试图用(偶数/奇数)奇偶性类型标记规范的Nat数据类型,看看我们是否可以获得任何自由定理.这是代码:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}

-- Use DataKind promotion with type function for even-odd

module EvenOdd where

  data Parity = Even | Odd
  -- Parity is promoted to kind level Parity.
  -- Even & Odd to type level 'Even & 'Odd of kind Parity

  -- We define type-function opp to establish the relation that
  -- type 'Even is opposite of 'Odd, and vice-versa
  type family Opp (n :: Parity) :: Parity
  type instance Opp 'Even = 'Odd
  type instance Opp 'Odd = 'Even

 -- We tag natural number with the type of its parity
  data Nat :: Parity -> * where
     Zero :: Nat 'Even
     Succ :: Nat p -> Nat (Opp p)

  -- Now we (should) get free theorems.
  -- 1. Plus of two even numbers is even
  evenPlus :: Nat 'Even -> Nat 'Even -> Nat 'Even
  evenPlus Zero n2 = n2  -- Line 31
  evenPlus (Succ (Succ n1)) n2 = Succ (Succ (evenPlus n1 n2))

但是,GHC抛出类型错误:

Could not deduce (p1 ~ 'Even)
from the context ('Even ~ Opp p)
  bound by a pattern with constructor
             Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
           in an equation for `evenPlus'
  at even-odd.hs:31:13-26
or from (p ~ Opp p1)
  bound by a pattern with constructor
             Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
           in an equation for `evenPlus'
  at even-odd.hs:31:19-25
  `p1' is a rigid type variable bound by
       a pattern with constructor
         Succ :: forall (p :: Parity). Nat p -> Nat (Opp p),
       in an equation for `evenPlus'
       at even-odd.hs:31:19
Expected type: Nat 'Even
  Actual type: Nat p
In the first argument of `evenPlus', namely `n1'
In the first argument of `Succ', namely `(evenPlus n1 n2)'

据我了解,上述错误的要点是GHC无法推断(p1~'No),当上下文具有等式:((Opp(Opp p1))〜'偶数).

为什么会这样？我的方法有问题吗？

1 个回答

我不认为GADT模式匹配细化是这样的.你有一个构造函数Opp p的结果类型.所以,如果你写的东西像
```
f :: Nat 'Even -> ...
f (Succ n) = ...
```
然后类型检查器知道,Nat (Opp t) ~ Nat 'Even因此Opp t ~ 'Even.但要解决这个问题,类型检查器必须反转函数Opp,这需要很多.

我建议你改变定义Nat来说:
```
data Nat :: Parity -> * where
  Zero :: Nat 'Even
  Succ :: Nat (Opp p) -> Nat p
```
这应该工作.

编辑

实际上,让我稍微扩展一下.

上面的建议并非没有(次要)价格.你失去了一些类型推断.例如,Succ Zero现在Succ Zero :: Opp p ~ 'Even => Nat p和不是Nat 'Odd.使用显式类型注释,它可以解决问题.

您可以通过添加约束来改进这一点,Succ这需要Opp自相反.唯一的两个元素Parity是Even和Odd,并且对于这些约束成立,所以它不应该导致任何问题:
```
data Nat :: Parity -> * where
  Zero :: Nat 'Even
  Succ :: (Opp (Opp p) ~ p) => Nat (Opp p) -> Nat p
```
现Succ Zero推断为类型Nat 'Odd,模式匹配仍然有效.
2023-02-13 10:38 回答

笑点已阵亡

撰写答案

今天，你开发时遇到什么问题呢？

立即提问

热门标签

Haskell无法统一类型​​实例方程

编辑

Haskell无法统一类型实例方程