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

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=abx。x=abx的预期含义是类型x具有根本不涉及递归的a居民，以及可以与递归调用配对的b值。（我们可以定义x*x=x，而不会丢失任何感兴趣的内容。）然后像x=n0x这样的方程对应于枚举，x=0x对应于平凡的1元素递归类型，x=abx是无限的
• 我使用了懒惰的自然法则，而不是高效的法则
• 我跟踪了一组可能的基数，随着新信息的学习，一个接一个地排除它们
• 我尝试使用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

正如李耀霞所说，最后一个没有意义，因为nevernever没有NF non-⊥ 价值观不确定是否有一个好的方法来考虑这一点。