haskell /GHC : How to write predicates on type-level naturals

Question

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

我正在尝试创建一种类型来对数字 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

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

我怎样才能正确地完成它们？

Answer 1

冲突问题很简单。 rules for overlapping type families非常简单:

The instance declarations of a type family used in a single program may only overlap if the right-hand sides of the overlapping instances coincide for the overlapping types. More formally, two instance declarations overlap if there is a substitution that makes the left-hand sides of the instances syntactically the same. Whenever that is the case, the right-hand sides of the instances must also be syntactically equal under the same substitution.

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

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，并且普通类型同义词出于语法平等的目的而被扩展，因此它们在左侧是相等的；但右侧不是，因此会出现错误。

您可能已经注意到我从上面的代码中删除了类上下文。更深层次的问题，也许是您没有预料到上述冲突发生的原因，是重复的实例实际上是冲突的重复项。一如既往，出于实例选择的目的，类上下文被忽略，如果我没记错的话，对于关联类型族来说，这会加倍，这在很大程度上是非关联类型族的语法便利，并且可能不会以您希望的方式受到类的限制期待。

现在，显然这两个实例应该是不同的，并且您希望根据使用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 :: * 

我们需要一个谓词来测试比较的结果:

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

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

在这种情况下更简单的是简单地定义比较结果的案例分析函数:

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 类型)，您可能需要添加适当的类定义，因为这些是根据以下条件选择术语所必需的:类型，而不是仅仅根据类型选择类型。