Counting type inhabitants.

Last modified on September 22, 2018 by Alex


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

You might also check out Wikipeida page on universal quantification to learn how to move forall a around.

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!

Techniques

-- Regular Yoneda lemma for functors.
Functof f => ( x. (a -> x) -> f x) ~ f a      
-- Yoneda in the functor category.
( g. (f ~> g) -> g a) ~ f a
-- Recursion.
Functor f => ( x. (f x -> x) -> x) ~ μ x. f x

-- A morphism from initial object.
(0 -> a) ~ 1
-- A morphism from terminal object.
(1 -> a) ~ a