← | →

Cardinality of types

Posted on Sunday, 11 May 2008 at 21:44.

In a recent blog entry, Dan Piponi wondered how many functions f :: () -> () there are. When interpreting the question in the widest sense, his answer was 5, taking the special “value” bottom into account. (Whether bottom actually is a value or not is a discussion on its own.) We’re going to answer this question for arbitrary types. Because types can be seen as sets of values, the number of values that a type comprises is called the type’s cardinality.

Let’s start with representing types:

{-# OPTIONS_GHC -XEmptyDataDecls #-}

data Type
  = D [Constructor]
  | Type :-> Type

infixr :->

data Constructor
  = C Name [Type]

type Name = String

In other words: a type is either a datatype with zero or more constructors, or a function from a domain to a codomain. A constructor has fields, each of a specific type. We give each constructor a name, too. This isn’t necessary to answer the cardinality question, but it will come in handy later on.

Let’s see how certain types translate to this representation. First, the simplest data type we can think of: void. It has no constructors; hence the flag at the top.

-- data Void
void :: Type
void = D []

Types with one and two constructors, respectively, both with no fields:

-- data () = ()
unit :: Type
unit = D [C "()" []]

-- data Bool = False | True
bool :: Type
bool = D [C "False" [], C "True" []]

We represent type constructors as functions taking Types and yielding a Type:

-- data Maybe a = Nothing | Just a
maybe :: Type -> Type
maybe a = D [C "Nothing" [], C "Just" [a]]

-- data Either a b = Left a | Right b
either :: Type -> Type -> Type
either a b = D [C "Left" [a], C "Right" [b]]

Notice how, since we’re pulling types one level down to the value level, kinds are suddenly pulled down to the type level! Either :: * -> * -> *, and indeed either :: Type -> Type -> Type.

We can do recursion, too:

-- data Peano = Zero | Succ Peano
peano :: Type
peano = D [C "Zero" [], C "Succ" [peano]]

-- data [a] = [] | a : [a]
list :: Type -> Type
list a = D [C "Cons" [a, list a], C "[]" []]

Let’s take a look at some non-trivial kinds:

-- GRose :: (* -> *) -> * -> *
-- data GRose f a = GRose a (f (GRose f a))
grose :: (Type -> Type) -> Type -> Type
grose f a = D [C "GRose" [a, f (grose f a)]]

-- Fix :: (* -> *) -> *
-- data Fix f = In (f (Fix f))
fix :: (Type -> Type) -> Type
fix f = D [C "In" [f (fix f)]]

Again, the types perfectly mimic the kinds.

Let’s see what happens with kind polymorphism:

-- Apply :: (k -> *) -> k -> *
-- data Apply f a = A (f a)
apply :: Kind t => (t -> Type) -> t -> Type
apply f a = D [C "Apply" [f a]]

Here the argument t -> Type would be too liberal if we didn’t constrain t to be (have?) a kind. We don’t want apply to accept a function of type Int -> Type, for example. This is how we can demand that t consists of only functions and Types:

class Kind k where
instance Kind Type where
instance (Kind a, Kind b) => Kind (a -> b) where

Finally, we can represent Integer as if it were a data type with infinitely many zero-field constructors. Here we can make use of the weave function we talked about last time, to interleave the positive and the negative integers:

-- data Integer = 0 | -1 | 1 | -2 | 2 | -3 | 3 | -4 | 4 | ...
integer :: Type
integer = D (map mkc is) where
  is    = weave [[0..], [(-1), (-2)..]]
  mkc i = C (show i) []

weave :: [[a]] -> [a]
weave = concat . transpose

Now we’re ready to compute a type’s cardinality:

class Card a where
  card :: a -> Integer

instance Card Type where
  card (D cs)    = sum (map card cs) + 1  -- + 1 for bottom
  card (a :-> b) = card b ^ card a   + 1  -- + 1 for bottom

instance Card Constructor where
  card (C _ ts)  = product (map card ts)

In words: for datatypes, we compute the cardinality of the datatype’s constructors and sum these up, since a datatype is a choice of constructors. For constructors, we take the product of its fields’ cardinalities, because a specific value instance of a constructor is a combination of choices from its fields. For functions, we raise the right side to the power of the left side: for a specific function value, we must make card a choices, each choice consisting of card b options.

Let’s see if we can reproduce Dan’s answer:

> card (unit :-> unit)
5

Yup! That works. Some more examples:

> card bool
3
> card (void :-> bool)
4
> card (maybe bool)
5
> card (either unit bool)
6

If some of these numbers look surprising, take a look at this image from Wikibooks demonstrating the values of Maybe Bool.

As expected, card never produces an answer when asked to compute the cardinality of an infinite type, such as Integer or [Bool].

With our current representation, there are a few things we cannot express:

Have I forgotten anything?

Leave a comment!

Martijn loves to receive comments! Add yours by filling out the fields below.