Haskell/GHC:如何在类型级自然变量上编写谓词
我发誓我最近看过一篇关于这个的文章，但是我找不到了。
我正在尝试创建一个类型来对数字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这让我认为，如果它认为它们是冲突的，我就会写错我的谓词。
我怎样才能把它们做好呢？
回答 1
Stack Overflow用户
发布于 2012-02-28 09:11:03
冲突问题很简单。rules for overlapping type families非常简单：
仅当重叠实例的右侧与重叠类型重合时，单个程序中使用的类型族的实例声明才能重叠。更正式地说，如果存在使两个实例的左侧在语法上相同的替换，则两个实例声明重叠。无论何时，在相同的替换下，实例的右侧也必须在语法上相等。
请注意，它指定了语法相等。考虑以下两个实例：
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 :: * 我们需要一个谓词来测试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现在我将使用后者，但如果您希望在其他地方使用更复杂的条件，那么通用方法开始变得更有意义。
不管怎么说。我们可以平分...er，将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类型间接处理--您可能需要添加适当的类定义，因为这些定义是根据类型选择术语所必需的，而不仅仅是根据类型选择类型。
https://stackoverflow.com/questions/9474226
复制相似问题
腾讯云开发者
