9

我可以发誓我最近看到了一篇关于此的文章，但我找不到它。

我正在尝试创建一种类型来对数字 mod 进行二进制编码n，但要这样做，我需要能够在类型级别自然上编写谓词：

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
module Modulo where

-- (pseudo-)binary representation of 
-- numbers mod n
--
--  e.g. Mod Seven contains
--    Zero . Zero . Zero $ Stop
--    Zero . Zero . One  $ Stop
--    Zero . One . Zero $ Stop
--    Zero . One . One  $ Stop
--    One . Zero . Zero $ Stop
--    One . Zero . One  $ Stop
--    One . One $ Stop 
data Mod n where
  Stop :: Mod One
  Zero :: Split n => Mod (Lo n) -> Mod n
  One  :: Split n => Mod (Hi n) -> Mod n

-- type-level naturals
data One
data Succ n 
type Two = Succ One

-- predicate to allow us to compare 
-- natural numbers
class Compare n n' b | n n' -> b

-- type-level ordering
data LT
data EQ
data GT

-- base cases
instance Compare One One EQ
instance Compare One (Succ n) LT
instance Compare (Succ n) One GT

-- recurse
instance Compare n n' b => Compare (Succ n) (Succ n') b

-- predicate to allow us to break down
-- natural numbers by their bit structure
--
-- if every number mod n can be represented in m bits, then
class Split n where
  type Lo n -- number of values mod n where the m'th bit is 0
  type Hi n -- number of values mod n where the m'th bit is 1

-- base case, n = 2
-- for this, we only need m=1 bit
instance Split Two where
  type Lo Two = One -- 0 mod 2
  type Hi Two = One -- 1 mod 2

-- recurse
--  if (Lo n) == (Hi n), then n = 2^m, so
--  the values mod (n+1) will require one extra bit
instance (Split n, Compare (Lo n) (Hi n) EQ) => Split (Succ n) where
  type Lo (Succ n) = n    -- all the numbers mod n will be prefixed by a 0
  type Hi (Succ n) = One  -- and one extra, which will be 10...0

-- recurse
--  if (Lo n) > (Hi n), then n < 2^m, so
--  the values mod (n+1) still only require m bits
instance (Split n, Compare (Lo n) (Hi n) GT) => Split (Succ n) where
  type Lo (Succ n) = Lo (n)       -- we've got the same number of lower values
  type Hi (Succ n) = Succ (Hi n)  -- and one more higher value

我当前的实现吐出了一堆编译器错误：

Nat.hs:60:8:
    Conflicting family instance declarations:
      type Lo Two -- Defined at Nat.hs:60:8-9
      type Lo (Succ n) -- Defined at Nat.hs:74:8-9

Nat.hs:61:8:
    Conflicting family instance declarations:
      type Hi Two -- Defined at Nat.hs:61:8-9
      type Hi (Succ n) -- Defined at Nat.hs:75:8-9

Nat.hs:66:10:
    Duplicate instance declarations:
      instance (Split n, Compare (Lo n) (Hi n) EQ) => Split (Succ n)
        -- Defined at Nat.hs:66:10-62
      instance (Split n, Compare (Lo n) (Hi n) GT) => Split (Succ n)
        -- Defined at Nat.hs:73:10-62

Nat.hs:67:8:
    Conflicting family instance declarations:
      type Lo (Succ n) -- Defined at Nat.hs:67:8-9
      type Lo (Succ n) -- Defined at Nat.hs:74:8-9

Nat.hs:68:8:
    Conflicting family instance declarations:
      type Hi (Succ n) -- Defined at Nat.hs:68:8-9
      type Hi (Succ n) -- Defined at Nat.hs:75:8-9

这让我觉得我要写错了我的谓词，如果它认为它们是冲突的。

我怎样才能把它们做对？

4

1 回答 1

14

冲突问题很简单。重叠类型族的规则非常简单：

仅当重叠实例的右侧与重叠类型重合时，在单个程序中使用的类型族的实例声明才可能重叠。更正式地说，如果有一个替换使实例的左侧在语法上相同，则两个实例声明重叠。在这种情况下，实例的右侧在相同的替换下也必须在语法上相等。

请注意，它在语法上指定相等。考虑这两个例子：

