# Counting type inhabitants.

# Counting inhabitants of rank-0 types.

```
Void ~ 0
() ~ 1
Bool ~ 2
Either a b ~ a + b
(a, b) ~ a * b
```

Now `a -> b`

is a little bit different in the case where we have (parametric) type polymorphism, as we’ll see later. But if both `a`

and `b`

are some fixed known types (e.g. `Bool`

or `Either [Bool] Int`

), then:

`a -> b ~ b ^ a`

Pretty boring, so no comments.

```
Either Bool (Maybe Bool)
~ 2 + (1 + 2)
~ 5
```

```
Bool -> Bool
~ 2 -> 2
~ 2^2
~ 4
```

```
Maybe Bool -> Bool
~ (1 + 2) -> 2
~ 2^3
~ 8
```

```
Bool -> Maybe Bool
~ 2 -> (1 + 2)
~ 3^2
~ 9
```

```
(Bool, Bool, Bool) -> ()
~ (2 * 2 * 2) -> 1
~ 1^8
~ 1
```

```
() -> Bool
~ 1 -> 2
~ 2
```

Please see Any is a final object for an explanation of this one.

```
Any -> ()
~ 1 -> 1
~ 1
```

# Counting inhabitants of rank-1 simple-kinded types. 1

First, we need to discuss Yoneda lemma. If `f`

is a `Functor`

, then:

`(∀ x. (a -> x) -> f x) ~ f a`

In order to show that there is indeed an isomorphism, we first construct two functions going between these types:

```
to :: (∀ x. (a -> x) -> f x) -> f a
to f = f id
from :: Functor f => f a -> (∀ x. (a -> x) -> f x)
from fa = \f -> fmap f fa
```

Now we prove that `to . from = id`

and `from . to = id`

:

```
to . from $ fa = to $ \f -> fmap f fa = fmap id fa = fa
from . to $ f = from $ f id = \g -> fmap g (f id)
```

We’ve encountered a problem proving that `from . to = id`

. This apparently follows from free theorems [WIP].

Another trick we will often be using is that

```
a ~ 1 -> a -- unit introduction
(a, a) ~ 2 -> a
```

And further down we’ll also need

```
(0 -> a) ~ 1
(n -> a) -> (m -> a) -> x ~ ((n + m) -> a) -> x
```

### Simple examples

```
∀ a. a -> a
-- a ~ 1 -> a
~ ∀ a. (1 -> a) -> a
-- Yoneda with f x = x
~ 1
```

```
∀ a b. (a, b) -> a
-- uncurrying
~ ∀ a b. b -> a -> a
-- 1 -> b ~ b
~ ∀ a b. (1 -> b) -> a -> a
-- Yoneda with f x = a -> a
~ ∀ a. a -> a
-- reusing the above proof
~ 1
```

```
∀ a. (a, a) -> a
-- (a, a) ~ 2 -> a
~ ∀ a. (2 -> a) -> a
-- Yoneda with f x = a -> a
~ 2
```

```
∀ a. (a, a) -> (a, a)
-- (a, a) ~ 2 -> a
~ ∀ a. (2 -> a) -> (a, a)
-- Yoneda with f x = (x, x)
~ (2, 2)
~ 4
```

```
∀ a b c. (a -> c) -> b -> a -> c
-- Yoneda with f x = b -> a -> x
~ ∀ a b. b -> a -> a
-- reusing one of the above theorems
~ 1
```

```
∀ a b c. (a -> b) -> (b -> c) -> a -> c
~ ∀ a b. (a -> b) -> ∀ c. (b -> c) -> a -> c
-- Yoneda with f x = a -> x
~ ∀ a b. (a -> b) -> a -> b
-- Yoneda with f x = a -> x
~ ∀ a. a -> a
-- reusing one of the above theorems
~ 1
```

```
∀ a b. (a -> b) -> b -> a -> b
~ ∀ a b. ((a + 1) -> b) -> a -> b
-- Yoneda with f x = a -> x
~ ∀ a. a -> (a + 1)
-- a ~ 1 -> a
~ ∀ a. (1 -> a) -> (a + 1)
-- Yoneda with f x = x + 1
~ 1 + 1
~ 2
```

```
∀ a b c. (a -> b) -> b -> a -> c
-- (0 -> c) -> x ~ x
~ ∀ a b c. (0 -> c) -> ((a -> b) -> b -> a -> c)
-- Yoneda with f x = (a -> b) -> b -> a -> x
~ ∀ a b. (a -> b) -> b -> a -> 0
~ ∀ a. (∀ b. (a -> b) -> b) -> a -> 0
~ ∀ a. a -> a -> 0
~ ∀ a. (2 -> a) -> 0
-- to prove that ∀ a. f a -> 0 is uninhabited
-- we need to prove that f a is inhabited for at least one a
-- substitute a = 1, we get
-- (2 -> 1) ~ 1
-- hence
~ 0
```

