← Branddating | Readline Hell →

# Cardinality of types

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 `Type`

s 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 `Type`

s:

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:

- Type classes
- Rank-n polymorphism

Have I forgotten anything?

## Leave a comment!

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