2つのデータ型間で完全なバイジェクションを作成するにはどうすればよいですか？

Question

2つのデータ型の間に双射を作成する方法はありますか？例えば、これらのデータ型を考えてみます。

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 

その後、あなたは一つに私が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 

これはかなりです。今では、自然界との共生を得ています。ポストコンポジションのために、自然界とビットストリームの間の好きな双生児を選ぶことができます。