Can I compute a type's cardinality generically?

Question

I'd like to have a type class that tells me how big various types are.

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

It's pretty straightforward to write instances; for example:

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

In fact, it's so straightforward, it feels like it ought to be automatable. Perhaps generic programming will help?

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

Most of the instances are pretty straightforward:

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

But then I get stuck. The straightforward thing for individual fields certainly doesn't work:

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

For recursive types, this is a very straightforward infinite loop. I've tried a variety of means of enriching the two classes involved here.

• I generalized cardinality and gcardinality to be functions, so that I could assume I already knew the size of recursive occurrences. Then in the K1 instance I could ask: if all your recursive instances were uninhabited, how big would you be? What if all your recursive instances had one inhabitant? And so on.
• I generalized from a single cardinality to a "recurrence relation" like x = a + bx. The intended meaning of x = a + bx is that the type x has a inhabitants that don't involve recursion at all, and b values that can be paired up with a recursive call. (We can define x*x = x without losing anything of interest.) Then equations like x = n + 0x correspond to enumerations, x = 0 + x correspond to trivial 1-element recursive types, and x = a + bx are infinite.
• I used lazy naturals instead of efficient ones.
• I tracked sets of possible cardinalities, ruling them out one by one as new information was learned.
• I took a stab at using Generic1 instead of Generic.

None of these ended up working well. There seem to be three core, hard problems/failure modes:

• A loop in the K1 definition for recursive types, or it works okay for recursive types but falls over for mutually recursive types.
• K1 is used both for recursive occurrences and plain fields, and there doesn't seem to be an easy way to distinguish between these.
• Choosing Finite 0 instead of Finite 1 for trivially recursive types.

Is there an approach that solves these problems? Where the generic instances for [Void], [()], X, and Y from above are all defined and correct?

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

As Li-yao Xia remarks, the last one doesn't really make sense, as never Never has no NF non-⊥ values. Not sure if there's a good way to take that into account.