我记得最近看到一篇关于这个的文章，但是我找不到它了。
我正在尝试制作一个类型来对数字模 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
这让我想到，如果它认为谓词冲突了，那么我写谓词的方式可能有误。如何正确地编写谓词呢？