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

是否有在两个数据类型之间创建双射的策略？例如，考虑这些数据类型：

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？（还有，这个属性叫什么？）

最佳答案

步骤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

然后你可以使用我在my previous answer中描述的技巧来回答你的一个问题，用自然语言构建一个双射回顾序言：

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

差不多就是这样。现在你已经得到了你的自然双射，你可以在自然双射和比特流之间选择你最喜欢的双射进行后合成。

关于algorithm - 如何在两种数据类型之间创建完美的双射？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/36228729/