在 Haskell 上枚举总和和产品类型的通用算法？

Question

前段时间，我问过how to map back and forth from godel numbers to terms of a context-free language。虽然答案专门解决了这个问题，但我在实际编程时遇到了问题。所以，这个问题更通用：给定一个递归代数数据类型，包含终结符、总和和乘积——例如

data Term = Prod Term Term | SumL Term | SumR Term | AtomA | AtomB

将这种类型的项映射到其哥德尔数及其倒数的算法是什么？

编辑：例如：

data Foo = A | B Foo | C Foo deriving Show

to :: Foo -> Int
to A = 1
to (B x) = to x * 2
to (C x) = to x * 2 + 1

from :: Int -> Foo
from 1 = A
from n = case mod n 2 of
    0 -> B (from (div n 2))
    1 -> C (from (div n 2))

在这里，to 和 from 为 Foo 做我想做的事。我只是要求一种系统的方法来为任何数据类型派生这些函数。

Answer 1

为了避免处理特定的 Goedel 编号，让我们定义一个 class 来抽象必要的操作（我们稍后需要一些导入）：

{-# LANGUAGE TypeOperators, DefaultSignatures, FlexibleContexts, DeriveGeneric #-}
import Control.Applicative
import GHC.Generics
import Test.QuickCheck
import Test.QuickCheck.Gen

class GodelNum a where
    fromInt :: Integer -> a
    toInt :: a -> Maybe Integer
    encode :: [a] -> a
    decode :: a -> [a]

所以我们可以注入自然数并对序列进行编码。让我们进一步创建这个 class 的规范实例，它将在整个代码中使用，它没有真正的 Goedel 编码，只是构建一个术语树。

data TermNum = Value Integer | Complex [TermNum]
  deriving (Show)

instance GodelNum TermNum where
    fromInt = Value
    toInt (Value x) = Just x
    toInt _         = Nothing
    encode = Complex
    decode (Complex xs) = xs
    decode _            = []

对于真正的编码，我们将使用另一种只使用一个 Integer 的实现，例如 newtype SomeGoedelNumbering = SGN Integer。

让我们进一步创建一个 class 类型，我们可以 encode/decode:

class GNum a where
    gto :: (GodelNum g) => a -> g
    gfrom :: (GodelNum g) => g -> Maybe a

    default gto :: (Generic a, GodelNum g, GGNum (Rep a)) => a -> g
    gto = ggto . from
    default gfrom :: (Generic a, GodelNum g, GGNum (Rep a)) => g -> Maybe a
    gfrom = liftA to . ggfrom

最后四行使用 GHC Generics 和 DefaultSignatures 定义了 gto 和 gfrom 的通用实现。他们使用的 class GGNum 是一个助手 class，我们将使用它来定义原子 ADT 操作的编码——产品、总和等：

class GGNum f where
    ggto :: (GodelNum g) => f a -> g
    ggfrom :: (GodelNum g) => g -> Maybe (f a)

-- no-arg constructors
instance GGNum U1 where
    ggto U1 = encode []
    ggfrom _ = Just U1

-- products
instance (GGNum a, GGNum b) => GGNum (a :*: b) where
    ggto (a :*: b) = encode [ggto a, ggto b]
    ggfrom e | [x, y] <- decode e    = liftA2 (:*:) (ggfrom x) (ggfrom y)
            | otherwise             = Nothing

-- sums
instance (GGNum a, GGNum b) => GGNum (a :+: b) where
    ggto (L1 x) = encode [fromInt 0, ggto x]
    ggto (R1 y) = encode [fromInt 1, ggto y]
    ggfrom e | [n, x] <- decode e = case toInt n of
                                    Just 0  -> L1 <$> ggfrom x
                                    Just 1  -> R1 <$> ggfrom x
                                    _       -> Nothing

-- metadata
instance (GGNum a) => GGNum (M1 i c a) where
    ggto (M1 x) = ggto x
    ggfrom e = M1 <$> ggfrom e

-- constants and recursion of kind *
instance (GNum a) => GGNum (K1 i a) where
    ggto (K1 x) = gto x
    ggfrom e = K1 <$> gfrom e

有了这个，我们就可以定义一个像你的数据类型，只需声明它的 GNum 实例，其他一切都会自动派生。

data Term = Prod Term Term | SumL Term | SumR Term | AtomA | AtomB
  deriving (Eq, Show, Generic)

instance GNum Term where

为了确保我们所做的一切都是正确的，让我们使用 QuickCheck 来验证我们的 gfrom 是 gto 的倒数：

instance Arbitrary Term where
    arbitrary = oneof [ return AtomA
                      , return AtomB
                      , SumL <$> arbitrary
                      , SumR <$> arbitrary
                      , Prod <$> arbitrary <*> arbitrary
                      ]

prop_enc_dec :: Term -> Property
prop_enc_dec x = Just x === gfrom (gto x :: TermNum)

main :: IO ()
main = quickCheck prop_enc_dec

备注:

同样的事情可以使用 Scrap Your Boilerplate 完成，也许更有效，因为它允许更高级别的访问 - 枚举构造函数和记录等。
另见论文 Efficient Bijective G¨odel Numberings for Term Algebras（我还没有读过这篇论文，但似乎相关）。

Answer 2

为了好玩，我决定尝试您发布的 link 中的方法，并且没有卡在任何地方。所以这是我的代码，没有注释（解释和上次一样）。首先，从其他答案中窃取的代码：

{-# LANGUAGE TypeSynonymInstances #-}
import Control.Applicative
import Data.Universe.Helpers

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

instance Godel Nat where to = id; from = id

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

以及特定于您的新类型的代码：

data Term = Prod Term Term | SumL Term | SumR Term | AtomA | AtomB
    deriving (Eq, Ord, Read, Show)

ts = AtomA : AtomB : interleave [uncurry Prod <$> ts +*+ ts, SumL <$> ts, SumR <$> ts]

instance Godel Term where
    to AtomA = 0
    to AtomB = 1
    to (Prod t1 t2) = 2 + 0 + 3 * to (t1, t2)
    to (SumL t)     = 2 + 1 + 3 * to t
    to (SumR t)     = 2 + 2 + 3 * to t
    from 0 = AtomA
    from 1 = AtomB
    from n = case quotRem (n-2) 3 of
        (q, 0) -> uncurry Prod (from q)
        (q, 1) -> SumL (from q)
        (q, 2) -> SumR (from q)

和上次一样的ghci测试：

*Main> take 30 (map from [0..]) == take 30 ts
True

在 Haskell 上枚举总和和产品类型的通用算法？

Generic algorithm to enumerate sum and product types on Haskell?

algorithm

haskell

functional-programming

generic-programming