[3] FUNCTIONS REVISITED
- 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
Example:
- 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:
Post a Comment