instance Split Two where
  type Lo Two = One -- 0 mod 2
  type Hi Two = One -- 1 mod 2

instance Split (Succ n) where
  type Lo (Succ n) = Lo (n)  
  type Hi (Succ n) = Succ (Hi n)

Two被定义为Succ One，并且为了句法相等而扩展了普通类型的同义词，因此它们在左侧是相等的；但右侧不是，因此错误。

您可能已经注意到我从上面的代码中删除了类上下文。更深层次的问题，也许是您没想到会发生上述冲突的原因，是重复的实例确实是相互冲突的重复。与往常一样，出于实例选择的目的，类上下文会被忽略，如果我没记错的话，这对于关联类型族来说是双倍的，这对于非关联类型族来说在很大程度上是一种语法便利，并且可能不会以你想要的方式受到类的约束预计。

现在，显然这两个实例应该是不同的，并且您想根据 using 的结果在它们之间进行选择Compare，因此该结果必须是类型类的参数，而不仅仅是约束。您还在这里将类型族与功能依赖项混合在一起，这是不必要的尴尬。因此，从顶部开始，我们将保留基本类型：

-- type-level naturals
data One
data Succ n 
type Two = Succ One

-- type-level ordering
data LT
data EQ
data GT

将函数重写Compare为类型族：

type family Compare n m :: *
type instance Compare One One = EQ
type instance Compare (Succ n) One = GT
type instance Compare One (Succ n) = LT
type instance Compare (Succ n) (Succ m) = Compare n m

现在，为了处理条件，我们需要某种“流控制”类型族。我将在这里定义一些更笼统的东西来启发和启发；根据口味专门。

我们将给它一个谓词、一个输入和两个可供选择的分支：

type family Check pred a yes no :: *

我们需要一个用于测试Compare结果的谓词：

data CompareAs a
type instance (CompareAs LT) LT yes no = yes 
type instance (CompareAs EQ) LT yes no = no
type instance (CompareAs GT) LT yes no = no
type instance (CompareAs LT) EQ yes no = no 
type instance (CompareAs EQ) EQ yes no = yes
type instance (CompareAs GT) EQ yes no = no
type instance (CompareAs LT) GT yes no = no
type instance (CompareAs EQ) GT yes no = no
type instance (CompareAs GT) GT yes no = yes

这是一组非常乏味的定义，当然，对于比较更大的类型值集来说，预测是相当严峻的。存在更多可扩展的方法（伪类标签和双射，自然是一个明显和有效的解决方案），但这有点超出了这个答案的范围。我的意思是，我们只是在这里进行类型级计算，我们不要变得荒谬或任何事情。

在这种情况下，更简单的方法是简单地在比较结果上定义一个案例分析函数：

type family CaseCompare cmp lt eq gt :: *
type instance CaseCompare LT lt eq gt = lt
type instance CaseCompare EQ lt eq gt = eq
type instance CaseCompare GT lt eq gt = gt

我现在将使用后者，但是如果您在其他地方想要更复杂的条件，那么通用方法开始变得更有意义。

反正。我们可以将......呃，Split类拆分成不相关的类型族：

data Oops

type family Lo n :: *
type instance Lo Two = One
type instance Lo (Succ (Succ n)) 
    = CaseCompare (Compare (Lo (Succ n)) (Hi (Succ n)))
                  Oops -- yay, type level inexhaustive patterns
                  (Succ n)
                  (Lo (Succ n))

type family Hi n :: *
type instance Hi Two = One
type instance Hi (Succ (Succ n)) 
    = CaseCompare (Compare (Lo (Succ n)) (Hi (Succ n)))
                  Oops -- yay, type level inexhaustive patterns
                  One
                  (Succ (Hi (Succ n)))

这里最重要的一点是（看似多余的）使用(Succ (Succ n))-- 原因是需要两个Succ构造函数来区分参数和Two，从而避免您看到的冲突错误。

请注意，为简单起见，我已将所有内容移至此处的类型族，因为它完全是类型级别的。如果您还希望根据上述计算以不同方式处理值 - 包括间接地，通过Mod类型 - 您可能需要添加适当的类定义，因为这些是根据类型选择术语所必需的，而不仅仅是基于类型选择关于类型。

于 2012-02-28T01:11:03.487 回答