How to proof the number of possible functions?

Question

Looking at function declaration, for example:

myFoo :: Bool -> Bool

I could say, the function myFoo has four possible unique implementation because function type is the exponent operator, here is the proof from the case above 2^2 = 4:

myFoo1 :: Bool -> Bool
myFoo1 True = False 
myFoo1 True = True


myFoo2 :: Bool -> Bool
myFoo2 False = False 
myFoo2 False = True

How I have following data declaration:

data Quad =
  One
  | Two
  | Three
  | Four
  deriving (Eq, Show)

and following function:

funcQuad :: Quad -> Quad

possible implementations are 256(4^4). I can not image it, there are a lot of implementation.

How can I proof without writing it out?

Answer 1

You can use algebra to count the number of inhabitant of a type.

There are 3 main type constructions:

• The sum type: Either a b, written as a + b
• The product type: (a, b), written as a × b
• The exponent (arrow) type, a -> b, written as b^a

There are also some basic types such as the unit type (), written as 1, and the empty type Void, written as 0.

Most of the common algebra work on types (distribution, commutativity, powers, etc...). The underlying meaning of the resulting expression is the number of inhabitants of your type. Equality can be translated as isomorphisms in the type world.

For an enumeration (i.e. the union of nullary constructors) like yours, we usually write that as 1 + 1 + ... + 1 with n 1s, given n the number of constructors.

Here, your Quad type translates as 1 + 1 + 1 + 1 in types, and that can be reduced as 4. Then, your Quad -> Quad type is written as 4⁴, which is 256.

Answer 2

A function f : A → B maps values x ↦ f(x). Given A and B are finite sets, than the number of possible functions, is limited to |B| ^|A|.

We can proof this by simple combinatorics. For every x ∈ A, there are |B| possible values to map f(x) to. For every such x we can independently pick a value b ∈ B, so as a result the total number of possible values is |B| × |B| × ... × |B| = |B| ^|A|.

For the Quad type, if you construct a function f :: Quad -> Quad, the A = B = Quad. That means that |A| = |B| = 4 (since there are four possible values, and none have parameters). So that means there are 4⁴=256 possibilities.

The number of fuctions g :: Quad -> Bool is thus 16: since A = Quad and B = Bool, this means that |A| = 4 and |B| = 2, so the number of possible functions is 2⁴=16. These are the following:

g01 One   = False
g01 Two   = False
g01 Three = False
g01 Four  = False

g02 One   = False
g02 Two   = False
g02 Three = False
g02 Four  = True

g03 One   = False
g03 Two   = False
g03 Three = True
g03 Four  = False

g04 One   = False
g04 Two   = False
g04 Three = True
g04 Four  = True

g05 One   = False
g05 Two   = True
g05 Three = False
g05 Four  = False

g06 One   = False
g06 Two   = True
g06 Three = False
g06 Four  = True

g07 One   = False
g07 Two   = True
g07 Three = True
g07 Four  = False

g08 One   = False
g08 Two   = True
g08 Three = True
g08 Four  = True

g09 One   = True
g09 Two   = False
g09 Three = False
g09 Four  = False

g10 One   = True
g10 Two   = False
g10 Three = False
g10 Four  = True

g11 One   = True
g11 Two   = False
g11 Three = True
g11 Four  = False

g12 One   = True
g12 Two   = False
g12 Three = True
g12 Four  = True

g13 One   = True
g13 Two   = True
g13 Three = False
g13 Four  = False

g14 One   = True
g14 Two   = True
g14 Three = False
g14 Four  = True

g15 One   = True
g15 Two   = True
g15 Three = True
g15 Four  = False

g16 One   = True
g16 Two   = True
g16 Three = True
g16 Four  = True

Finally one can ask about the number of functions f :: a -> b -> c. a -> b -> c is short for a -> (b -> c). So the number of functions f :: Quad -> (Quad -> Bool). Since the number of function Quad -> Bool is 16, this thus means that A = Quad and B = (Quad -> Bool) and thus |A| = 4 and |B| = 16. This results in a total of 16⁴=65 536 possible functions. Since the number of possible implementations increases very fast, exhaustively enumerating them will thus easily become unfeasible.