Personal tools

User:Michiexile/MATH198/Lecture 9

From HaskellWiki

< User:Michiexile | MATH198(Difference between revisions)
Jump to: navigation, search

Revision as of 18:03, 17 November 2009



1 Recursion patterns




1.1 Coalgebras for endofunctors








Onwards to recursion schemes!


  • We write μf for the fixed point operator
mu f = x where x = f x
  • MFP write (fΔg) for
  • MFP write (f\nabla g) x for
(Nabla f g) (Left x) = f x
(Nabla f g) (Right x) = g x




1.2 Catamorphisms




u :: Int
u = 0
m :: (A, Int) -> Int
m (a, n) = n+1
MFP define the catamorphism by, supposing
is initial for the functor


type T a = [a]
instance Functor (F a) where
  fmap _ Nil = Nil
outT [] = Nil
outT (a:as) = Cons a as
lphi :: F a Int -> Int
lphi Nil = 0
lphi (Cons a n) = n + 1
l = cata lphi
where we observe that
has a global definition for everything we do and
is defined once we settle on the functor
and its initial algebra. Thus, the definition of
really is the only place that the recursion data shows up.

1.3 Anamorphisms



Example: we can write a recursive function

first :: Int -> [Int]
first 1 = [1]
first n = n : first (n - 1)


c 0 = Left ()
c n = Right (n, n-1)

and we observe that we can chase through the diagram


to conclude that therefore

f 0 = []
f n = n : f (n - 1)

which is exactly the recursion we wrote to begin with.

MFP define the anamorphism by a fixpoint as well, namely:



-- Reuse mu, F, T from above
inT Nil = []
inT (Cons a as) = a:as
fpsi :: Int -> F Int Int
fpsi 0 = Nil
fpsi n = Cons n (n-1)
Again, we can note that the implementation of
here is exactly the
function above would.

1.4 Hylomorphisms



MFP define it, again, as a fix point:




phi :: F Int Int -> Int
phi Nil = 1
phi (Cons n m) = n*m
psi :: Int -> F Int Int
psi 0 = Int
psi n = Cons n (n-1)
factorial = hylo phi psi

1.5 Metamorphisms



1.6 Paramorphisms


1.7 Apomorphisms


2 Further reading


3 Further properties of adjunctions

3.1 RAPL

Proposition If F is a right adjoint, thus if F has a left adjoint, then F preserves limits in the sense that F(\lim_{\leftarrow} A_i) = \lim_{\leftarrow} F(A_i).

Example: (\lim_{\leftarrow_i} A_i)\times X = \lim_{\leftarrow_i} A_i\times X.

We can use this to prove that things cannot be adjoints - since all right adjoints preserve limits, if a functor G doesn't preserve limits, then it doesn't have a left adjoint.

Similarly, and dually, left adjoints preserve colimits. Thus if a functor doesn't preserve colimits, it cannot be a left adjoint, thus cannot have a right adjoint.

The proof of these statements build on the Yoneda lemma:

Lemma If C is a locally small category (i.e. all hom-sets are sets). Then for any c\in C_0 and any functor F: C^{op}\to Sets there is an isomorphism

hom_{hom_{Sets^{C^{op}}}}(yC, F) = FC

where we define yC = d\mapsto hom_C(d,c) : C^{op}\to Sets.

The Yoneda lemma has one important corollary:

Corollary If yA = yB then A = B.

Which, in turn has a number of important corollaries:

Corollary (A^B)^C = A^{B\times C}

Corollary Adjoints are unique up to isomorphism - in particular, if F: C\to D is a functor with right adjoints U, V: D\to C, then U = V.

Proof homC(C,UD) = homD(FC,D) = homC(C,VD), and thus by the corollary to the Yoneda lemma, UD = VD, natural in D.

3.2 Functors that are adjoints

  • The functor X\mapsto X\times A has right adjoint Y\mapsto Y^A. The universal mapping property of the exponentials follows from the adjointness property.
  • The functor \Delta: C\to C\times C, c\mapsto (c,c) has a left adjoint given by the coproduct (X,Y)\mapsto X + Y and right adjoint the product (X,Y)\mapsto X\times Y.
  • More generally, the functor C\to C^J that takes c to the constant functor constc(j) = c,constc(f) = 1c has left andright adjoints given by colimits and limits:
\lim_\rightarrow -| \Delta -| \lim_\leftarrow
  • Pointed rings are pairs (R, r\in R) of rings and one element singled out for attention. Homomorphisms of pointed rings need to take the distinguished point to the distinguished point. There is an obvious forgetful functor U: Rings_* \to Rings, and this has a left adjoint - a free ring functor that adjoins a new indeterminate R\mapsto (R[x], x). This gives a formal definition of what we mean by formal polynomial expressions et.c.
  • Given sets A,B, we can consider the powersets P(A),P(B) containing, as elements, all subsets of A,B respectively. Suppose f:A\to B is a function, then f^{-1}: P(B)\to P(A) takes subsets of B to subsets of A.
Viewing P(A) and P(B) as partially ordered sets by the inclusion operations, and then as categories induced by the partial order, f − 1 turns into a functor between partial orders. And it turns out f − 1 has a left adjoint given by the operation im(f) taking a subset to the set of images under the function f. And it has a right adjoint f_*(U) = \{b\in B: f^{-1}(b)\subseteq U\}
  • We can introduce a categorical structure to logic. We let L be a formal language, say of predicate logic. Then for any list x = x1,x2,...,xn of variables, we have a preorder Form(x) of formulas with no free variables not occuring in x. The preorder on Form(x) comes from the entailment operation - f | − g if in every interpretation of the language, f \Rightarrow g.
We can build an operation on these preorders - a functor on the underlying categories - by adjoining a single new variable: *: Form(x) \to Form(x, y), sending each form to itself. Obviously, if f | − g with x the source of free variables, if we introduce a new allowable free variable, but don't actually change the formulas, the entailment stays the same.
It turns out that there is a right adjoint to * given by f\mapsto \forall y. f. And a left adjoint to * given by f\mapsto \exists y. f. Adjointness properties give us classical deduction rules from logic.

4 Homework

  1. Write a fold for the data type
  2. Write the fibonacci function as a hylomorphism.
  4. Write a prime numbers generator as an anamorphism.
primes :: [Integer]
primes = sieve [2..]
data Tree = Leaf Integer | Node Integer [Tree]
divisionTree 60 = 
  Node 60 [
    Node 30 [
      Node 15 [
        Leaf 5,
        Leaf 3],
      Node 10 [
        Leaf 5,
        Leaf 2],
      Node 6 [
        Leaf 3,
        Leaf 2]],
    Node 20 [
      Node 10 [
        Leaf 5,
        Leaf 2],
      Node 4 [
        Leaf 2]],
    Node 12 [
      Node 6 [
        Leaf 3,
        Leaf 2],
      Node 4 [
        Leaf 2]]]