我可以通用地计算类型的基数吗？

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对应于平凡的一元素递归类型，并且x = a + bx是无限的。
• 我用的是懒惰的自然人而不是高效的自然人。
• 我跟踪了一组可能的基数，并在了解新信息时一一排除它们。
• 我尝试使用Generic1而不是Generic.

这些最终都没有取得很好的效果。似乎存在三种核心的难题/失败模式：

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

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

Answer 1

{-# LANGUAGE DeriveGeneric, TypeFamilies, ScopedTypeVariables, UnicodeSyntax\n           , TypeApplications, AllowAmbiguousTypes\n           , DataKinds, PolyKinds, DefaultSignatures\n           , FlexibleInstances, DeriveAnyClass #-}\n\nimport GHC.Generics\nimport Numeric.Natural\nimport Data.Void\nimport Data.Proxy\nimport GHC.TypeLits\n\ndata Cardinality = Finite Natural | Infinite\n deriving (Show)\n\ninstance Sized Void where cardinalityIC _ = Finite 0\ninstance Sized ()   where cardinalityIC _ = Finite 1\ninstance Sized Bool where cardinalityIC _ = Finite 2\n\ninstance Sized a => Sized [a] where\n    cardinalityIC rctxt = case cardinalityIC @a rctxt of\n        Finite 0 -> Finite 1\n        _ -> Infinite\n\ndata TypeIdentifier = TypeIdentifier\n  { typeName, moduleName, packageName :: String }\n  deriving (Eq, Show)\n\nclass GSized f where gcardinalityIC :: [TypeIdentifier] -> Cardinality\nclass Sized a where\n    cardinalityIC :: [TypeIdentifier] -> Cardinality\n    default cardinalityIC :: (Generic a, GSized (Rep a))\n              => [TypeIdentifier] -> Cardinality\n    cardinalityIC = gcardinalityIC @(Rep a)\n\ncardinality :: \xe2\x88\x80 a . Sized a => Cardinality\ncardinality = cardinalityIC @a []\n\ninstance GSized V1 where gcardinalityIC _ = Finite 0\ninstance GSized U1 where gcardinalityIC _ = Finite 1\n\ninstance GSized f => GSized (M1 C c f) where gcardinalityIC = gcardinalityIC @f\ninstance GSized f => GSized (M1 S c f) where gcardinalityIC = gcardinalityIC @f\n\ninstance (GSized f, KnownSymbol tn, KnownSymbol mn, KnownSymbol pn)\n            => GSized (D1 ('MetaData tn mn pn nt) f) where\n  gcardinalityIC rctxt\n    | thisType`elem`rctxt  = Infinite\n    | otherwise            = gcardinalityIC @f $ thisType : rctxt\n   where thisType = TypeIdentifier\n                     (symbolVal $ Proxy @tn)\n                     (symbolVal $ Proxy @mn)\n                     (symbolVal $ Proxy @pn)\n         moduleName = symbolVal $ Proxy @tn\n\ninstance (GSized f, GSized g) => GSized (f :+: g) where\n    gcardinalityIC rctxt = case (gcardinalityIC @f rctxt, gcardinalityIC @g rctxt) of\n         (Finite n, Finite n') -> Finite (n+n')\n         _ -> Infinite\ninstance (GSized f, GSized g) => GSized (f :*: g) where\n    gcardinalityIC rctxt = case (gcardinalityIC @f rctxt, gcardinalityIC @g rctxt) of\n        (Finite 0, _) -> Finite 0\n        (_, Finite 0) -> Finite 0\n        (Finite n, Finite n') -> Finite (n*n')\n        _ -> Infinite\n\n\ninstance Sized c => GSized (K1 i c) where\n    gcardinalityIC = cardinalityIC @c\n\ndata Foo = F0 Bool | F1 Bool\n deriving (Generic, Sized)\n\ndata Bar = B0 Bool | B1 Bar\n deriving (Generic, Sized)\n\ndata Never = Never Never\n deriving (Generic, Sized)\n

\n

ghci> cardinality @Foo\nFinite 4\nghci> cardinality @Bar\nInfinite\nghci> cardinality @Never\nInfinite\n

\n

正如夏立耀所说，最后一个实际上没有意义，因为从来Never没有 NF 非\xe2\x8a\xa5 值。不确定是否有好的方法来考虑这一点。

\n