如何在两种数据类型之间创建完美的双射？

Question

是否存在在两种数据类型之间创建双射的策略？例如,考虑以下数据类型:

data Colbit 
    = White Colbit Colbit 
    | Black Colbit Colbit 
    | Tip

data Bits
    = B0 Bits
    | B1 Bits
    | BEnd

加上有效元素Colbit必须具有奇数个节点(白/黑构造函数)的约束.我该如何创建地图:

toColbit :: Bits -> Colbit
fromColbit :: Colbit -> Bits

这样,对所有人b : Bits,fromColbit (toColbit b) == b对所有人来说c : Colbit,toColbit (fromColbit c) == c？(另外,这个属性叫什么？)

Answer 1

第1步是将奇数约束转换Colbit为类型级别:

{-# LANGUAGE TypeSynonymInstances #-}

data Color = Black | White deriving (Bounded, Enum, Eq, Ord, Read, Show)
data Odd = Evens Color Even Even | Odds Color Odd Odd deriving (Eq, Ord, Read, Show)
data Even = Tip | OddL Color Odd Even | OddR Color Even Odd deriving (Eq, Ord, Read, Show)
type Colbit = Odd

然后你可以在我之前回答你的一个问题时玩我描述的技巧来建立一个自然的双射.回顾序言:

type Nat = Integer
class Godel a where
    to :: a -> Nat
    from :: Nat -> a

instance Godel Nat where to = id; from = id

-- you should probably fix this instance to not use
-- Double if you plan to use it for anything serious
instance (Godel a, Godel b) => Godel (a, b) where
    to (m_, n_) = (m + n) * (m + n + 1) `quot` 2 + m where
        m = to m_
        n = to n_
    from p = (from m, from n) where
        isqrt    = floor . sqrt . fromIntegral
        base     = (isqrt (1 + 8 * p) - 1) `quot` 2
        triangle = base * (base + 1) `quot` 2
        m = p - triangle
        n = base - m

instance (Godel a, Godel b) => Godel (Either a b) where
    to (Left  l) = 0 + 2 * to l
    to (Right r) = 1 + 2 * to r
    from n = case n `quotRem` 2 of
        (l, 0) -> Left  (from l)
        (r, 1) -> Right (from r)

有了这些,我们类型的实例非常简单.

monomorph :: Either a a -> Either a a
monomorph = id

toColored :: Godel v => (Color, v) -> Nat
toColored (Black, v) = to (monomorph (Left  v))
toColored (White, v) = to (monomorph (Right v))

fromColored :: Godel v => Nat -> (Color, v)
fromColored n = case from n of
    Left  v -> (Black, v)
    Right v -> (White, v)

instance Godel Odd where
    to (Evens c l r) = 0 + 2 * toColored (c, (l, r))
    to (Odds  c l r) = 1 + 2 * toColored (c, (l, r))
    from n = case n `quotRem` 2 of
        (clr, 0) -> Evens c l r where (c, (l, r)) = fromColored clr
        (clr, 1) -> Odds  c l r where (c, (l, r)) = fromColored clr

instance Godel Even where
    to Tip = 0
    to (OddL c l r) = 1 + 2 * toColored (c, (l, r))
    to (OddR c l r) = 2 + 2 * toColored (c, (l, r))
    from 0 = Tip
    from n = case (n-1) `quotRem` 2 of
        (clr, 0) -> OddL c l r where (c, (l, r)) = fromColored clr
        (clr, 1) -> OddR c l r where (c, (l, r)) = fromColored clr

这就是它.现在你已经完成了对自然的双射,并且你可以在自然和比特流之间选择你喜欢的双射来进行后期合成.