我可以一般地计算类型的基数吗？

Question

我想要一个类型类来告诉我各种类型有多大。

data Cardinality = Finite Natural | Infinite
class Sized a where cardinality :: Cardinality

编写实例非常简单；例如：

instance Sized Void where cardinality = Finite 0
instance Sized ()   where cardinality = Finite 1
instance Sized Bool where cardinality = Finite 2

instance Sized a => Sized [a] where
    cardinality = case cardinality @a of
        Finite 0 -> Finite 1
        _ -> Infinite

data X = X Y
data Y = Y X X
instance Sized X where cardinality = Finite 1
instance Sized Y where cardinality = Finite 1

事实上，它是如此简单，感觉它应该是可自动化的。也许泛型编程会有所帮助？

class GSized f where gcardinality :: Cardinality
class Sized a where
    cardinality :: Cardinality
    default cardinality :: (Generic a, GSized (Rep a)) => Cardinality
    cardinality = gcardinality @(Rep a)

大多数实例都非常简单：

instance GSized V1 where gcardinality = Finite 0
instance GSized U1 where gcardinality = Finite 1
instance GSized f => GSized (M1 i c f) where gcardinality = gcardinality @f
instance (GSized f, GSized g) => GSized (f :+: g) where
    gcardinality = case (gcardinality @f, gcardinality @g) of
         (Finite n, Finite n') -> Finite (n+n')
         _ -> Infinite
instance (GSized f, GSized g) => GSized (f :*: g) where
    gcardinality = case (gcardinality @f, gcardinality @g) of
        (Finite 0, _) -> Finite 0
        (_, Finite 0) -> Finite 0
        (Finite n, Finite n') -> Finite (n*n')
        _ -> Infinite

但后来我卡住了。单个字段的直接操作肯定行不通：

instance Sized c => GSized (K1 i c) where
    gcardinality = cardinality @c

对于递归类型，这是一个非常简单的无限循环。我尝试了多种方法来丰富这里涉及的两个类。

• 我将cardinality 和gcardinality 概括为函数，因此我可以假设我已经知道递归事件的大小。然后在K1 实例中我可以问：如果你所有的递归实例都无人居住，你会有多大？如果所有递归实例都有一个居民怎么办？等等。
• 我从单一基数概括为像x = a + bx 这样的“递归关系”。 x = a + bx 的预期含义是 x 类型具有完全不涉及递归的 a 居民，以及可以与递归调用配对的 b 值。 （我们可以定义 x*x = x 而不会失去任何有趣的东西。）然后像 x = n + 0x 这样的方程对应于枚举，x = 0 + x 对应于平凡的 1 元素递归类型，x = a + bx 是无限的。
• 我使用了懒惰的自然而不是高效的。
• 我跟踪了一组可能的基数，并在了解新信息后将它们一一排除。
• 我尝试使用 Generic1 而不是 Generic。

这些都没有成功。似乎存在三种核心的难题/失败模式：

• K1 定义中用于递归类型的循环，或者对于递归类型可以正常工作，但对于相互递归类型会失败。
• K1 用于递归出现和普通字段，似乎没有简单的方法来区分它们。
• 为普通递归类型选择 Finite 0 而不是 Finite 1。

是否有解决这些问题的方法？上面的[Void]、[()]、X 和Y 的通用实例在哪里都已定义且正确？

Answer 1

{-# LANGUAGE DeriveGeneric, TypeFamilies, ScopedTypeVariables, UnicodeSyntax
           , TypeApplications, AllowAmbiguousTypes
           , DataKinds, PolyKinds, DefaultSignatures
           , FlexibleInstances, DeriveAnyClass #-}

import GHC.Generics
import Numeric.Natural
import Data.Void
import Data.Proxy
import GHC.TypeLits

data Cardinality = Finite Natural | Infinite
 deriving (Show)

instance Sized Void where cardinalityIC _ = Finite 0
instance Sized ()   where cardinalityIC _ = Finite 1
instance Sized Bool where cardinalityIC _ = Finite 2

instance Sized a => Sized [a] where
    cardinalityIC rctxt = case cardinalityIC @a rctxt of
        Finite 0 -> Finite 1
        _ -> Infinite

data TypeIdentifier = TypeIdentifier
  { typeName, moduleName, packageName :: String }
  deriving (Eq, Show)

class GSized f where gcardinalityIC :: [TypeIdentifier] -> Cardinality
class Sized a where
    cardinalityIC :: [TypeIdentifier] -> Cardinality
    default cardinalityIC :: (Generic a, GSized (Rep a))
              => [TypeIdentifier] -> Cardinality
    cardinalityIC = gcardinalityIC @(Rep a)

cardinality :: ∀ a . Sized a => Cardinality
cardinality = cardinalityIC @a []

instance GSized V1 where gcardinalityIC _ = Finite 0
instance GSized U1 where gcardinalityIC _ = Finite 1

instance GSized f => GSized (M1 C c f) where gcardinalityIC = gcardinalityIC @f
instance GSized f => GSized (M1 S c f) where gcardinalityIC = gcardinalityIC @f

instance (GSized f, KnownSymbol tn, KnownSymbol mn, KnownSymbol pn)
            => GSized (D1 ('MetaData tn mn pn nt) f) where
  gcardinalityIC rctxt
    | thisType`elem`rctxt  = Infinite
    | otherwise            = gcardinalityIC @f $ thisType : rctxt
   where thisType = TypeIdentifier
                     (symbolVal $ Proxy @tn)
                     (symbolVal $ Proxy @mn)
                     (symbolVal $ Proxy @pn)
         moduleName = symbolVal $ Proxy @tn

instance (GSized f, GSized g) => GSized (f :+: g) where
    gcardinalityIC rctxt = case (gcardinalityIC @f rctxt, gcardinalityIC @g rctxt) of
         (Finite n, Finite n') -> Finite (n+n')
         _ -> Infinite
instance (GSized f, GSized g) => GSized (f :*: g) where
    gcardinalityIC rctxt = case (gcardinalityIC @f rctxt, gcardinalityIC @g rctxt) of
        (Finite 0, _) -> Finite 0
        (_, Finite 0) -> Finite 0
        (Finite n, Finite n') -> Finite (n*n')
        _ -> Infinite


instance Sized c => GSized (K1 i c) where
    gcardinalityIC = cardinalityIC @c

data Foo = F0 Bool | F1 Bool
 deriving (Generic, Sized)

data Bar = B0 Bool | B1 Bar
 deriving (Generic, Sized)

data Never = Never Never
 deriving (Generic, Sized)

ghci> cardinality @Foo
Finite 4
ghci> cardinality @Bar
Infinite
ghci> cardinality @Never
Infinite

正如夏立耀所说，最后一个并没有真正的意义，因为Never 从来没有没有 NF 非⊥ 值。不确定是否有考虑到这一点的好方法。