How to prove the number of possible functions?

Question

Looking for an ad function, for example:

myFoo :: Bool -> Bool

I could say that a function myFoohas four possible unique implementations, since the type of the function is the exponent operator, here is the proof from the above case 2^2 = 4:

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


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

Like my following data declaration:

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

and the following function:

funcQuad :: Quad -> Quad

Possible implementation: 256(4^4). I can not imagine it, there is a lot of implementation.

How can I prove without writing it out?

Answer 1

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

There are 3 main types of designs:

• Type of sum: canonically Either a bwritten as a + b in type algebra
• : (a, b), × b
• (), a -> b, b ^a

, (), 1, Void, 0.

(, , ..), " ". . .

(.. ), , , 1 + 1 + ... + 1 n 1 s, n .

Quad 1 + 1 + 1 + 1 4. Quad -> Quad 4 ⁴ 256.

Answer 2

f: A & rightarrow; B x & mapsto; F (X). A B , , | B | ^{| |.}

. x & in; A, | B | f (x) . x b & in; B, | B | & ; | B | & ;... & times; | B | = | B | ^{| |.}

Quad, f :: Quad -> Quad, A = B = Quad. , | A | = | B | = 4 ( , ). , , 4 ⁴= 256 .

, fuctions g :: Quad -> Bool 16: A = Quad B = Bool, , | A | = 4 | B | = 2, 2 ⁴= 16. :

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

, f :: a -> b -> c. a -> b -> c a -> (b -> c). , f :: Quad -> (Quad -> Bool). Quad -> Bool 16, , A = Quad B = (Quad -> Bool) , , | A | = 4 | B | = 16. 16 ⁴= 65 536 . , , , .

Answer 3

, Quad= 4 Quad -> Quad= 4 ⁴. , , 256 Quad -> Quad.

4 ⁴= 4 & times; 4 ; 4 ; 4. (Quad, Quad, Quad, Quad). :

type Quad4 = (Quad, Quad, Quad, Quad)

tupleToFunction :: Quad4 -> (Quad -> Quad)
tupleToFunction (a, b, c, d) x = case x of
  One -> a
  Two -> b
  Three -> c
  Four -> d

functionToTuple :: (Quad -> Quad) -> Quad4
functionToTuple f = (f One, f Two, f Three, f Four)

: Quad4 4- 4, 0000 ₄= 0 = (One, One, One, One) 3333 ₄= 255 = (Four, Four, Four, Four).

. , ; "" . , Quad -> Quad Word8!

You can also do this by extending the product type (tuple) to the sum types ( Either). For Quadit would be great, but here is how you did it with Bool -> Bool= 2 ² = 2 & times; 2 = 2 + 2:

type BB = Either Bool Bool

eitherToFunction :: BB -> (Bool -> Bool)
eitherToFunction (Left a) _ = a
eitherToFunction (Right a) b = a == b  -- xnor

Now we can imagine const Truehow Left True, const Falsehow Left False, idhow Right Trueand nothow Right False, and we write the other half of the isomorphism, respectively

functionToEither :: (Bool -> Bool) -> BB
functionToEither f
  | f True && f False = Left True
  | f True = Right True
  | f False = Right False
  | otherwise = Left False