Tuesday, July 22, 2008

[2008.07.22] Functions, Monoids and Monads [Part III/IV]


  • recall that functions under composition form a monoid of the same type, that is f·g = h:a -> a given that f:a -> a and g:a -> a
  • now let us modify the types of f and g such that:
    • f:a -> b
    • g:b -> c
  • now under composition, f·g = h but what is the type of h?
  • since f takes a type a and returns a type b, and g takes a type b and returns a type c, then the composition produces h:a -> c
  • it is important to note here that we can only compose this in one way
  • in this case, the composition does not form a monoid, instead, it forms a Monoidal Category which is part of the Category Theory branch of mathematics
  • so a monoidal category basically states that types need to line up
  • thus far you know all this from your experience in programming imperative languages like C# and VB where your types line up when you nest function calls
  • given the functions:
    • f:int -> int
    • g:int -> string
  • now what is the type of g (h a) ?
  • we know f a will return an int, so after f a is evaluated, conceptually we have something like g(int) and also know that g returns a string
  • therefore, g (f a) = h:int -> string

[1] Show that Function Composition is Associative

  • want to show that the composition operator, · , is associative, that is: (f · g) · h is equivalent to f · (g · h)
  • given the type system:
    • x:a
    • f:a -> a
    • g:a -> a
    • h:a -> a
  • take a look at the right hand side of our equation and expand by putting in an argument, a
    • this states that when we apply h to our argument a, and then apply g to that to get g (h a)
    • now if we compose f with the result, then the only way to apply that composition is to call f like f(g(h a))
  • take a look at the left hand side of the equation and expand by putting in an argument, a
    • this states that f compose g means that f is calling g, which is calling something else of type a
    • as we can see, there is only one way for this to happen, so g is actually calling h a which is written as f(g(h a)) and f is calling all that, which can only be done in one way: g(h a)
  • therefore, as you can see, function composition is associative

[2] Show Identity

  • there is a specific function called id of type a such that id:a -> a
  • id is defined such that if we apply id to any argument a, we get back a
  • now compose f with id such that (f · id)
    • expand by adding an argument to the expression such that we call id with an argument of type a such that id a
    • but we know that id a = a
    • now apply f to the result to get f(id a) = f a
  • therefore, f composed with id is f

No comments: