tag:blogger.com,1999:blog-3857512306503018420Sat, 31 Jan 2015 10:05:15 +0000NattermorphismsRamblings about Functional Programminghttp://nattermorphisms.blogspot.com/noreply@blogger.com (Ben)Blogger7125tag:blogger.com,1999:blog-3857512306503018420.post-1458009480450343029Fri, 15 Jun 2012 05:55:00 +00002012-06-15T06:55:57.227+01:00Unfolding with View PatternsA while back I across a way of looking at fold / unfold duality which I've not seen anywhere else. It makes use of view patterns to highlight the symmetry in the implementation of the two combinators.<br /><br />Firstly, for reference, the standard implementation:<br /><br /><span class="Apple-style-span" style="font-size: x-small;"></span><br /><blockquote class="tr_bq"><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">foldr :: (a -> b -> b) -> b -> [a] -> b<br />foldr f b [] = b<br />foldr f b (x : xs) = f x $ foldr f b xs</span></blockquote>Then we rewrite the inputs slightly:<span class="Apple-style-span" style="font-size: x-small;"></span><br /><blockquote class="tr_bq"><span class="Apple-style-span" style="font-size: x-small;"><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><br />foldr3 :: (() -> b,(a,b) -> b) -> [a] -> b<br />foldr3 (b,f) [] = b ()<br />foldr3 (b,f) (x : xs) = f (x, foldr3 (b,f) xs)<br /> </span></span></blockquote><span class="Apple-style-span" style="font-size: x-small;"></span>...and rewrite them a little more...:<span class="Apple-style-span" style="font-size: x-small;"></span><br /><blockquote class="tr_bq"><span class="Apple-style-span" style="font-size: x-small;"><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">-- | (+) -| Delta (Coproduct bifunctor is left adjoint to Diagonal functor)<br />foldr4 :: (Either () (a,b) -> b) -> [a] -> b<br />foldr4 f [] = f $ Left ()<br />foldr4 f (x : xs) = f $ Right (x, foldr4 f xs)</span></span></blockquote><br /><blockquote class="tr_bq"><span class="Apple-style-span" style="font-size: x-small;"><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"></span></span><br /><div style="margin-bottom: 0px; margin-left: 0px; margin-right: 0px; margin-top: 0px;">...now we can create 'unfoldr' just by swapping the LHS and RHS of the definitions of 'foldr4':<span class="Apple-style-span" style="font-size: x-small;"></span></div><blockquote class="tr_bq"></blockquote><span class="Apple-style-span" style="font-size: x-small;"><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">-- | Now just swap the LHS and RHS of the '=' !!!<br />unfoldr2 :: (b -> Either () (a,b)) -> b -> [a]<br />unfoldr2 f (f -> Left () ) = []<br />unfoldr2 f (f -> Right (x, unfoldr2 f -> xs)) = (x : xs)</span></span></blockquote><span class="Apple-style-span" style="font-size: x-small;"><div style="font-family: Calibri, sans-serif;"><br /></div></span>http://nattermorphisms.blogspot.com/2012/06/unfolding-with-view-patterns.htmlnoreply@blogger.com (Ben)3tag:blogger.com,1999:blog-3857512306503018420.post-7286198545609531002Thu, 23 Feb 2012 06:47:00 +00002012-02-23T06:47:46.701+00:00PerspectiveLast night, on the BBC News, I saw the worst thing I ever have.<br /><br />Whilst covering the deaths of Marie Colvin and Remi Ochlik, they showed footage of a two-year-old child dying from injuries sustained in the bombardment of Homs.<br /><br />A child. Two years old.<br /><br />Suddenly my world seemed very different, and much smaller.http://nattermorphisms.blogspot.com/2012/02/perspective.htmlnoreply@blogger.com (Ben)0tag:blogger.com,1999:blog-3857512306503018420.post-1613371941756742937Sun, 18 Jan 2009 15:32:00 +00002009-01-18T21:38:22.242+00:00The Category Theory of AppendagesThere has been much discussion recently on haskell-cafe about Monoids, much (too much!) focusing on the possibility of renaming of the existing monoid typeclass to "Appendable"... which is a daft idea, not least because then we'd need to rename Monad to be "Appendage".<br /><br />Anyway, I wanted to focus a bit on the link between the two concepts (monoid and monad), and how that's treated from the Category Theoretic perspective. (I'm not aiming at any kind of rigour ... simply trying to gain some basic intuitions). In terms of assumptions, I assume familiarity with the definitions of Category, Functor and ideally categorical products / co-products, initiality and finality.<br /><br />This article aims to cover similar ground to one of sigfpe's <a href="http://sigfpe.blogspot.com/2008/11/from-monoids-to-monads.html">here</a>, but at a slightly higher (hopefully simpler) level.<br /><br /><br /><b>Traditional Monoids</b><br /><br />The basic concept of Monoid is treated from the standard mathematical (abstract algebra) perspective <a href="http://en.wikipedia.org/wiki/Monoid">here</a>, and from the practical (Haskell) perspective sigfpe has a nice article <a href="http://sigfpe.blogspot.com/2009/01/haskell-monoids-and-their-uses.html">here</a>.<br /><br />So, from a traditional point of view, a monoid is:<br /><br />* A set, along with...<br />* an associative binary function over that set, accompanied by ...<br />* an identity element<br /><br />The basic (non-category theoretic) view of monoids in Haskell is pretty much the standard one, viewing Haskell types as sets. So in Haskell common examples of monoids are: <tt>(String, (++), [])</tt> and <tt>(Int, (+), 0)</tt> and <tt>(Int, (*), 1)</tt> and <tt>(Bool, (&&), True)</tt> and <tt>(Bool, (||), False)</tt>.<br /><br />In the Haskell setting this means that the function has both arguments and result with the same type - ie the function's type is "a -> a -> a", and the identity element is a distinguished value of type "a". And, of course, it is exactly this which is embodied in the <a href="http://www.haskell.org/ghc/docs/latest/html/libraries/base/Data-Monoid.html">Data.Monoid</a> typeclass.<br /><br />Category takes this standard view of monoids and generalises it somewhat. This generalisation has two parts - not only does it generalise so that we can talk about monoids in different categories, but it also generalises so that we can have multiple ways of identifying monoids <i>within</i> a single category.<br /><br /><br /><b>Categories which can contain Monoids</b><br /><br />From the category theory perspective, a category can only "play host" to monoids under the following conditions:<br /><br />* It must be equipped with a <b>functor</b> over the category which maps any pair of objects to another object, and any pair of arrows to another arrow. (This type of functor is similar to a normal functor apart from operating on pairs - and is known as a Bifunctor). Let us call this functor "<b>B</b>".<br /><br />* It must have a distinguished <b>object</b> (which we'll call "<b>e</b>") which acts as an identity for this functor.<br /><br />This then gives us what is known as a <a href="http://en.wikipedia.org/wiki/Monoidal_category">Monoidal Category</a>. (Note that by making different choices for the (bi)functor and distinguished object we may have several different ways to view an underlying category as monoidal).<br /><br />The simplest example is on Set - we take the standard product as the (bi)functor (which maps any pair of sets to the set which is their product), and a single-element set (ie terminal object) as the distinguished object. <!-- Slightly more generally, any category with products and a terminal object is monoidal using product as the (bi)functor and the terminal object as the distinguished object, and any category with co-products and an initial object is monoidal using co-product as the (bi)functor and the initial object as the distinguished object. --><br /><br />In the context of Haskell, we take as the (bi)functor, the product (bi)functor (which maps any pair of types, say 'a' and 'b', to their product type "(a,b)", and any pair of functions, say 'a->c' and 'b->d' to the function '(a,b)->(c,d)'). As the distinguished object we take "()" - the unit type whose sole value "()" is written syntactically identically to its type.<br /><br /><br /><b>Category Theoretical Monoids</b><br /><br />Once we have those two components, we have a category in which it is possible to identify categorical monoids, but we don't actually have the definition of a categorical monoid itself. A <a href="http://en.wikipedia.org/wiki/Monoid_(category_theory)">monoid within a monoidal category</a> is defined to be:<br /><br />* An object (which we'll call "c")<br />* An arrow from <b>B</b> (c,c) to c.<br />* An arrow from <b>e</b> to c.<br /><br />...such that <a href="http://en.wikipedia.org/wiki/Monoid_(category_theory)">some basic diagrams commute</a>. Now, recall that "<b>B</b>" is the (bi)functor which we selected when creating our monoidal category, so "<b>B</b> (c,c)" is just another object.<br /><br />So, to make this concrete - if we consider Haskell as a monoidal category as above, then we can take "c" to be "String", our first arrow to be "(++) :: (String,String) -> String", and our second arrow to be the function ":: () -> String" which takes "()" as its argument and returns "[]".<br /><br />If we compare this with our first, non-categorical, definition of (String, (++), []) as a monoid above, the parallels are quite clear. The differences are firstly that we now need to pretend that (++) has type "(String,String) -> String" rather than "String -> String -> String", which we can do simply by viewing it as an uncurried function, and secondly that we're representing "[]" by a function rather than a value. This extra baggage only really becomes useful when we look at other categorical monoids (which aren't plain, normal monoids).<br /><br /><br /><b>Monads</b><br /><br />So far, when discussing Haskell, we've implicitly had in mind the category "Hask" which has types as its objects, and Haskell functions between those types as its arrows. What we can now do, is to consider another category which is closely related to "Hask" - namely the category formed by taking as objects all Haskell functors ("Maybe", "[]", etc...) and as arrows all functions from one functor type to another ("listToMaybe :: [a] -> Maybe [a]", "maybeToList :: Maybe a -> [a]", etc...). This is the "endofunctor" category over Hask, and these arrows are natural transformations.<br /><br />Next we're going to go looking for monoids in this "endofunctor" category using our above definitions. We need to keep a slightly clear head at this point, because we need to remember that the objects of this category are functors over another category - hence when we just say "functor" we need to be clear whether we're talking about one of these objects (ie a functor <b>in the underlying category</b>), or about a functor <b>over this category</b>.<br /><br />First we need to choose a (bi)functor <b>over this category</b> - we'll choose composition of functors (so this takes a pair of objects - say "Maybe" and "[]" and maps them to their composition "[Maybe]"). Secondly we need to choose a distinguished object - we'll choose the identity functor "Id".<br /><br />Finally, using our second definition, we can see that a monoid in this category must be an object along with two suitable arrows (ie this will be a functor and two natural transformations in Hask). We can take 'Maybe' as the object, 'join :: Maybe (Maybe a) -> Maybe a' as the first arrow, and 'Just :: a -> Maybe a' as our second arrow.<br /><br />Thus equipped, "Maybe" can be seen as a monoid in the endofunctor category over Hask. And that, of course, is what a monad is - a monad over a category 'C' is a (categorical) monoid in the endofunctor category over 'C'.<br /><br /><br /><b>Back to Set (...and Hask?) </b><br /><br />We can now go back and take another look at the Set category. This time we can look for some monoids which are monoids from the category theoretic perspective, but <b><i>not</i></b> from the traditional perspective.<br /><br />We can do this by viewing Set as a monoidal category using <i>co-product</i> as the (bi)functor (ie disjoint union rather than product) and taking the initial object (the empty set) as the distinguished object. Under this definition, "monoids" would be objects (ie Sets - as before), equipped with (a) a function to the set from the disjoint union of the set with itself, and (b) a function to the set from the empty set - ie the empty function.<br /><br />Now, I have to confess I don't remotely understand the implications of this. I haven't ever seen any reference to what such objects would be called in "Set". In Hask, the coproduct of 'a' and 'b' is 'Either a b', and on functions takes 'a->c' and 'b->d' to 'Either a b -> Either c d'. Also, I'm not sure how much sense it makes to talk about an empty type in Hask, or an empty function in Hask.<br /><br />It seems like there ought to be something useful (back in Haskell land) to drop out of this... I'd be very interested in anyone has any ideas / pointers...http://nattermorphisms.blogspot.com/2009/01/category-theory-of-appendages.htmlnoreply@blogger.com (Ben)48tag:blogger.com,1999:blog-3857512306503018420.post-5728890438230881759Wed, 24 Dec 2008 15:50:00 +00002008-12-24T15:56:00.632+00:00Christmas Profiling TipIf you're profiling some code and you get something like this from <tt>hp2ps</tt> ...<br /><br /><pre><br />c:/ws/fpfdev/depot/QA/EDG/EDG_priv/FPF_Dev.br/src $ hp2ps -c<br />GenBarriers.hp<br />c:\ws\fpfdev\depot\QA\EDG\EDG_priv\FPF_Dev.br\ThirdParty\ghc\ghc-6.10.1\<br />bin\hp2ps.exe: Disaster! (bucket out of range)<br /></pre><br /><br />...then the chances are it's because you have a partially truncated <tt>.hp</tt> file (eg if your program didn't exit cleanly). This is easily fixed, by searching for the last <tt>BEGIN_SAMPLE</tt> line in the file, and deleting everything from there onwards.http://nattermorphisms.blogspot.com/2008/12/christmas-profiling-tip.htmlnoreply@blogger.com (Ben)0tag:blogger.com,1999:blog-3857512306503018420.post-7953418964243514393Sun, 09 Nov 2008 20:15:00 +00002008-11-09T20:33:10.012+00:00Why does Functional Programming matter?Of course we all know <a href="http://www.md.chalmers.se/~rjmh/Papers/whyfp.html">the answer</a>...<div><br /></div><div>...but recently I've been wondering how to explain what I feel is important about FP in a pithy, succinct way. (I've frequently found myself failing to explain it well).</div><div><br /></div><div>I think in the future I'm going to say this:</div><div><br /></div><div><blockquote>"Functional Programming makes programs <span class="Apple-style-span" style="font-style: italic;">easier to understand</span>. And that means they're less likely to go wrong."</blockquote></div><div>For my money this is why functional programming is vitally important - because the biggest problem we have right now isn't concurrency ... it's the fact that we can't even write single-threaded programs that work properly. (Of course "go wrong" is used above in the standard rather than the <a href="http://books.google.com/books?id=ti6zoAC9Ph8C&pg=PA111&lpg=PA111&dq=well+typed+programs+don't+go+wrong&source=web&ots=EzGfuHkYVy&sig=d3wef7W5R22Kz_jna_YFnon1IY8&hl=en&sa=X&oi=book_result&resnum=10&ct=result">Milner</a> sense).</div><div><br /></div><div>One other comment I'd make is that I think the "easier to understand" bit becomes more apparent with bigger programs.</div><div><br /></div><div>I'd be interested in hearing if anyone's got a better way of describing it.</div><div><br /><br /></div>http://nattermorphisms.blogspot.com/2008/11/why-does-functional-programming-matter.htmlnoreply@blogger.com (Ben)2tag:blogger.com,1999:blog-3857512306503018420.post-7668587104450418342Thu, 30 Oct 2008 09:16:00 +00002008-10-30T11:38:29.141+00:002 Minute intro to Associated Types / Type FamiliesType Families are an important recent addition to GHC which have been developed over the past couple of years (and indeed are still being developed). They promise to address some of the same issues addressed by functional dependencies whilst avoiding some of the nastier corner cases and allowing for a more solid theoretical underpinning and implementation.<br /><br />There is a lot of material available on Type Families, in fact it seemed somewhat bewildering to me initially. There doesn't seem to be an "idiot's guide" overview - so that's what this post attempts to do - to provide a just enough background to help you work out which papers etc you want to read next.<br /><br /><div><b>Terminology and Syntax</b></div><br />The thing to note is that there are essentially four different concepts, each of which have a couple of different terms for them:<br /><br /><table border="1"><tr> <td><b>Associated (Data) Type</b> <pre>class ArrayElem e where<br /> data Array e<br /> index :: Array e -> Int -> e<br /><br />instance ArrayElem Int where<br /> data Array Int = IntArray UIntArr<br /> index (IntArray a) i = ...</pre></td></tr><tr><td><span class="Apple-style-span" style="font-weight: bold;">Associated (Type) Synonym </span><span class="Apple-style-span" style=""> <pre>class Collection c where<br /> type Elem c<br /> insert :: Elem c -> c -> c<br /><br />instance Eq e => Collection [e] where<br /> type Elem [e] = e<br /> ...</pre></span></td><tr> <tr><td><span class="Apple-style-span" style="font-weight: bold;">Data (Type) Family</span> <pre>data family Array e<br /><br />data instance Array Int = IntArray UIntArr<br /><br />data instance Array Char = MyCharArray a b </pre></td></tr><tr> <td><span class="Apple-style-span" style="font-weight: bold;">(Type) Synonym Family</span> <pre>type family Elem c<br /><br />type instance Elem [e] = e<br /><br />type instance Elem BitSet = Char</pre></td></tr></table><br /><br /><div><b>Associated or Family?</b></div><br /><br /><div>The first "axis" of categorization is "Associated" vs "Family". The "Associated ..." variants (which were invented first) are those which are declared inside a standard typeclass declaration, the "... Family" variants are stand-alone, top-level, use the "family" keyword and were invented a year or so later. The Family variants (collectively known as Type Families) are strict generalizations of the associated ones, and the associated ones are simple syntactic sugar for the family variants.</div><br /><br /><div><b>Data or Type Synonym?</b></div><br /><br /><div>The other "axis" of categorization is "Data" vs "Type Synonym". This distinction mirrors that of normal Haskell "data" and "type" declarations. The key point is that associated <b>data</b> types and <b>data</b> families let you create a <b><i>bijection</i></b> (ie one-to-one mapping) from source type to destination type. Associated type <b>synonyms</b> and <b>synonym</b> families on the other hand allow you to map two different souce types onto the same destination type. The best reference for more details on the difference is the first part of section 7 of the "Associated Type Synonyms" paper.</div><br /><br /><div><b>Equality Constraints</b><br />The final piece of syntax allows us to assert type-level equalities using the above:<br /><pre><br />sumCollection :: (Collection c, Elem c ~ Int) => c -> Int<br />sumCollection c = sum (toList c)<br /></pre><br />This (as with the other examples) is slightly modified from one of the papers - in this case the "Associated Type Synonyms" paper where the syntax uses "=" rather than the "~" which was ultimately used.<br /></div><br /><br /><div><b>Compatability</b></div><div>Many of the above features are actually available in the GHC 6.8 branch but they are only really supported under 6.10 onwards. (I understand that the main reason the code is in 6.8 at all is to facilitate merging of other, unrelated fixes between those branches). I've had success with both kinds of associated types under 6.8 but ran into problems using equality constraints. </div><div><br /><b>References</b><br /><ul><li><a href="http://www.haskell.org/haskellwiki/GHC/Type_families">http://www.haskell.org/haskellwiki/GHC/Type_families</a><br /></li><li><a href="http://www.cse.unsw.edu.au/~chak/papers/CKPM05.html">Associated Types with Class</a></li><li><a href="http://www.cse.unsw.edu.au/~chak/papers/CKP05.html">Associated Type Synonyms</a></li><li><a href="http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html">System F with Type Equality Coercions</a></li><li><a href="http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html">Type Checking with Open Type Functions</a></li></ul><br /></div>http://nattermorphisms.blogspot.com/2008/10/2-minute-intro-to-associated-types-type.htmlnoreply@blogger.com (Ben)16tag:blogger.com,1999:blog-3857512306503018420.post-6093465227919956076Sun, 03 Aug 2008 20:05:00 +00002008-08-04T21:04:04.559+01:00Join-ing the BlogosphereI'd like to share a little Haskell snippet (I wanted to say "idiom" but actually I'm not sure if I've seen it used anywhere else...) that I quite like:<br /><br /><tt><br />join (,) 9<br /></tt><br /><br />What does this do? On its own, not much - in fact you just get:<br /><br /><tt><br />(9,9)<br /></tt><br /><br />...which you'd have been much better off typing in yourself. Where it can come-in handy though is when writing code in a pointfree style if you have a need to duplicate an anonymous value into both parts of a pair:<br /><br /><tt><br />functionWhichTakesAPair . join (,) . functionWhichProducesASingleValue<br /></tt><br /><br />Anyway, how / why does this construct work....?<br /><br />The <tt>(,)</tt> is just the standard data constructor for a 2-tuple, a pair. (This constructor has type <tt>a -> b -> (a,b)</tt> so you can always write <tt>(,) 9 9</tt> as an alternative notation for <tt>(9,9)</tt> if you wish).<br /><br />The <tt>join</tt> is the standard function <tt>:: Monad m => m (m a) -> m a</tt> we know from monadic programming (Control.Monad). But this just raises the question of how it can make sense to apply it to <tt>(,)</tt> which as we've seen is a function of type <tt>a -> b -> (a,b)</tt>.<br /><br />The answer is of course that this function may be considered to be of type <tt>m (m a)</tt>. This is because <tt>Control.Monad.Instances</tt> declares any partially applied function (eg <tt>a -> ...</tt>) to be a monad (the type <tt>a</tt> can be seen as representing an encapsulated environment which is threaded through by the monadic bind). This then means that a function of two arguments (such as <tt>(,)</tt>) can be seen as having type <tt>m (m a)</tt> which is just what we need to be able to apply <tt>join</tt>. The net result is that the single argument of the resulting function (<tt>join (,)</tt>) is passed in twice as desired.<br /><br />This of course generalises to functions other than <tt>(,)</tt> - whenever we use <tt>join f</tt> where <tt>f</tt> is a function of two arguments, we end up with a function of one argument which is passed into <tt>f</tt> twice.http://nattermorphisms.blogspot.com/2008/08/join-ing-blogosphere.htmlnoreply@blogger.com (Ben)1