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?

user_745903 · Answer

{-# 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.

Can I compute a type's cardinality generically?

1 Answers