# Difference between revisions of "Free structure"

From HaskellWiki

(change 'injection' to 'embedding' in the informal description of freeness, since injectivity isn't necessarily implied.) |
Tomjaguarpaw (talk | contribs) (Deleting page that hasn't been edited for over 10 years) |
||

Line 1: | Line 1: | ||

− | [[Category:Glossary]] |
||

− | [[Category:Theoretical foundations]] |
||

− | [[Category:Mathematics]] |
||

− | |||

− | === Introduction === |
||

− | |||

− | This article attempts to give a relatively informal understanding of "free" structures from algebra/category theory, with pointers to some of the formal material for those who desire it. The later sections make use of some notions from [[category theory]], so some familiarity with its basics will be useful. |
||

− | |||

− | === Algebra === |
||

− | |||

− | ==== What sort of structures are we talking about? ==== |
||

− | |||

− | The distinction between free structures and other, non-free structures, originates in [http://en.wikipedia.org/wiki/Abstract_algebra abstract algebra], so that provides a good place to start. Some common structures considered in algebra are: |
||

− | |||

− | * '''[[Monoid]]s''' |
||

− | ** consisting of |
||

− | *** A set <math>M</math> |
||

− | *** An identity <math>e \in M</math> |
||

− | *** A binary operation <math>* : M \times M \to M</math> |
||

− | ** And satisfying the equations |
||

− | *** <math> x * (y * z) = (x * y) * z </math> |
||

− | *** <math> e * x = x = x * e </math> |
||

− | |||

− | * '''[http://en.wikipedia.org/wiki/Group_(mathematics) Groups]''' |
||

− | ** consisting of |
||

− | *** A monoid <math>(M, e, *)</math> |
||

− | *** An additional unary operation <math>\,^{-1} : M \to M</math> |
||

− | ** satisfying |
||

− | *** <math> x * x^{-1} = e = x^{-1} * x</math> |
||

− | |||

− | * '''[http://en.wikipedia.org/wiki/Ring_(mathematics) Rings]''' |
||

− | ** consisting of |
||

− | *** A set <math>R</math> |
||

− | *** A unary operation <math>- : R \to R</math> |
||

− | *** Two binary operations <math> +, * : R \times R \to R</math> |
||

− | *** Distinguished elements <math>0, 1 \in R</math> |
||

− | ** such that |
||

− | *** <math>(R, 0, +, -)</math> is a group |
||

− | *** <math>(R, 1, *)</math> is a monoid |
||

− | *** <math> x + y = y + x </math> |
||

− | *** <math> (x + y)*z = x*z + y*z </math> |
||

− | *** <math> x * (y + z) = x*y + x*z </math> |
||

− | |||

− | So, for algebraic structures, we have sets equipped with operations that are expected to satisfy equational laws. |
||

− | |||

− | ==== Free algebraic structures ==== |
||

− | |||

− | Now, given such a description, we can talk about the free structure over a particular set <math>S</math> (or, possibly over some other underlying structure; but we'll stick with sets now). What this means is that given <math>S</math>, we want to find some set <math>M</math>, together with appropriate operations to make <math>M</math> the structure in question, along with the following two criteria: |
||

− | |||

− | * There is an embedding <math>i : S \to M</math> |
||

− | * The structure generated is as 'simple' as possible. |
||

− | ** <math>M</math> should contain only elements that are required to exist by <math>i</math> and the operations of the structure. |
||

− | ** The only equational laws that should hold for the generated structure are those that are required to hold by the equational laws for structures of that type. |
||

− | |||

− | So, in the case of a free monoid (from here on out, we'll assume that the structure in question is a monoid, since it's simplest), the equation <math>x * y = y * x</math> should not hold unless <math>x = y</math>, <math>x = e</math> or <math>y = e</math>. Further <math>i x \in M</math>, for all <math>x</math>, and <math>e \in M</math>, and <math>\forall x, y \in M.\,\, x * y \in M</math> (and these should all be distinct, except as required by the monoid laws), but there should be no 'extra' elements of <math>M</math> in addition to those. |
||

− | |||

− | For monoids, the free structure over a set is given by the monoid of lists of elements of that set, with concatenation as multiplication. It should be easy to convince yourself of the following (in pseudo-Haskell): |
||

− | |||

− | <haskell> |
||

− | M = [S] |
||

− | e = [] |
||

− | * = (++) |
||

− | |||

− | i : S -> [S] |
||

− | i x = [x] -- i x = x : [] |
||

− | |||

− | [] ++ xs = xs = xs ++ [] |
||

− | xs ++ (ys ++ zs) = (xs ++ ys) ++ zs |
||

− | |||

− | xs ++ ys = ys ++ xs iff xs == ys || xs == [] || ys == [] |
||

− | -- etc. |
||

− | </haskell> |
||

− | |||

− | === The category connection === |
||

− | |||

− | ==== Free structure functors ==== |
||

− | |||

− | One possible objection to the above description (even a more formal version thereof) is that the characterization of "simple" is somewhat vague. [[Category theory]] gives a somewhat better solution. Generally, structures-over-a-set will form a category, with arrows being structure-preserving homomorphisms. "Simplest" (in the sense we want) structures in that category will then either be [http://en.wikipedia.org/wiki/Initial_and_terminal_objects initial or terminal], [1] and thus, freeness can be defined in terms of such universal constructions. |
||

− | |||

− | In its [http://en.wikipedia.org/wiki/Free_object full categorical generality], freeness isn't necessarily categorized by underlying set structure, either. Instead, one looks at "forgetful" functors [2] from the category of structures to some other category. For our free monoids above, it'd be: |
||

− | |||

− | * <math>U : Mon \to Set</math> |
||

− | |||

− | The functor taking monoids <math>(M, e, *)</math> to their underlying set <math>M</math>. Then, the relevant universal property is given by finding an [http://en.wikipedia.org/wiki/Adjunction adjoint functor]: |
||

− | |||

− | * <math>F : Set \to Mon</math>, <math> F</math> ⊣ <math>U </math> |
||

− | |||

− | <math>F</math> being the functor taking sets to the free monoids over those sets. So, free structure functors are left adjoint to forgetful functors. It turns out this categorical presentation also has a dual: cofree structure functors are right adjoint to forgetful functors. |
||

− | |||

− | ==== Algebraic constructions in a category ==== |
||

− | |||

− | Category theory also provides a way to extend specifications of algebraic structures to more general categories, which can allow us to extend the above informal understanding to new contexts. For instance, one can talk about monoid objects in an arbitrary [http://en.wikipedia.org/wiki/Monoidal_category monoidal category]. Such categories have a tensor product <math>\otimes</math> of objects, with a unit object <math>I</math> (both of which satisfy various laws). |
||

− | |||

− | A monoid object in a monoidal category is then: |
||

− | |||

− | * An object <math>M</math> |
||

− | * A unit 'element' <math>e : I \to M</math> |
||

− | * A multiplication <math>m : M \otimes M \to M</math> |
||

− | |||

− | such that: |
||

− | |||

− | * <math>m \circ (id_{M} \otimes e) = u_l</math> |
||

− | * <math>m \circ (e \otimes id_M) = u_r</math> |
||

− | * <math> m \circ (id_M \otimes m) = m \circ (m \otimes id_M) \circ \alpha</math> |
||

− | |||

− | Where: |
||

− | |||

− | * <math>u_l : M \otimes I \to M</math> and <math>u_r : I \otimes M \to M</math> are the identity isomorphisms for the monoidal category, and |
||

− | * <math> \alpha : M \otimes (M \otimes M) \to (M \otimes M) \otimes M </math> is part of the associativity isomorphism of the category. |
||

− | |||

− | So, hopefully the connection is clear: we've generalized the carrier set to a carrier object, generalized the operations to morphisms in a category, and equational laws are promoted to being equations about composition of morphisms. |
||

− | |||

− | ==== Monads ==== |
||

− | |||

− | One example of a class of monoid objects happens to be [[monad (sans metaphors)|monads]]. Given a base category <math>C</math>, we have the monoidal category <math>C^C</math>: |
||

− | |||

− | * Objects are endofunctors <math>F : C \to C</math> |
||

− | * Morphisms are [[Category theory/Natural transformation|natural transformations]] [3] between the functors |
||

− | * The tensor product is composition: <math>F \otimes G = F \circ G</math> |
||

− | * The identity object is the identity functor, <math>I</math>, taking objects and morphisms to themselves |
||

− | |||

− | If we then specialize the definition of a monoid object to this situation, we get: |
||

− | |||

− | * An endofunctor <math>M : C \to C</math> |
||

− | * A natural transformation <math>\eta : I \to M</math> |
||

− | * A natural transformation <math>\mu : M \circ M \to M</math> |
||

− | |||

− | which satisfy laws that turn out to be the standard monad laws. So, monads turn out to be monoid objects in the category of endofunctors. |
||

− | |||

− | ==== Free Monads ==== |
||

− | |||

− | But, what about our intuitive understanding of free monoids above? We wanted to promote an underlying set, but we have switched from sets to functors. So, presumably, a free monad is generated by an underlying (endo)functor, <math>F : C \to C</math>. We then expect there to be a natural transformation <math>i : F \to M</math>, 'injecting' the functor into the monad. |
||

− | |||

− | In Haskell, we can write the type of free monads over Haskell endofunctors as follows: |
||

− | |||

− | <haskell> |
||

− | data Free f a = Return a | Roll (f (Free f a)) |
||

− | |||

− | instance Functor f => Monad (Free f) where |
||

− | return a = Return a |
||

− | Return a >>= f = f a |
||

− | Roll ffa >>= f = Roll $ fmap (>>= f) ffa |
||

− | |||

− | -- join (Return fa) = fa |
||

− | -- join (Roll ffa) = Roll (fmap join ffa) |
||

− | |||

− | inj :: Functor f => f a -> Free f a |
||

− | inj fa = Roll $ fmap Return fa |
||

− | </haskell> |
||

− | |||

− | This should bear some resemblance to free monoids over lists. <code>Return</code> is analogous to <code>[]</code>, and <code>Roll</code> is analogous to <code>(:)</code>. Lists let us create arbitrary length strings of elements from some set, while <code>Free f</code> lets us create structures involving <code>f</code> composed with itself an arbitrary number of times (recall, functor composition was the tensor product of our category). <code>Return</code> gives our type a way to handle the 0-ary composition of <code>f</code> (as <code>[]</code> is the 0-length string), while <code>Roll</code> is the way to extend the nesting level by one (just as <code>(:)</code> lets us create (n+1)-length strings out of n-length ones). Finally, both injections are built in a similar way: |
||

− | |||

− | <haskell> |
||

− | inj_list x = (:) x [] |
||

− | inj_free fx = Roll (fmap Return fx) |
||

− | </haskell> |
||

− | |||

− | This, of course, is not completely rigorous, but it is a nice extension of the informal reasoning we started with. |
||

− | |||

− | === Further reading === |
||

− | |||

− | For those looking for an introduction to the necessary category theory used above, Steve Awodey's [http://www.math.uchicago.edu/~may/VIGRE/VIGRE2009/Awodey.pdf Category Theory] is a popular, freely available reference. |
||

− | |||

− | === Notes === |
||

− | |||

− | ==== Universal constructions ==== |
||

− | |||

− | Initial (final) objects are those that have a single unique arrow from (to) the object to (from) every other object in the category. For instance, the empty set is initial in the category of sets, and any one-element set is final. Initial objects play an important role in the semantics of algebraic datatypes. For a datatype like: |
||

− | |||

− | <haskell> |
||

− | data T = C1 A B C | C2 D E T |
||

− | </haskell> |
||

− | |||

− | we consider the following: |
||

− | |||

− | * A functor <math>F : Hask \to Hask</math>, <math>F X = A \times B \times C + D \times E \times X</math> |
||

− | * F-algebras which are: |
||

− | ** An object <math>A \in Hask</math> |
||

− | ** An action <math>a : FA \to A</math> |
||

− | * Algebra homomorphisms <math>(A, a) \to (B, b)</math> |
||

− | ** These are given by <math>h : A \to B</math> such that <math> b \circ Fh = h \circ a</math> |
||

− | |||

− | The datatype <code>T</code> is then given by an initial F-algebra. This works out nicely because the unique algebra homomorphism whose existence is guaranteed by initiality is the [[fold]] or 'catamorphism' for the datatype. |
||

− | |||

− | Intuitively, though, the fact that <code>T</code> is an F-algebra means that it is in some sense closed under forming terms of shape F---suppose we took the simpler signature <code>FX = 1 + X</code> of the natural numbers; then both Z = inl () and Sx = inr x can be incorporated into Nat. However, there are potentially many algebras; for instance, the naturals modulo some finite number, and successor modulo that number are an algebra for the natural signature. |
||

− | |||

− | However, initiality constrains what Nat can be. Consider, for instance, the above modular sets 2 and 3. There can be no homomorphism <math>h : 2 \to 3</math>: |
||

− | |||

− | * <math>h0=0 \,\, ;\, h1=0</math> |
||

− | ** <math>S(h1) = S0 = 1\,</math> but <math>h(S1) = h0 = 0 \neq 1</math> |
||

− | * <math> h0=0 \,\,;\, h1=1</math> |
||

− | ** <math>S(h1) = S1 = 2\,</math> but <math>h(S1) = h0 = 0 \neq 2</math> |
||

− | * <math> h0=0 \,\,;\, h1=2</math> |
||

− | ** <math>S(h0) = S0 = 1\,</math> but <math>h(S0) = h1 = 2 \neq 2</math> |
||

− | * <math> h0 \neq 0 </math> |
||

− | ** <math> 0 = Z \neq hZ = h0</math> |
||

− | |||

− | This is caused by these algebras identifying elements in incompatible ways (2 makes SSZ = Z, but 3 doesn't, and 3 makes SSSZ = Z, but 2 doesn't). So, the values of an initial algebra must be compatible with any such identification scheme, and this is accomplished by identifying ''none'' of the terms in the initial algebra (so that h is free to send each term to an appropriate value in the target, according to the identifications there). A similar phenomenon occurs in the main section of this article, except that the structures in question have additional equational laws that terms must satisfy, so the initial structure ''is'' allowed to identify those, ''but no more'' than those. |
||

− | |||

− | By the same argument, we can determine that 3 is not a final algebra. Nor are the naturals (for any modular set M, S(h(M-1)) = S(M-1) = M, but h(S(M-1)) = h0 = 0). The final algebra is the set {0}, with S0 = 0 and Z = 0, with unique homomorphism hx = 0. This can be seen as identifying as many elements as possible, rather than as few. Naturally, final algebras don't receive that much interest. However, finality is an important property of [http://en.wikipedia.org/wiki/Initial_algebra#Final_coalgebra coalgebras]. |
||

− | |||

− | ==== Forgetful functors ==== |
||

− | |||

− | The term "forgetful functor" has no formal specification; only an intuitive one. The idea is that one starts in some category of structures, and then defines a functor by forgetting part or all of what defines those structures. For instance: |
||

− | |||

− | * <math>U : Str \to Set</math>, where <math>Str</math> is any category of algebraic structures, and U simply forgets about all of the n-ary operations and equational laws, and takes structures to their underlying sets, and homomorphisms to functions over those sets. |
||

− | * <math>U : Grp \to Mon</math>, which takes a group and forgets about the inverse operation to give a monoid. This functor would then be related to "free groups over a monoid". |
||

− | |||

− | ==== Natural transformations ==== |
||

− | |||

− | The wiki article gives a formal definition of natural transformations, but a Haskell programmer can think of a natural transformation between functors F and G as: |
||

− | |||

− | <haskell> |
||

− | trans :: forall a. F a -> G a |
||

− | </haskell> |