```
∀ a. (0 -> a) -> a -> 0
~ ∀ a. (0 -> a) -> (1 -> a) -> 0
~ ∀ a. (1 -> a) -> 0
-- Yoneda with f x = 0
~ 0
```

```
∀ a b. (a -> 0, b) -> 2 * b
~ ∀ a b. b -> (a -> 0) -> 2 * b
-- Yoneda
~ ∀ a. (a -> 0) -> 2
-- Add (0 -> a) ~ 1
~ ∀ a. (0 -> a) -> (a -> 0) -> 2
-- Yoneda
~ (0 -> 0) -> 2
~ 1 -> 2
~ 2
```

```
∀ a. (a -> 0) -> 0
~ ∀ a. (0 -> a) -> (a -> 0) -> 0
~ (0 -> 0) -> 0
~ 1 -> 0
~ 0
```

```
∀ a. (a -> 0) -> a -> 0
~ ∀ a. a -> (a -> 0) -> 0
~ (1 -> 0) -> 0
~ 0 -> 0
~ 1
```

```
∀ a. (a -> 0, a -> 0) -> (a -> 0)
~ ∀ a. a -> 2 * (a -> 0) -> 0
~ ∀ a. (1 -> a) -> 2 * (a -> 0) -> 0
~ 2 * (1 -> 0) -> 0
~ 2 * 0 -> 0
~ 1
```

But what to do about `∀ a. (a -> a) -> (a -> a)`

? Intuitively, we know that the answer is `ω`

(a countable number of inhabitants) as `\f -> f`

, `\f -> f . f`

, `\f -> f . f . f`

, etc are all valid expressions satisfying that type. Can we make this proof more rigorous and less syntax-dependent?

Well, time for big guns,

```
∀ a. (a -> a) -> a -> a
-- (a -> a, a) ~ (1 + a) -> a
~ ∀ a. ((1 + a) -> a) -> a
-- define f x = 1 + x
~ ∀ a. (f a -> a) -> a
~ μ x. f x
~ ω
```

```
∀ a b. (a -> b -> a) -> a -> b -> a
-- move parameters around
~ ∀ a b. b -> (a -> b -> a) -> a -> a
~ ∀ a b. b -> ((a * b + 1) -> a) -> a
~ ∀ b. b -> (μ x. x * b + 1)
-- Yoneda
~ μ x. x * () + 1
~ ω
```

```
∀ a. (a -> a) -> a
-- f x = x
~ μ x. x
~ 0
```

Is there a mechanical way to check if `μ x. f x`

is inhabited?

## What is not free about Functor laws?

Suppose that `F :: * -> *`

is a functor, we write some implementation of `fmap :: forall a b. (a -> b) -> F a -> F b`

for it, what should we look out for?

```
∀ a b. (a -> b) -> F a -> F b
-- f b = F a -> F b
-- if F is a functor,
~ ∀ a. F a -> F a
~ F :~> F
```

So `fmap ~ F :~> F`

, meaning that the only freedom in implementing `fmap`

that we have is modifying the context (`F`

) without modifying the contents (`a`

) of `F a`

. This explains why `fmap id = id`

is crucially important, if this law were to be omitted, we could write an `fmap`

that combines a natural transformation of `F :~> F`

with lifting of `a -> b`

to `F a -> F b`

.

## Another way to derive theorems for free?

```
∀ a. (a -> Bool) -> F a -> F a
~ ∀ a. (F a, a -> Bool) -> F a
-- G x = (F x, x -> Bool)
~ G :~> F
-- C a b = (a -> b, b -> a)
-- D a b = a -> b
-- α . (G f) = (F f) . α
```

This section is still WIP, but here is something to think about: can every free theorem be expressed as a sufficient condition for some `F :~> G`

to be a natural transformation?

# Counting inhabitants for rank-N and higher-kinded types.

```
∀ f. f A -> f B
-- define g x = (x = A)
-- f A ~ g :~> f
~ ∀ f. (g :~> f) -> f B
-- Yoneda
~ g B
~ A = B
```

```
∀ f a b. f (G a) -> f (G b)
~ ∀ a b. ∀ f. f (G a) -> f (G b)
-- using the theorem above
~ ∀ a b. G a = G b
```

This is really tricky and we’ll have to take a pause and talk about…

### Bounding the number of inhabitants above.

Consider any polymorphic type `∀ a. f a`

, can we say anything about the number of its inhabitants by instantiating `a`

with different types?

Can the number of instances increase because of instantiation? Most certainly!

```
∀ a. a -> a ~ 1
-- but
2 -> 2 ~ 4
```

Can the number of instances decrease because of instantiation? Yes:

```
∀ a. (a, a) -> a ~ 2
-- but
(0, 0) -> 0 ~ 1
-- and
(1, 1) -> 1 ~ 1
```

Well, I will figure it out later.

# Counting inhabitants of types given laws.

Is hard!