tag:blogger.com,1999:blog-36798122088007659692018-03-02T08:57:48.206-08:00monoidalghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.comBlogger12125tag:blogger.com,1999:blog-3679812208800765969.post-29079611359001247672013-01-29T05:02:00.000-08:002013-01-29T05:02:05.688-08:00On safety and abstractionHaskell does not have full-fledged dependent types. For example, there is no way to create naturals as a subset of integers. One way to sidestep this restriction is creating an abstract datatype. Define<br /><pre>newtype Natural = N Integer</pre>and add a collection of methods (addition, printing etc.). Clients can interact with this type only via these methods. They cannot construct a pathological value such as <tt>N (-1)</tt>, which could violate some invariants and crash the program.<br /><br />Furthermore, we can change the implementation later on (for example, to <tt>data Natural = Zero | Succ Natural</tt>) and the clients will not notice, as long as we do not change the protocol.<br /><br />It seems that abstract datatypes give us two things at once: safety from invalid values and modularity. I think this is a bad conflation. These two concerns should be separated.<br /><br /><b>Subsets</b><br /><br />Without support of dependent types we can at least label where they should be. Define<br /><pre>newtype Subset a = Subset a<br /><br />fromSubset :: Subset a -> a<br />fromSubset (Subset a) = a<br /><br />unsafeToSubset :: a -> Subset a<br />unsafeToSubset = Subset</pre>and change the definition of naturals to<br /><pre>newtype Natural = N (Subset Integer)</pre>Here <tt>Subset a</tt> is an unspecified, context-dependent, subset of type <tt>a</tt>.<br /><br />This way safety and modularity is separated. If you match on <tt>N</tt> it means that you break the module abstraction: your code depends on the implementation details. If, furthermore, you use <tt>Subset</tt>, you have to guarantee you're not constructing pathological values.<br /><br />The same thing happens in <a href="http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/safe-haskell.html#id654754">restricted IO from GHC's manual</a>, which can be defined with:<br /><pre>newtype RIO a = RIO (Subset (IO a))</pre><br /><b>Quotients</b><br /><br />In naturals, unconstrained use of constructor <tt>N</tt> might lead to nonsensical objects. Sometimes there's a dual situation: unconstrained use of pattern matching might lead to invalid results.<br />For example, rationals are pairs of integers p/q, but we want 1/2 and 2/4 to be indistinguishable - the "numerator" operation breaks abstraction. In <a href="http://monoidal.blogspot.com/2010/09/algorithms-and-functions.html">this</a> post I talked about this phenomenon with functions represented by algorithms.<br /><pre>newtype Quotient a = Quotient a<br /><br />toQuotient :: a -> Quotient a<br />toQuotient = Quotient<br /><br />unsafeFromQuotient :: Quotient a -> a<br />unsafeFromQuotient (Quotient a) = a</pre>Note that the direction of functions is reversed. Going from an object to quotient is well-defined, but when you go the other way you have to guarantee consistent behavior for equivalent answers.<br /><br />Free groups (see <a href="http://blog.sigfpe.com/2007/06/monads-from-algebra-and-the-gray-code.html">sigfpe's post</a>) can be defined with<br /><tt>newtype FreeGroup x = FreeGroup (Quotient [Either x x])</tt><br />which means that an element of a free group is represented by a list, but with some identifications: <tt>[Right a, Left a]</tt> is equivalent to <tt>[]</tt> since aa<sup>-1</sup>=1.<br /><br />What about rationals? An explicit version of<br /><tt>data Rational = Rational Integer Integer</tt><br />is<br /><tt>data Rational = Rational (Quotient (Integer, Subset Integer))</tt><br /><br />Here there are both mechanisms: equivalent pairs must be equal, and the denominator must be nonzero. Both constructing and deconstructing rationals is unsafe in full generality; the type tells you exactly in what manner.<br /><br /><b>Final thoughts</b><br /><br />In my opinion marking quotients and subsets should become a custom, even in absence of dependent types. It makes things explicit where they should be.<br /><br />If you think those newtypes are littering too much, you can at least make them transparent with<br /><pre>type Subset a = a<br />type Quotient a = a</pre>and let your type definitions speak more.<br /><br />Finally, while both <tt>Subset a</tt> and <tt>Quotient a</tt> are ambiguous (they do not specify the subset or the partition), you can make an indication with a phantom tag:<br /><pre>data NonNegative<br />newtype Subset' p a = Subset' a<br />type Natural = Subset' NonNegative Integer</pre>but handling tags gets troublesome rather fast (there is no automatic way to reason on them).ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com0tag:blogger.com,1999:blog-3679812208800765969.post-26979087712952522412012-09-17T11:07:00.000-07:002012-09-17T11:07:58.639-07:00A kind for regionsWith a new powerful kind system in GHC, there are many lurking opportunities for expressive programming. Here's one.<br /><br />What is the kind of the <a href="http://hackage.haskell.org/packages/archive/base/latest/doc/html/Control-Monad-ST.html">ST</a> type constructor? Currently, it's <tt>ST :: * -> * -> *</tt>.<br /><br />It should not be. In <tt>ST s a</tt>, the parameter <tt>s</tt> is special. It is not meant to be a "real" type like <tt>Int</tt>. It is used only to control the scope of references. One day I'd like to see a separate kind for <tt>s</tt>.<br /><br /><pre>kind Region<br />ST :: Region -> * -> *<br />STRef :: Region -> * -> *<br />runST :: (forall (s :: Region). ST s a) -> a</pre><br />This way it's clear that in <tt>ST s a</tt> the types <tt>s</tt> and <tt>a</tt> are of different nature. Attempting to write <tt>ST s s</tt> is a kind error.ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com0tag:blogger.com,1999:blog-3679812208800765969.post-60152250007221637502012-05-24T16:47:00.000-07:002012-05-27T07:20:45.123-07:00A toy version of Safe HaskellThe idea of Safe Haskell is to control unsafe operations. Here is an alternative idea of implementation. Define a class<br /><br /><pre>> {-# LANGUAGE FlexibleContexts, Rank2Types #-}<br />> class Unsafe a where</pre>The "a" parameter is unneccessary, but it is required by GHC.<br /><br />Add the unsafe constraint to each operation.<br /><br /><pre>> unsafePerformIO :: Unsafe () => IO a -> a<br />> unsafePerformIO = undefined -- implementation skipped<br /><br />> unsafeCoerce :: Unsafe () => a -> b<br />> unsafeCoerce = undefined</pre><br />That's it. You can now code with unsafe functions. The constraint "Unsafe" is contagious: everything that internally uses unsafe* will be tagged. Old code does not have to be changed except type signatures.<br /><br />The compiler only has to prohibit users from defining instance <tt>Unsafe ()</tt>. If you do this, you are releasing the brakes, and back to normal Unsafe Haskell.<br /><br />Safe Haskell has "trustworthy" modules, which can use unsafe features, but their authors claim their interfaces are safe.<br /><br />This idea can be implemented if there was a special function allowed in trustworthy modules removing the constraint:<br /><br /><pre>> unsafe :: forall a. (Unsafe () => a) -> a<br />> unsafe = undefined</pre><br />Of course this falls short of real Safe Haskell, which must forbid Template Haskell, overlapping instances etc. I like the fact that unsafeness of <tt>unsafePerformIO</tt> is expressed in its type.<br /><br /><hr/>I hope this demonstrates zero-parameter type classes might be something reasonable. For now, you can simulate them with <tt>-XConstraintKinds</tt> and <tt>-XDataKinds</tt>:<br /><br /><tt>{-# LANGUAGE ConstraintKinds, KindSignatures, DataKinds #-} <br />class Unsafe' (a :: ()) <br />type Unsafe = Unsafe' '() </tt><br /><br />Edit:<br /><br />I just realized you can have unsafe instances:<br /><br /><pre>instance (Unsafe (), Show a) => Show (IORef a) where <br /> show = show . unsafePerformIO . readIORef</pre>ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com3tag:blogger.com,1999:blog-3679812208800765969.post-65107881707218670892012-04-16T11:10:00.000-07:002012-04-16T11:10:08.924-07:00Descending the level ladderThe following is a way to compute 2+1 using the GHC type system. The ":kind!" command tells GHCi to display normalized version of a type.<br /><pre>{-# LANGUAGE TypeFamilies #-}<br />data Zero<br />data Succ a<br /><br />type family Add x y<br />type instance Add Zero x = x<br />type instance Add (Succ x) y = Succ (Add x y)<br /><br />*Main> :kind! Add (Succ (Succ Zero)) (Succ Zero)<br />Add (Succ (Succ Zero)) (Succ Zero) :: *<br />= Succ (Succ (Succ Zero))</pre><br />Notice we did not use Haskell values anywhere. Not even undefined. This way of computing 2+1 uses types only.<br /><br />Imagine you are a malicious professor teaching Haskell to freshmen. You tell them that this is the normal way to compute 2+1 in Haskell. The students later code Fibonacci, multiplication etc. They get a Turing complete language.<br /><br />They have no idea that Haskell has what we call values. To them, "values" are things like <tt>Succ Zero</tt>, what we call "types". They think Haskell has a type system, that prohibits nonsense such as <tt>Zero (Succ Succ)</tt>. In reality, that type system is kinds.<br /><br />Later, the students discover the truth; their values are really types, and their types are really kinds.<br /><br />In this post I will argue we might live in such shifted world as well. There is a layer below Haskell values.<br /><br />What is it? By Curry-Howard, we can think of values as proofs for types. For example, the identity function is a proof that <tt>p -> p</tt>. Analogously, we can think of "undervalues" as proofs for values. So I will call this level "proofs". We have<br /><blockquote>kinds > types > values > proofs</blockquote>where A>B means that A is a type system for B.<br /><br />One way to see "undervalues" is to check what are values in above scenario. If we add to the initial code the datatype<br /><pre>data Equal a b where<br /> Eq :: Equal a a</pre>then a value of type<br /><pre>com :: forall (m :: *) (n :: *). Equal (Add m n) (Add n m)</pre>could work as a proof that addition is commutative. <br /><br />So, in the shifted scenario, we have a kind <tt>*</tt> (a poor man's Naturals), types <tt>Zero</tt> and <tt>Succ</tt>, and a value of type <tt>Equal (Add m n) (Add n m)</tt>.<br /><br />Shifting down, we have a type <tt>Natural</tt>, values <tt>Zero</tt> and <tt>Succ</tt>, and a proof of value <tt>m + n == n + m</tt>, which cannot be seen in normal Haskell.<br /><br /><pre>data Natural = Zero | Succ Natural <br /><br />add :: Natural -> Natural -> Natural<br />add Zero x = x<br />add (Succ x) y = Succ (add x y)<br /><br />*Main> add (Succ (Succ Zero)) (Succ Zero)<br />Succ (Succ (Succ Zero))<br /><br />-- com :: forall (m :: Natural) (n :: Natural). add m n == add n m<br />-- cannot be written</pre><br /><b>Intuition</b><br />When you write a type T in Haskell, you can check its correctness from <i>above</i>:<br /><br /><blockquote>Is there a K such that type(T)=K?<br />(i.e. Is there a valid kind for T?)</blockquote><br />but you can also check it from <i>below</i>:<br /><br /><blockquote>Is there a V such that type(V)=T?<br />(i.e. Is there a valid value for T? Is T inhabited?)</blockquote><br />Analogously, when you write a value V in Haskell, you can check its correctness from <i>above</i>:<br /><br /><blockquote>Is there a T such that type(V)=T?<br />(i.e. Is there a valid type for V?)</blockquote><br />but you can also check it from <i>below</i>:<br /><br /><blockquote>Is there a P such that type(P)=V?<br />(i.e. Is there a valid proof for V? Is V inhabited?)</blockquote><br />Checking from above corresponds to checking <i>syntax</i>, and checking from below to checking <i>semantics</i>.<br /><br />The type <tt>Equal Int Bool</tt> is not invalid. You can use it in type-level computation. But it is uninhabited, and this is a sign it might not make sense. The same thing happens when you write an instance of <tt>Monoid</tt> which is not a monoid. You used an uninhabited value. Since syntax is OK, you can run your code. But you will run into trouble, since semantics is wrong. There is no proof of your monoid instance, just like there is no value of the type <tt>Equal Int Bool</tt>.<br /><br /><b>Encoding equational reasoning</b><br /><br />A lot of functional literature contains proofs. Here is an example of what I mean - product of two associative operations is associative. Suppose (a,b)+(c,d)=(a+b,c+d). (The + symbol is overloaded and means 3 different things, beware.)<br /><br /><pre>(x + y) + z =<br /> [use x = (fst x, snd x)]<br />((fst x, snd x) + (fst y, snd y)) + (fst z, snd z) =<br /> [Definition of product operation]<br />((fst x + fst y, snd x + snd y) + (fst z, snd z) =<br /> [Definition of product operation]<br />((fst x + fst y) + fst z, (snd x + snd y) + snd z) =<br /> [Associativity of + and +]<br />(fst x + (fst y + fst z), snd x + (snd y + snd z)) =<br /> [Definition of product operation]<br />(fst x, snd x) + (fst y + fst z, snd y + snd z) =<br /> [Definition of product operation]<br />(fst x, snd x) + ((fst y, snd y) + (fst z, snd z)) =<br /> [use (fst x, snd x) = x]<br />x + (y + z)</pre><br />This should remind you of function composition:<br /><pre> f g h<br /> A --> B --> C --> D</pre>but on a lower level: types A,B,C,D become values, and values f,g,h become proofs.<br /><br />It has always bugged me that such proofs are not easily executable in Haskell despite their routine feel.<br /><br />This is because we cannot access the proof level. We can attempt to do so, by shifting everything up. I will adapt the proof and show that the product of two monoids is a monoid.<br /><br />We start by encoding values as types. For simplicity, we will not transfer their types to complicated kinds.<br /><br />The <tt>(:=)</tt> datatype encodes reasoning rules for equality.<br /><br /><pre>{-# LANGUAGE GADTs, KindSignatures, RankNTypes, TypeOperators, TypeFamilies,<br /> ScopedTypeVariables #-}<br />data Fst x<br />data Snd x<br />data ProdOp (f :: * -> * -> *) (g :: * -> * -> *) x y<br /><br />data a := b where <br /> Refl :: a := a<br /> Sym :: a := b -> b := a<br /> Comp :: a := b -> b := c -> a := c<br /> Arg :: a := b -> c := d -> f a c := f b d<br /> PairC :: a := (Fst a, Snd a)<br /> DefProd :: ProdOp f g (a, b) (c, d) := (f a c, g b d)</pre><br />Now, we can write proofs of associativity and left/right identity. The functions <tt>neutrLProd</tt> and <tt>neutrRProd</tt> take proofs that f,g have neutral elements m,n and show that their product has neutral element (m,n). The function <tt>assocProd</tt> does the same with associativity.<br /><pre>type NeutralL (+) e = forall x. e + x := x<br />neutrLProd :: NeutralL m e -> NeutralL n f -> NeutralL (ProdOp m n) (e,f)<br />neutrLProd e1 e2 =<br /> -- (e,f) + x<br /> Arg Refl PairC<br /> `Comp` -- (e,f) + (fst x, snd x)<br /> DefProd<br /> `Comp` -- (e + fst x, f + snd x)<br /> Arg e1 e2<br /> `Comp` -- (fst x, snd x)<br /> Sym PairC<br /> -- x<br /><br />type NeutralR (+) e = forall x. x + e := x<br />neutrRProd :: NeutralR m e -> NeutralR n f -> NeutralR (ProdOp m n) (e,f)<br />neutrRProd e1 e2 =<br /> -- x + (e, f)<br /> Arg PairC Refl<br /> `Comp` -- (fst x, snd x) + (e, f)<br /> DefProd<br /> `Comp` -- (fst x + e, snd x + f)<br /> Arg e1 e2<br /> `Comp` -- (fst x, snd x)<br /> Sym PairC<br /> -- x<br /><br />type Assoc (+) = forall x y z. ((x + y) + z) := (x + (y + z))<br />assocProd :: Assoc f -> Assoc g -> Assoc (ProdOp f g)<br />assocProd a1 a2 =<br /> -- (x + y) + z<br /> Arg (Arg PairC PairC) PairC<br /> `Comp` -- ((fst x, snd x) + (fst y, snd y)) + (fst z, snd z)<br /> Arg DefProd Refl<br /> `Comp` -- (fst x + fst y, snd x + snd y) + (fst z, snd z)<br /> DefProd<br /> `Comp` -- ((fst x + fst y) + fst z, (snd x + snd y) + snd z)<br /> Arg a1 a2<br /> `Comp` -- (fst x + (fst y + fst z), snd x + (snd y + snd z))<br /> Sym DefProd<br /> `Comp` -- (fst x, snd x) + (fst y + fst z, snd y + snd z)<br /> Arg Refl (Sym DefProd)<br /> `Comp` -- (fst x, snd x) + ((fst y, snd y) + (fst z, snd z))<br /> Sym (Arg PairC (Arg PairC PairC))<br /> -- x + (y + z)</pre><br />(Exercise for the reader: Write the proof that product of two commutative operations is commutative.)<br /><br />This is the normal monoid type class in Haskell, with unenforceable laws:<br /><br /><pre>class Monoid m where<br /> (<>) :: m -> m -> m<br /> mempty :: m<br /> -- law (a <> b) <> c == a <> (b <> c)<br /> -- law mempty <> a == a<br /> -- law a <> mempty == a</pre><br />Now we shift everything: types become kinds, values become types, and proofs become values. Since we do not have kind classes yet, we will simulate them with an additional parameter. (We are doing <a href="http://www.haskell.org/haskellwiki/Traits_type_class">this</a> trick, only on kind level.)<br /><br /><pre>data Proxy i = Proxy<br /><br />class Monoid' i where<br /> type Mappend i :: * -> * -> *<br /> type Mempty i :: *<br /> assoc :: Proxy i -> Assoc (Mappend i)<br /> neutrL :: Proxy i -> NeutralL (Mappend i) (Mempty i)<br /> neutrR :: Proxy i -> NeutralR (Mappend i) (Mempty i)<br /><br />instance (Monoid' m, Monoid' n) => Monoid' (m,n) where<br /> type Mappend (m,n) = ProdOp (Mappend m) (Mappend n)<br /> type Mempty (m,n) = (Mempty m, Mempty n)<br /><br /> assoc (Proxy :: Proxy (m,n)) = assocProd (assoc (Proxy :: Proxy m))<br /> (assoc (Proxy :: Proxy n))<br /> neutrL (Proxy :: Proxy (m,n)) = neutrLProd (neutrL (Proxy :: Proxy m))<br /> (neutrL (Proxy :: Proxy n))<br /> neutrR (Proxy :: Proxy (m,n)) = neutrRProd (neutrR (Proxy :: Proxy m))<br /> (neutrR (Proxy :: Proxy n))</pre><br />That Proxy is needed to avoid ambiguity errors in type families. If I could, I would write <tt>assoc :: Assoc (Mappend i), assoc = assocProd assoc assoc</tt>.<br /><br />We can write a monoid and prove it satisfies the monoid laws. If the language had a support for proofs, we could do that on value level as well.<br /><br />In category theory, equations sometimes change to morphisms:<br /><br /><ul><li> A monoid is a type m with a product of type (+) :: m -> m -> m and a proof of value (a + b) + c = a + (b + c),<br />A monoidal category is a kind k with a product of kind (+) :: k -> k -> k and a value of type a + (b + c) -> (a + b) + c [and other things],<br /><li>A monoid homomorphism between monoids m,n is a value of type m -> n with proofs of values f(m)*f(n)=f(m*n) and e=f(e); <br />An applicative functor between monoidal categories m, n is a type f :: m -> n with values of type f m * f n -> f (m * n) and () -> f ().</li><br /></ul>Interestingly, some languages support "universe polymorphism", which allows to unify such declarations.<br/><br/> <strong>Final thoughts</strong><br/> Equational reasoning is a very powerful tool for program transformations. GHC uses them to make strong optimizations. It is also the base of <a href="http://community.haskell.org/~ndm/hlint/">hlint</a>. It can express many folklore ideas - free theorems/parametricity, stream fusion, fold properties etc. I hope some day those things will become an integral part of the language or standard library. When you are adding a rewrite rule to GHC or a suggestion to hlint, you could write a proof that the rewriting is a consequence of laws. When you are writing an instance of a type class, you can prove required laws.<br/><br/> A well-known Haskell saying is that if you think a lot about types, then the values will write themselves. In the same way, if you think a lot about values, their proofs should - in theory - be easy. Perhaps a tool like Djinn could find the proof automatically in limited cases.<br/><br/> Haskellers often write types, and leave values as <tt>undefined</tt>. In the same way, you could write values, and worry about supplying proofs later. So at least in theory, adding proofs should not be a revolution. Currently, whatever you write in Haskell, your code will be full of intangible assumptions and invisible <tt>undefined</tt> proofs!<br/><br/> So there is an invisible world - the world of proofs - hidden below values. Is there an even lower level below proofs? If you take proofs to be objects, then arrows between them could mean their transformations.<br/><br />This is the path taken by dependently typed languages such as Agda. However, as far as I know dependent types are not a requirement for proofs: we have only added an additional layer, we do not allow types to depend on values.ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com2tag:blogger.com,1999:blog-3679812208800765969.post-61979138525703133792011-10-27T11:42:00.000-07:002011-10-27T11:56:34.895-07:00Kind polymorphism - a draftI extended the <a href="http://monoidal.blogspot.com/2010/07/kind-polymorphism-in-action.html">post on kind polymorphism</a> to Omega, and I'm rather satisfied - I captured 10 different senses of monoids, used level polymorphism and type functions on the way.<br /><br /><pre>sumMonoid :: Monoid Hask Int -- monoid<br />maybeMonad :: Monoid EndHask Maybe -- monad<br />envComonad :: Monoid CoEndHask (Env s) -- comonad<br />haskCat :: Monoid Graph (->) -- category<br />ixState :: Monoid Indexed IxState -- indexed monad<br />ixStore :: Monoid CoIndexed IxStore -- indexed comonad<br />intRing :: Monoid Ab Int -- ring<br />sumCMonoid :: Monoid Monoids Int -- commutative monoid<br />complexAlgebra :: Monoid (VSpaces Float) Complex -- R-algebra<br />EndHask'' :: Monoid' Cats (*0 ~> *0) -- monoidal category</pre><br /><br />A draft is available <a href="http://students.mimuw.edu.pl/~kg262935/kpol/Author.pdf">here</a> and Omega source code is available <a href="http://students.mimuw.edu.pl/~kg262935/kpol/prog.hs">here</a>. There are still things that can be improved and researched on.<br /><br />Also, see a new paper on kind system: <a href="http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf">Giving Haskell a Promotion</a>.ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com2tag:blogger.com,1999:blog-3679812208800765969.post-20425455908881584642010-09-01T14:44:00.001-07:002010-09-02T11:04:42.608-07:00Algorithms and functionsConsider the following two functions:<br /><br /><pre>f :: () -> ()<br />f = const ()<br /><br />g :: () -> ()<br />g = id</pre><br /><br />Is there a way to write a function that tells them apart? Given an infinite loop, first will stop and the second will hang. But you can do better, give an exception and check if it was thrown:<br /><br /><pre>data TestException = TestException deriving (Show, Typeable)<br /><br />instance Exception TestException<br /><br />test :: (() -> ()) -> Bool<br />test k = unsafePerformIO $ catch (k (throw TestException) `seq` return True)<br /> (\TestException -> return False)</pre><br /><br />Is this a safe trick?<br /><br />On the one hand, it looks rather innocently: a function is given some box, and if it opens it, it's caught red-handed. Such function would hang given infinite loop. A function that doesn't touch the box, yet finishes, is <span style="font-family:courier new;">const ()</span>. Such 'test' is a nice feature to have.<br /><br />On the other hand, something is wrong, since <span style="font-family:courier new;">f</span> is more defined than <span style="font-family:courier new;">g</span>, and <span style="font-family:courier new;">test f</span> is not at least as defined as <span style="font-family:courier new;">test g</span>. This contradicts monotonicity. By giving two exceptions to (+), you can check which argument is evaluated first:<br /><br /><pre>throw A + throw B</pre><br />That means <span style="font-family:courier new;">flip (+)</span> is not the same as <span style="font-family:courier new;">(+)</span>. Addition is not commutative!<br /><br />Which of these points is correct?<br /><br /><b>The representation of a->b</b><br />Internally, the (->) type is a list of instructions - force a thunk, case, perform a primitive instruction like adding integers. In other words, it's an algorithm. You could conceivably write an algebraic datatype that encompassed all those options.<br /><pre>data Instruction a b = Force Thunk | Return Value...<br />type Algorithm a b = [Instruction a b]</pre><br /><br />Haskell has an evaluator that takes an algorithm and runs it step by step.<br /><pre>($) :: Algorithm a b -> a -> b</pre><br /><br />Having access to internal source code of an algorithm, you can write a "debugger" that stops if the function forces its argument. In a sense, this is what the function <span style="font-family:courier new;">test</span> is doing.<br /><br />Lazy IO uses this trick. When a thunk is forced evaluation is stopped momentarily, and IO is performed.<br /><br />Still, the denotational semantics argument seems disturbing.<br /><br /><b>The distinction</b><br /><br />The solution to the dilemma is:<br /><br />There are two different ways of interpreting values of type a -> b.<ul><br /><br /><li><strong>functions</strong> that assign a value of b to each value of a.</li><br /><li><strong>algorithms</strong> that are recipes how to turn a into b.</li></ul><br /><br />In Haskell, the function view is used, but in this post I'll use both to illustrate differences. I'll call the algorithm view "operational" and function view "denotational".<br /><br />Representing algorithms is possible using ADT, as you seen above. Functions are represented using algorithms:<br /><br /><pre>data Function a b = Function (Algorithm a b)</pre><br /><br />You can turn an algorithm into a function:<br /><br /><pre>evaluate :: Algorithm a b -> Function a b<br />evaluate = Function</pre><br /><br />but the reverse conversion is ill-defined - one function has many representations. <span style="font-family:courier new;">evaluate</span> turns an algorithm into a "black box".<br /><br />Think about rational numbers. You represent them as pairs of integers, even though a rational number is not a pair. Then, you write operations like addition, which don't break 'internal consistency'. Not every operation on pairs can be lifted to operation on rationals. Different pairs may represent same rationals. It's the same with functions stored as algorithms.<br /><br /><b>Questions:</b><br />The questions focus on differences between algorithms and functions.<br /><br />1. Can you compare values of type a -> b for equality?<br /><a href='javascript:toggle("sol1a")'>Answer</a><br /><div id="sol1a" style="display:none">You can compare algorithms, since they are lists of instructions. You cannot in general compare functions because of the halting problem.<br /><br />For example, the following two are different algorithms:<br /><br /><pre>mergesort :: Ord a => [a] -> [a]<br />insertionsort :: Ord a => [a] -> [a]</pre><br /><br />But they are the same functions: <span style="font-family:courier new;">evaluate mergesort</span> is the same as <span style="font-family:courier new;">evaluate insertionsort</span>. In denotational view asymptotic complexity is discounted.<br /><br />In operational view, <span style="font-family:courier new;">\x -> 4</span> and <span style="font-family:courier new;">\x -> 2+2</span> are two different values. Equational reasoning is not allowed, since there's "quoting" after lambda.<br /></div><hr/><br />2. How would you show an algorithm? A function?<br /><a href='javascript:toggle("sol2a")'>Answer</a><br /><div id="sol2a" style="display:none">You can show an algorithm showing its source code. You can show a function by allowing the user to interactively change the argument, and displaying the result in response.<br /></div><hr/><br />3. How would you read an algorithm? A function?<br /><a href='javascript:toggle("sol3a")'>Answer</a><br /><div id="sol3a" style="display:none">To read an algorithm, read its source code. To read a function, the user must act as an oracle, giving the result of the function when asked.<br /></div><hr/><br />4. What abstract models of computation correspond to algorithms and functions?<br /><a href='javascript:toggle("sol4a")'>Answer</a><br /><div id="sol4a" style="display:none">Turing machines and lambda calculus, respectively.<br /></div><hr/><br />5. How does semantic order on values a -> b look like?<br /><a href='javascript:toggle("sol5a")'>Answer</a><br /><div id="sol5a" style="display:none">Denotationally, f>=g means that for all x, f(x)>=g(x).<br /><br />Operationally, algorithms are only "source codes" and are ordered discretely, as integers:<br /><br /><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://4.bp.blogspot.com/_A5ZPqPvNJqM/S-AxN4nKD0I/AAAAAAAAAGs/F8vKNwtSiy4/s1600/7.jpg"><img margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 67px;" src="http://4.bp.blogspot.com/_A5ZPqPvNJqM/S-AxN4nKD0I/AAAAAAAAAGs/F8vKNwtSiy4/s400/7.jpg" border="0" alt="" id="BLOGGER_PHOTO_ID_5467424062232465218" /></a><br /><br />That's why the <span style="font-family:courier new;">test</span> function from beginning is correct from the operational view. It's not true that algorithm <span style="font-family:courier new;">f</span> is more defined than algorithm <span style="font-family:courier new;">g</span>.<br /></div><hr/><br /><br />6. Is the following function<br /><br /><pre>f :: (() -> ()) -> Bool<br />"f g = [return True if evaluation of g () halts within 100 evaluation steps]"</pre><br />well-defined?<br /><br /><a href='javascript:toggle("sol6a")'>Answer</a><br /><div id="sol6a" style="display:none">It is correct if you fix operational semantics and consider the argument to be an algorithm. It falls under "debugging" category. However, since implementations of the same function may run for different amounts of time, it doesn't make sense in denotational view.<br /></div><hr/><br />7. What about this?<br /><br /><pre>lub :: (Bool -> ()) -> ()<br />lub f = [return () if evaluation of f False or f True halts]</pre><br /><br /><a href='javascript:toggle("sol7a")'>Answer</a><br /><div id="sol7a" style="display:none">It makes sense in algorithm view, since you can run f False and f True in parallel, interleaving steps. But as it turns out, this is a rare case where a function makes sense in denotational semantics. See <a href="http://hackage.haskell.org/package/lub">lub</a> package.<br /></div><hr/><br />8. Since a->b in Haskell is seen as function type, not algorithm type, anything dependent of "internals" is ambiguous. How does Haskell deal with it?<br /><br /><a href='javascript:toggle("sol8a")'>Answer</a><br /><div id="sol8a" style="display:none">By using the IO monad.<br /><br />For example, catching exceptions is allowed only in IO, since they can be used to inspect evaluation order. Another example is:<br /><br /><pre>Control.Concurrent.mergeIO :: [a] -> [a] -> IO [a]</pre><br /><br />You can deem lazy I/O as safe, if you take the 'algorithm' view. In the denotational view, <a href="http://www.haskell.org/pipermail/haskell/2009-March/021064.html">lazy IO doesn't make sense</a> unless you consider IO as nondeterministic.<br /><br />In my opinion this is not a good approach, and it might be better if Haskell had separate types for computations and values. (A computation can be thought as an algorithm returning a value. For example, 2+2 and 4 are two different computations.)<br /></div><hr/><br /><br /><b>Summary</b><br />In most languages, 'functions' are algorithms. In Haskell, the emphasis is on functions as in mathematics and referential transparency. <br /><br />Since Haskell is running on a computer, operational semantics (algorithms) describe how things work on the lower level and you can't do away with them. Things like "debugging", "unsafePerformIO", "measuring time/space complexity of a function", "order of evaluation" are relevant to operational semantics and break the abstraction. Things like "referential transparency" or "functional reactive programming" are valid for functions.<br /><br />I think this is what makes Haskell different from imperative languages. FP is about functions, not algorithms. This has advantages, like better support for composability - and disadvantages, like more difficult time/space reasoning.ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com1tag:blogger.com,1999:blog-3679812208800765969.post-50391475343617932992010-07-29T08:51:00.001-07:002010-07-29T10:40:34.609-07:00The universal spaceTake (or imagine) a blank sheet of paper. This is a plane. You can put points and vectors on it. A vector connects two points, but it is "movable": if you can translate one vector into another, they are deemed equal. A vector doesn't really have a beginning - you can position it wherever you want.<br /><br />In this setting, some operations make sense, like<br /><br /><ul><li>vector + point = point:<br />Position the vector at a point, and its end will be the result.</li><br /><li>point - point = vector:<br />Join the points to get a vector from A to B. (It's inverse of vector + point = point.)</li><br /><li>vector + vector = vector:<br />Put the beginning of one vector to the end of the second.</li></ul><br /><br />But some don't, like adding two points, or subtracting vector - point. With added origin, you can do anything using coordinates, as in (2,1) + (3,0) = (5,1). In fact, with given origin you can consider every point as a vector from the origin. But without it, it's like physical motion - you cannot tell if something is moving without a frame of reference.<br /><br />Although addition point + point doesn't make sense, (point + point) / 2 should - it's middle between the points. 0.2 point + 0.8 point is somewhere in the 4/5 of the segment. This is known as "affine combination".<br /><br />An expression like vector + point - point can be computed in two different ways: (vector + point) - point and vector + (point - point) and it turns out the result will be the same. There must be some structure here.<br /><br />Define mass of a vector as 0, and mass of point as 1. Then,<br /><br /><ul><li>vector + point = point: 0 + 1 = 1</li><br /><li>point - point = vector: 1 - 1 = 0</li><br /><li>vector + vector = vector: 0 + 0 = 0</li><br /><li>(point + point) / 2 = point: (1+1) / 2 = 1</li></ul><br /><br />In fact you can enlarge the space. Define an object to be either a vector with mass 0, or a pair (p,m) which is a point p with a nonzero mass m. I'll write a point as m*p. Then multiplication streches a vector, or changes a point's mass: a*(m*p) = (a*m)*p. Addition is done with:<br /><br /><div class="latex">m p + v = m (p + \frac{v}{m})</div> - translation<br /><br /><div class="latex">m_{1}p_{1} + m_{2}p_{2} = (m_{1}+m_{2}) (\frac{m_{1}}{m_{1}+m_{2}} p_{1} + \frac{m_{2}}{m_{1}+m_{2}} p_{2})</div> - weighted mean of points<br /><br /><div class="latex">m_{1}p_{1} - m_{1} p_{2} = m_{1} (p_{1} - p_2})</div> - a vector joining two points<br /><br />In this space, points and vectors are equal partners, and anything can be added and multiplied by a number. It's a vector space with dimension one more than the original.<br /><br />In the original space, you assign a meaning to a sum like 0.2a + 0.8b, but not to the summands. In this space, summands make sense and 0.2a + 0.8b is really a sum of 0.2a and 0.8b.<br /><br />In mathematical terms, this is an assignment of a vector space to every affine space. This construction is known as the universal space. Now, vector spaces and affine spaces have their own meaning of functions. A linear map respects linear combinations: f(cx+dy) = c f(x)+d f(y). An affine map is something that respects affine combinations: f(cx+dy) = cf(x)+ df(y), where c+d=1. It's easy to present a linear map using a matrix. How to present an affine map? The answer is, given affine map, you can extend it to a linear map between universal spaces by f(m*p)=m*f(p) for all m. And that <a href="http://en.wikipedia.org/wiki/Affine_map#Representation">gives</a> a matrix. <br /><br />For category theory lovers, this construction is the left adjoint of a functor that assigns an affine space to a vector space by forgetting the origin.ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com2tag:blogger.com,1999:blog-3679812208800765969.post-34465039159467542352010-07-26T16:49:00.000-07:002010-07-28T11:31:13.795-07:00Kind polymorphism in action<a href="http://www.cs.uu.nl/wiki/UHC">Ultrecht Haskell Compiler</a> is an experimental Haskell compiler that supports polymorphism on the kind level. This means that in<br /><pre>data Eq a b = Eq (forall f. f a -> f b)</pre><br />Eq is given kind<br /><pre>Eq :: forall a . a -> a -> *</pre><br /><br />and both Eq Integer Char and Eq [] Maybe are valid types.<br /><br />Using kind polymorphism, it is possible to write sigfpe's <a href="http://blog.sigfpe.com/2008/11/from-monoids-to-monads.html">From monoids to monads</a> using a single type class.<br /><br />To talk about monoids, you need a category (mor), multiplication (mul) and a unit.<br /><br /><pre>class Monoid mor mul unit m where<br /> one :: mor unit m<br /> mult :: mor (mul m m) m<br /></pre><br /><br />With mor being (->), mul being (,), unit being () this is a normal monoid (one :: () -> m and mult :: (m,m) -> m.). For example:<br /><br /><pre>instance Monoid (->) (,) () Integer where<br /> one () = 1<br /> mult = uncurry (*)<br /></pre><br /><br />Now, instead of functions, there will be natural transformations; instead of (,) there will be functor composition; instead of unit there will be identity functor.<br /><br /><pre>data Nat f g = Nat (forall x. f x -> g x)<br />data Comp f g x = Comp (f (g x))<br />data Id x = Id x<br />Nat :: (* -> *) -> (* -> *) -> *<br />Comp :: (* -> *) -> (* -> *) -> * -> *<br />Id :: * -> *<br /></pre><br /><br />And here is the list monad. Notice kinds are different than in the previous case, but it is still an instance of the same type class.<br /><br /><pre>instance Monoid Nat Comp Id [] where<br /> one = Nat $ \(Id x) -> [x] -- one :: Nat Id []<br /> mult = Nat $ \(Comp x) -> concat x -- mult :: Nat (Comp [] []) []<br /></pre><br /><br />So, monads are really monoids in category of endofunctors.<br /><br />If you invert the arrows, you get a comonad. Here's the product comonad.<br /><br /><pre><br />data CoNat f g = CoNat (forall x. g x -> f x)<br />data CoComp f g x = CoComp (g (f x))<br />CoNat :: (* -> *) -> (* -> *) -> *<br />CoComp :: (* -> *) -> (* -> *) -> * -> *<br /><br />data Product w a = Product w a<br /><br />instance Monoid CoNat CoComp Id (Product w) where<br /> one = CoNat $ \(Product a b) -> Id b<br /> mult = CoNat $ \(Product a b) -> CoComp $ Product a (Product a b)<br /></pre><br /><br />Question: what are kinds of mor, mul, unit and m in the Monoid type class definition?<br /><br />There's a small lie here: monads require also a liftM/fmap function. Not all Haskell types of * -> * are functors, and I used that as a poor replacement.<br /><br />I didn't write monoid laws, which if translated happen to be monad laws. You're welcome to read sigfpe's original post. It's hard to write them generically since there's no access to fmap.<br /><br />The code is available on <a href="http://hpaste.org/fastcgi/hpaste.fcgi/view?id=28248">hpaste</a> and can be run in UHC.ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com4tag:blogger.com,1999:blog-3679812208800765969.post-62687591699472566842010-05-04T08:04:00.001-07:002010-05-07T13:34:32.905-07:00Denotational semanticsYou're given diagrams of some Haskell types ordered by semantic order. Vertices are inhabitants of a datatype, and the lines point upwards, from less defined to more defined. (See <a href="http://en.wikibooks.org/wiki/Haskell/Denotational_semantics">Wikibooks</a> for an introduction and examples.) Your objective is to construct a type corresponding to the diagram, or show that is impossible.<br /><br /><br />I've done the first one - it is obviously Bool. Good luck!<br /><br /><table border="1"><tbody><tr><td>Diagram</td><td>Type</td></tr><tr><td><br /><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://4.bp.blogspot.com/_A5ZPqPvNJqM/S-AwIinHU6I/AAAAAAAAAF8/pxSRzhdp6Y0/s1600/1.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 67px;" src="http://4.bp.blogspot.com/_A5ZPqPvNJqM/S-AwIinHU6I/AAAAAAAAAF8/pxSRzhdp6Y0/s400/1.jpg" border="0" alt="" id="BLOGGER_PHOTO_ID_5467422870915732386" /></a><br /></td><td><pre>Bool</pre></td></tr><tr><td><br /><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://1.bp.blogspot.com/_A5ZPqPvNJqM/S-AwIxJnWfI/AAAAAAAAAGE/24KlQV2z0EY/s1600/2.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 112px;" src="http://1.bp.blogspot.com/_A5ZPqPvNJqM/S-AwIxJnWfI/AAAAAAAAAGE/24KlQV2z0EY/s400/2.jpg" border="0" alt="" id="BLOGGER_PHOTO_ID_5467422874818533874" /></a><br /></td><td><br /><a href='javascript:toggle("sol2")'>Solution</a><br /><div id="sol2" style="display:none"><br /><pre>data Three = X | Y | Z<br />data Four = A | B | C | D<br />data T = P | Q Three | R Four</pre><br />Using this method you can define any finite tree.<br /><br /><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R2JxY8duI/AAAAAAAAAIQ/bYeR2ZxLev4/s1600/2desc.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 243px; height: 172px;" src="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R2JxY8duI/AAAAAAAAAIQ/bYeR2ZxLev4/s400/2desc.jpg" border="0" alt=""id="BLOGGER_PHOTO_ID_5468625757783488226" /></a><br /></div><br /></td></tr><tr><td><br /><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R2KGT7ZhI/AAAAAAAAAIY/NUfseSTyXrw/s1600/3.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 125px;" src="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R2KGT7ZhI/AAAAAAAAAIY/NUfseSTyXrw/s400/3.jpg" border="0" alt=""id="BLOGGER_PHOTO_ID_5468625763399591442" /></a><br /></td><td><br /><a href='javascript:toggle("sol3")'>Solution</a><br /><div id="sol3" style="display:none"><br /><pre>data NaturalsUp = S NaturalsUp</pre><br /><br /><br /><br /><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://3.bp.blogspot.com/_A5ZPqPvNJqM/S-R2KXl7pXI/AAAAAAAAAIg/zdMNSV_aAoc/s1600/3desc.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 125px;" src="http://3.bp.blogspot.com/_A5ZPqPvNJqM/S-R2KXl7pXI/AAAAAAAAAIg/zdMNSV_aAoc/s400/3desc.jpg" border="0" alt=""id="BLOGGER_PHOTO_ID_5468625768038507890" /></a><br /></div><br /></td></tr><tr><td><br /><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R2KRlq5pI/AAAAAAAAAIo/ZPXj_fLJTxg/s1600/4.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 94px;" src="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R2KRlq5pI/AAAAAAAAAIo/ZPXj_fLJTxg/s400/4.jpg" border="0" alt=""id="BLOGGER_PHOTO_ID_5468625766426797714" /></a><br /></td><td><br /><a href='javascript:toggle("sol4")'>Solution</a><br /><div id="sol4" style="display:none"><br />Impossible. There is no bottom element.</div></td></tr><tr><td><br /><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://1.bp.blogspot.com/_A5ZPqPvNJqM/S-R2K-VDc5I/AAAAAAAAAIw/OCC5dqkBhGw/s1600/5.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 146px;" src="http://1.bp.blogspot.com/_A5ZPqPvNJqM/S-R2K-VDc5I/AAAAAAAAAIw/OCC5dqkBhGw/s400/5.jpg" border="0" alt=""id="BLOGGER_PHOTO_ID_5468625778436699026" /></a><br /></td><td><br /><a href='javascript:toggle("sol5")'>Solution</a><br /><div id="sol5" style="display:none"><br /><pre>type NaturalsDown = NaturalsUp -> ()</pre><br /><br /><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R3lIXD2UI/AAAAAAAAAJI/C39GGMwfXQs/s1600/5desc.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 146px;" src="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R3lIXD2UI/AAAAAAAAAJI/C39GGMwfXQs/s400/5desc.jpg" border="0" alt=""id="BLOGGER_PHOTO_ID_5468627327317694786" /></a><br /></div></td></tr><tr><td><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R3k7xgXLI/AAAAAAAAAJA/3fCOFzru_v8/s1600/6.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 166px;" src="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R3k7xgXLI/AAAAAAAAAJA/3fCOFzru_v8/s400/6.jpg" border="0" alt=""id="BLOGGER_PHOTO_ID_5468627323938954418" /></a></td><td><br /><a href='javascript:toggle("sol6")'>Solution</a><br /><div id="sol6" style="display:none"><br /><pre><br />data Wrap = Wrap k<br />type T = Wrap (Wrap (Maybe NaturalsUp)<br /></pre><br /></div></td></tr><tr><td><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://4.bp.blogspot.com/_A5ZPqPvNJqM/S-AxN4nKD0I/AAAAAAAAAGs/F8vKNwtSiy4/s1600/7.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 67px;" src="http://4.bp.blogspot.com/_A5ZPqPvNJqM/S-AxN4nKD0I/AAAAAAAAAGs/F8vKNwtSiy4/s400/7.jpg" border="0" alt="" id="BLOGGER_PHOTO_ID_5467424062232465218" /></a></td><td><br /><a href='javascript:toggle("sol7")'>Solution</a><br /><div id="sol7" style="display:none"><br /><pre>Integer</pre><br /></div><br /></td></tr><tr><td><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://3.bp.blogspot.com/_A5ZPqPvNJqM/S-AxOEGM8PI/AAAAAAAAAG0/9vccg9K4xMM/s1600/8.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 156px;" src="http://3.bp.blogspot.com/_A5ZPqPvNJqM/S-AxOEGM8PI/AAAAAAAAAG0/9vccg9K4xMM/s400/8.jpg" border="0" alt="" id="BLOGGER_PHOTO_ID_5467424065315467506" /></a></td><td><br /><a href='javascript:toggle("sol8")'>Solution</a><br /><div id="sol8" style="display:none"><br /><pre>((),())</pre><br /></div><br /></td></tr><tr><td><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-AxOSDubiI/AAAAAAAAAG8/98HGUYX7x1E/s1600/9.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 155px;" src="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-AxOSDubiI/AAAAAAAAAG8/98HGUYX7x1E/s400/9.jpg" border="0" alt="" id="BLOGGER_PHOTO_ID_5467424069063175714" /></a></td><td><br /><a href='javascript:toggle("sol9")'>Solution</a><br /><div id="sol9" style="display:none"><br /><pre>data T = L T | R T</pre><br /></div><br /></td></tr><tr><td><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://1.bp.blogspot.com/_A5ZPqPvNJqM/S-AxOongtJI/AAAAAAAAAHE/L1iIu9HctA0/s1600/10.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 155px;" src="http://1.bp.blogspot.com/_A5ZPqPvNJqM/S-AxOongtJI/AAAAAAAAAHE/L1iIu9HctA0/s400/10.jpg" border="0" alt="" id="BLOGGER_PHOTO_ID_5467424075118851218" /></a></td><td><br /><a href='javascript:toggle("sol10")'>Solution</a><br /><div id="sol10" style="display:none"><br />Impossible. The type must form a complete partial order - you could carry the computation indefinitely long, and get the infinite path.</div></td></tr><tr><td><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R3lX2GS0I/AAAAAAAAAJQ/37ZOCoeoo2w/s1600/11.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 154px;" src="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-R3lX2GS0I/AAAAAAAAAJQ/37ZOCoeoo2w/s400/11.jpg" border="0" alt=""id="BLOGGER_PHOTO_ID_5468627331474410306" /></a></td><td><br /><a href='javascript:toggle("sol11")'>Solution</a><br /><div id="sol11" style="display:none"><br /><pre>data T1 = A T2 | B T2<br />data T2 = C T1 | D T1 | E T1</pre></div></td></tr><tr><td><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-Axz2WsYUI/AAAAAAAAAHU/AAMctstNorc/s1600/12.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 32px;" src="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-Axz2WsYUI/AAAAAAAAAHU/AAMctstNorc/s400/12.jpg" border="0" alt="" id="BLOGGER_PHOTO_ID_5467424714461569346" /></a></td><td><br /><a href='javascript:toggle("sol12")'>Solution</a><br /><div id="sol12" style="display:none"><br /><pre>data Void</pre><br />An empty data type has no inhabitants other than bottom. It is used in <a href="http://www.haskell.org/haskellwiki/Phantom_type">phantom types.</a><br /></div></td></tr><tr><td><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://3.bp.blogspot.com/_A5ZPqPvNJqM/S-Ax0GHEIqI/AAAAAAAAAHc/L6o4S4cAm1w/s1600/13.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 160px;" src="http://3.bp.blogspot.com/_A5ZPqPvNJqM/S-Ax0GHEIqI/AAAAAAAAAHc/L6o4S4cAm1w/s400/13.jpg" border="0" alt="" id="BLOGGER_PHOTO_ID_5467424718690984610" /></a></td><td><br /><a href='javascript:toggle("sol13")'>Solution</a><br /><div id="sol13" style="display:none"><br /><pre>data Void<br />data B k = B k deriving (Show)<br />data T x = P x | A !(T (B x)) deriving (Show)<br />type X = T Void</pre><br /><br />The tree looks like:<br /><br /><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-Ax0rrRr_I/AAAAAAAAAHk/n4JOuRP3D28/s1600/13a.jpg"><img style="display:block; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 311px; height: 186px;" src="http://2.bp.blogspot.com/_A5ZPqPvNJqM/S-Ax0rrRr_I/AAAAAAAAAHk/n4JOuRP3D28/s400/13a.jpg" border="0" alt="" id="BLOGGER_PHOTO_ID_5467424728774979570" /></a><br /><br />The type system is quite expressive - for example, the depths could form only perfect squares.</div><br /></td></tr><tr><td><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://1.bp.blogspot.com/_A5ZPqPvNJqM/S-R3lnOgITI/AAAAAAAAAJY/qh1Qd_QZjAk/s1600/14.jpg"><img style="float:left; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 150px; height: 125px;" src="http://1.bp.blogspot.com/_A5ZPqPvNJqM/S-R3lnOgITI/AAAAAAAAAJY/qh1Qd_QZjAk/s400/14.jpg" border="0" alt=""id="BLOGGER_PHOTO_ID_5468627335603298610" /></a></td><td><br />This is a variant of NaturalsDown and will require cheating a little. Create a module that will export a data type, and only a "<a href="http://www.haskell.org/haskellwiki/Smart_constructors">smart constructor</a>" that will equate undefined and const undefined.<br /><br /><a href='javascript:toggle("sol14")'>Solution</a><br /><div id="sol14" style="display:none"><br /><pre><br />module M (Fun, Nat(..), create) where<br /><br />data Nat = Zero | S Nat<br />newtype Fun = Fun (Nat -> ())<br /><br />infinity = S infinity<br />create :: (Nat -> ()) -> Fun<br />create f = seq (f infinity) (Fun f)<br /></pre> Outside the module, you cannot create Fun (const undefined).</div><br /></td></tr></tbody></table><br /><br /><strong>Application</strong><br /><br />A great application of denotational semantics is doing <a href="http://conal.net/blog/posts/exact-numeric-integration/">numerical integration</a> exactly.ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com2tag:blogger.com,1999:blog-3679812208800765969.post-858068456589441282010-04-26T06:39:00.001-07:002010-04-27T03:57:20.696-07:00Conjugating verbs in Haskell<pre><br />> {-# LANGUAGE RecordWildCards #-}<br />> import Data.Maybe<br />> import Data.Default<br />> import Control.Monad.Writer hiding (First)<br /></pre><br />I'll show you an English verb conjugator. Although handling inflections is complex, the structure of the language can be expressed idiomatically, using a monad. You'll see that things like "perfect continuous" are really "perfect" on top of "continuous", in code.<br /><br />First, some boring code and auxiliary functions.<br /><pre><br />> data Tense = Past | Present | Future<br />> type Infinitive = String<br />> data Person = First | Second | Third<br />> -- plural in English is the same form as second person<br /><br />> pastForms inf = fromMaybe (inf++"ed", inf++"ed") $<br />> lookup inf [("do", ("did", "done")),<br />> ("have", ("had", "had")),<br />> ("be", ("was", "been")),<br />> ("drive", ("drove", "driven")),<br />> ("build", ("built", "built"))]<br /><br />> presentParticiple inf | last inf == 'e' && inf /= "be" = init inf ++ "ing"<br />> | otherwise = inf ++ "ing"<br /><br />> pastParticiple inf = snd $ pastForms inf<br /><br />> conjugate1 :: Tense -> Person -> Infinitive -> String<br />> conjugate1 Future p inf = "will " ++ inf<br />> conjugate1 t p "be" = case (t, p) of<br />> (Present, First) -> "am"<br />> (Present, Second) -> "are"<br />> (Present, Third) -> "is"<br />> (Past, Second) -> "were"<br />> (Past, _) -> "was"<br /><br />> conjugate1 Past p inf = fst $ pastForms inf<br />> conjugate1 Present Third "have" = "has"<br />> conjugate1 Present Third "do" = "does"<br />> conjugate1 Present Third inf = inf ++ "s"<br />> conjugate1 Present _ inf = inf<br /></pre><br />We can conjugate verbs in three tenses, and form participles. For example:<br /><pre><br />> test1 = conjugate1 Future First "drive"<br />> test2 = conjugate1 Present Third "phone"<br />> test3 = presentParticiple "have"<br /></pre><br /><strong>Adding "perfect"</strong><br />Now the fun begins.<br /><br />Exercise: Allow forming perfect tenses:<br /><pre><br />> conjugate2 :: Bool -> Tense -> Person -> Infinitive -> String<br /></pre><br />(For example, conjugate2 True Present Third "drive" should be "has driven")<br /><br /><br /><br />Solution:<br /><br />Perfect is "have" + past participle. You can express this directly:<br /><pre><br />> conjugate2 False tense person inf = conjugate1 tense person inf<br />> conjugate2 True tense person inf = conjugate1 tense person "have" ++ " " ++ pastParticiple inf<br /></pre><br /><br /><strong>Adding "continuous"</strong><br />It will be downhill now.<br /><br />Exercise: Allow forming continuous tenses:<br /><pre><br />> conjugate3 :: Bool -> Bool -> Tense -> Person -> Infinitive -> String<br /></pre><br /><br />where the first parameter will be continuous or not. For example, conjugate3 True False Present Third "drive" should be "is driving".<br /><br /><br /><br />Solution:<br /><br />It's be + present participle.<br /><pre><br />> conjugate3 False perf tense person inf = conjugate2 perf tense person inf<br />> conjugate3 True perf tense person inf = conjugate2 perf tense person "be" ++ " " ++ presentParticiple inf<br /></pre><br /><br />This composes nicely:<br /><pre><br />> test4 = "he " ++ conjugate3 True True Present Third "drive"<br /></pre><br /><strong>Adding passive voice</strong><br />Exercise: Allow forming passive voice:<br /><br /><pre><br />> conjugate4 :: Bool -> Bool -> Bool -> Tense -> Person -> Infinitive -> String<br /><br />> test5 = "the house " ++ conjugate4 True True False Present Third "build"<br /></pre><br /><br /><br /><br />Solution:<br /><pre><br />> conjugate4 False cont perf tense person inf = conjugate3 cont perf tense person inf<br />> conjugate4 True cont perf tense person inf = conjugate3 cont perf tense person "be" ++ " " ++ pastParticiple inf<br /><br /></pre><br /><strong>Merging</strong><br />conjugate2, conjugate3 and conjugate4 can be joined into a single function. <br />Remembering all arguments in order and specifying them every time is problematic. This is described in Brent Yorgey's <a href="http://byorgey.wordpress.com/2010/04/03/">Haskell anti-pattern - incremental ad-hoc parameter abstraction</a>. Also there's a lot of repetition.<br /><br /><pre><br />> conjugate5 :: Bool -> Bool -> Bool -> Tense -> Person -> Infinitive -> String<br />> conjugate5 True continuous perfect tense person inf =<br />> conjugate5 False continuous perfect tense person "be" ++ " " ++ pastParticiple inf<br />> conjugate5 _ True perfect tense person inf =<br />> conjugate5 False False perfect tense person "be" ++ " " ++ presentParticiple inf<br />> conjugate5 _ _ True tense person inf =<br />> conjugate5 False False False tense person "have" ++ " " ++ pastParticiple inf<br />> conjugate5 _ _ _ tense person inf = conjugate1 tense person inf<br /></pre><br /><br /><strong>Using records</strong><br /><br /><pre><br />> data ConjugateOptions = ConjugateOptions { passive :: Bool,<br />> perfect :: Bool,<br />> continuous :: Bool,<br />> person :: Person,<br />> tense :: Tense }<br /><br />> instance Default ConjugateOptions where<br />> def = ConjugateOptions False False False First Present<br /><br />> conjugate6 :: ConjugateOptions -> Infinitive -> String<br />> conjugate6 (o@ConjugateOptions{ .. }) inf<br />> | passive = conjugate6 o { passive = False } "be" ++ " " ++ pastParticiple inf<br />> | continuous = conjugate6 o { continuous = False } "be" ++ " " ++ presentParticiple inf<br />> | perfect = conjugate6 o { perfect = False } "have" ++ " " ++ pastParticiple inf<br />> | otherwise = conjugate1 tense person inf<br /></pre><br />Much better - we can use it like<br /><br /><pre><br />> test6 = conjugate6 def { perfect=True } "paint"<br /></pre><br /><br /><strong>Using the Writer monad</strong><br />conjugate6 is doing recursion on some infinitive and adds "remaining part" to the end. The Writer monad can express this.<br /><br /><pre><br />> plumb :: Infinitive -> (Infinitive -> String) -> Infinitive -> Writer [String] Infinitive<br />> plumb aux participle inf = Writer (aux, [participle inf])<br /><br />> passive' = plumb "be" pastParticiple<br />> continuous' = plumb "be" presentParticiple<br />> perfect' = plumb "have" pastParticiple<br /><br />> conjugate7 :: Tense -> Person -> (Infinitive -> Writer [String] Infinitive) -> Infinitive -> String<br /><br />> conjugate7 tense person tr inf =<br />> let (a,b) = runWriter (tr inf)<br />> in unwords $ (conjugate1 tense person a):(reverse b)<br /></pre><br /><br />You can join those different "higher order verbs" using >=>.<br /><br /><pre><br />> test7 = "he " ++ conjugate7 Past Third (continuous' >=> perfect') "paint"<br /></pre><br /><br />and add new new ones instantly:<br /><pre><br />> learn = plumb "learn" ("to "++)<br /><br />> test8 = "I " ++ conjugate7 Present First (learn >=> perfect') "love" ++ " Haskell"<br /></pre><br />Obviously there is a lot missing - inflections ("he go<strong>e</strong>s", "he panic<strong>k</strong>s"), irregular verbs, modal verbs, negation, "used to", "have something done", interrogative mood... It gets dirty then.<br /><br />You can write such conjugator in similar languages, like German.<br /><br />Haskell is a great language - imagine how would you write conjugate1 without pattern matching, or writing the plumbing in conjugate5 again, when Writer can do that for you.ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com0tag:blogger.com,1999:blog-3679812208800765969.post-76147873339816097012009-09-12T15:11:00.000-07:002010-07-29T10:06:01.000-07:00Balanced brackets, finite sets and ordinal numbers<pre><br />import Data.List<br />import Data.Set as Set<br />import Data.MultiSet as MultiSet -- not required<br /></pre><br /><br /><b>Balanced brackets</b><br /><br />The <a href="http://en.wikipedia.org/wiki/Dyck%20language">Dyck language</a> is the set of correctly parenthesised strings, like "(()(()()))".<br /><br /><pre><br />data Dyck = Dyck [Dyck]<br /></pre><br /><br />If you disregard the type constructor, an inhabitant looks like [[], [[], []]]. This type represents rooted trees. A rooted tree is a list of rooted trees. To convert a list of rooted trees to a rooted tree, you add the root. To convert back, you remove it.<br /><br /><a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://4.bp.blogspot.com/_A5ZPqPvNJqM/SqFUpaVv7rI/AAAAAAAAABg/t8vYDUxIYnY/s1600-h/vvv.GIF"><img style="display:block; margin:0 10px 10px 0;cursor:pointer; cursor:hand;width: 320px; height: 100px;" src="http://4.bp.blogspot.com/_A5ZPqPvNJqM/SqFUpaVv7rI/AAAAAAAAABg/t8vYDUxIYnY/s400/vvv.GIF" border="0" alt=""id="BLOGGER_PHOTO_ID_5377672500478996146" /></a><br /><br />Traversing the tree gives us the string:<br /><br /><pre>string (Dyck x) = "(" ++ concatMap string x ++ ")"</pre><br /><br />To be honest, we're missing strings like ()() and the real Dyck type is [Dyck]. But it isn't important since these types are isomorphic as the picture above shows.<br /><br /><b>Hereditarily finite sets</b><br /><br />If we use sets instead of lists, then we get <a href="http://en.wikipedia.org/wiki/Hereditarily_finite_set">hereditarily finite sets</a>.<br /><br /><pre><br />data HFS = HFS (Set HFS)<br /><br />instance Eq HFS where<br /> (==) (HFS x) (HFS y) = x == y<br /><br />instance Ord HFS where<br /> compare (HFS x) (HFS y) = compare x y<br /></pre><br /><br />I was a bit surprised this works - to talk about Set HFS you have to implement comparision for HFS (since sets in Data.Set are binary search trees inside), but to implement comparision for HFS you have to define HFS first. Mutual recursion.<br /><br />Here are <span class="latex">A=\{\emptyset\}</span> and <span class="latex">B=\{\emptyset, \{\emptyset\}\}</span>.<br /><br /><pre>hfs = HFS . Set.fromList<br /><br />setA = hfs [hfs []]<br />setB = hfs [hfs [], setA]<br /><br />-- Every natural number can be written in binary:<br />data Binary = Natural -> Bool<br />-- We can write the exponents in binary too:<br />data Binary = Binary -> Bool<br />-- And, since a function into Bool represents some set,<br />data Binary = Set Binary</pre><br /><br />This is the same as the equation for HFS. To convert, recursively change a number to the set of exponents: 15 = {0,1,2,3} = {{},{0},{1},{0,1}} = {{}, {{}}, {{0}}, {{},{0}}} = {{}, {{}}, {{{}}}, {{},{{}}}}. It turns out there's a <a href="http://logic.cse.unt.edu/tarau/research/2008/fSET.pdf">paper</a> on this subject.<br /><br /><b>Ordinal numbers</b><br /><br />Here's another example. If you don't know <a href="http://en.wikipedia.org/wiki/Ordinal_number">ordinal numbers</a> skip this paragraph. I'll talk only about ordinals lesser than <span class="latex">\epsilon_{0}</span>. They can be written in the form<br /><br /><span class="latex">\omega^{a_1}+\dots+\omega^{a_n}</span><br /><br />where <span class="latex">a_i</span> is a nonincreasing sequence of ordinal numbers. These <span class="latex">a_i</span> may be written recursively in that form too, and this recursion will always stop at some point. You can put coefficients after each <span class="latex">\omega^{a_i}</span> and require that the sequence is decreasing. This looks very similar to previous examples.<br /><br /><pre><br />data ON = ON (MultiSet ON) -- (small) ordinal<br /><br />instance Eq ON where<br /> (==) (ON x) (ON y) = x == y<br /><br />instance Ord ON where<br /> compare (ON x) (ON y) = compare x y<br /><br />on = ON . MultiSet.fromList<br /></pre><br /><br />If you don't have multisets installed (cabal install multiset), you may use lists instead and think of them as multisets. Just be careful to always put the items on the list in nonincreasing order.<br /><br />on [] is the empty sum - 0<br />on [on []] is <span class="latex">\omega^0=1</span><br />on [on [on []]] is <span class="latex">\omega^1=\omega</span><br />on [on [on []],on []] is <span class="latex">\omega+1</span><br /><br />It is interesting that the ordering given by instance Ord is <i>exactly</i> the standard ordering used in mathematics to compare ordinals. (It doesn't matter if you use multisets or sorted lists.) We got it out of nothing. Some other operations are also nicely implemented. The function <span class="latex">\omega^x</span> is simply f x = on [x]. The <a href="http://en.wikipedia.org/wiki/Ordinal_arithmetic#Natural_operations">natural sum</a> is sum of multisets (or merging of sorted lists). Normal addition isn't hard to write too.<br /><br /><b>Natural numbers</b><br /><br />Peano's natural numbers can be written as<br /><br /><pre>data Nat = Succ Nat | Zero</pre><br /><br />or<br /><br /><pre>data Nat = Nat (Maybe Nat)</pre><br /><br /><b>The common pattern</b><br /><br />What we have done above was finding a type X such that X=F(X) for some type constructor F (lists, sets, multisets, Maybe). This is the fixed point of F!<br /><br /><pre><br />data Y f = Y (f (Y f))<br />a = Y [Y [], Y [Y [], Y []]]<br /><br />ghci> :t a<br />a :: Y []<br />ghci> :k Y<br />Y :: (* -> *) -> *<br /></pre><br /><br />It works. However, we can't show it (deriving (Show) won't help). <br /><br /><b>Problem:</b> Write an instance of Show. My solution is a workaround.<br /><br /><br /><br /><br /><br /><b>Solution:</b><br /><br />I do hope you tried and convinced yourself that something like<br /><br /><pre><br />instance (Show (f a), Show a) => Show (Y f) where<br /> show x = "Y " ++ (show x)<br /></pre><br /><br />or similar won't work. What we want is, in pseudocode:<br /><br /><pre><br />instance (forall a. Show a => Show (f a)) => Show (Y f) where<br /> show x = "Y " ++ (show x)<br /></pre><br /><br />In other words we require that f is a type constructor that conveys showability: if x is showable, then f x is showable too. I made a separate type class for such f.<br /><br /><pre><br />class Show' f where<br /> show' :: (Show a) => f a -> String<br /><br />instance Show' [] where<br /> show' = show<br /><br />instance Show' Set where<br /> show' = show<br /><br />instance Show' Multiset where<br /> show' = show<br /><br />instance Show' f => Show (Y f) where<br /> show (Y x) = "Y " ++ (show' x)<br /><br />ghci> a<br />Y [Y [],Y [Y [],Y []]]<br /></pre><br /><br />Much better solutions are given in comments.<br /><br />The same boilerplate can be used for Eq and Ord to get two last examples as Y Set and Y Multiset. The instance of Ord gives you lexicographic order on the words in Dyck language (Y []), ordering of natural numbers written in binary (Y Set), ordering of natural numbers in unary (Y Maybe), and the normal ordering of ordinals (Y Multiset).<br /><br /><b>Exercise:</b><br /><pre><br />data H a = H (Maybe (Integer, a))<br /></pre><br /><br />What is Y H? Write functions <br /><br /><pre>convert :: that_type -> Y H<br />convert2 :: Y H -> that_type</pre><br /><br />If you're stuck, try to construct some value of type Y H.<br /><br /><br /><br /><br /><br /><b>Solution:</b><br /><br />Our fixed point equation is t = Maybe (Integer, t). I discussed this <a href="http://monoidal.blogspot.com/2009/08/some-thoughts-and-exercises-on-folding.html">last time</a>: these are lists. The conversion functions we are looking for are fold and unfold. I'll write another version of foldr I mentioned previously:<br /><br /><pre><br />foldr2 :: (Maybe (a,b) -> b) -> [a] -> b<br />foldr2 f = foldr (curry (f . Just)) (f Nothing)<br /><br />convert :: Y Helper -> [Integer]<br />convert2 :: [Integer] -> Y Helper<br /><br />convert = unfoldr (\(Y (H x)) -> x)<br />convert2 = foldr2 (Y . H)<br /></pre><br /><br />Many other recursive types like binary trees or infinite streams can be treated similarily.<br /><br />I ought to add infinite lists are lurking here. Our balanced brackets type has other inhabitants, like [[],[],...] or [[[...]]]. You shouldn't worry about that. First, we don't have to use all values of the type: as long as we're careful, they won't show up unexpectedly and you may regard the type as the type of finite lists. Second, you can enforce that with strictness. Third and most important point, infinite lists appear quite naturally and they do have applications. I'll give an example later.<br /><br />[Update: expanded on the hereditarily finite sets. Thanks to Ryan Ingram and Edward Kmett for great solutions of Show (Y f).]<br /><br />[Update 17 Sep: I've found a <a href="http://logic.csci.unt.edu/tarau/research/2009/fISO.pdf">paper</a> (7 MB) covering very much of what I said. Haven't read it yet, but looks very promising.]ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com3tag:blogger.com,1999:blog-3679812208800765969.post-50620361393351989932009-08-22T09:36:00.000-07:002010-04-26T06:51:04.149-07:00Some thoughts and exercises on foldingI assume you know what are foldl and foldr and have basic experience with them - you know how to express functions like sum, maximum using these folds. <a href="http://cale.yi.org/index.php/Fold_Diagrams">Here</a> are some very nice diagrams showing fold and related functions.<br /><br />Warmup exercise:<br /><br /><span style="font-family:courier new;">compose :: [a -> a] -> a -> a</span><br /><span style="font-family:courier new;">compose [f1, f2, ..., fn] = f1 . f2 . ... . fn</span><br /><br />Write <span style="font-family:courier new;">map</span> and <span style="font-family:courier new;">compose</span> using <span style="font-family:courier new;">foldr</span>. Write <span style="font-family:courier new;">foldr</span> using <span style="font-family:courier new;">map</span> and <span style="font-family:courier new;">compose</span>.<br /><br />Solution at the end.<br /><br /><span style="font-weight: bold;">Automata</span><br />A finite automaton is some device that has finitely many states (finite memory), reads a string, letter by letter, and changes its state according to some fixed transition rules. For example, it can remember if the number of a's was even or odd - it toggles a single bit after each 'a'. Here's an automaton that checks if the whole word is built of 'x' and 'y' only:<br /><br /><span style="font-family:courier new;">aut = foldl (\state a -> state && (a == 'x' || a == 'y')) True</span><br /><br />Automata are really doing foldl. In this case we could have written this more easily using <span style="font-family:courier new;">all</span>, but in general the behaviour can be quite complex.<br /><br />Exercise:<br /><br />I described a deterministic automaton - it always worked in the same way.<br /><br /><span style="font-family:courier new;">deterministic :: (a -> b -> a) -> a -> [b] -> a</span><br /><span style="font-family:courier new;">deterministic = foldl</span><br /><br />Now, we have a nondeterministic one - it can choose from some list of possible states and go on. Return all possible states the automaton could finish with.<br /><br /><span style="font-family:courier new;">nondeterministic :: (a -> b -> [a]) -> a -> [b] -> [a]</span><br /><br />Don't worry about removing duplicates.<br /><br /><br /><br />Solution:<br /><br />You can regard a nondeterministic automaton as a deterministic one whose states are lists of states.<br /><br />Our transition function is a -> b -> [a]. To use foldl, we need [a] -> b -> [a].<br /><br /><span style="font-family:courier new;">convert :: (a -> b -> [a]) -> [a] -> b -> [a]</span><br /><span style="font-family:courier new;">convert f m a = concatMap (\x -> f x a) m</span><br /><br /><span style="font-family:courier new;">nondeterministic f s = foldl (convert f) [s]</span><br /><br />Does the convert function remind you of something? We can easily change the code to work with Maybe - the automaton will be deterministic, but it will be able to abort the computation anytime. It could also ask the user about the next state using IO. It's the list monad.<br /><br /><span style="font-family:courier new;">convert' :: (Monad m) => (a -> b -> m a) -> m a -> b -> m a</span><br /><span style="font-family:courier new;">convert' f m a = m >>= (\x -> f x a)</span><br /><br /><span style="font-family:courier new;">nondeterministic' :: (Monad m) => (a -> b -> m a) -> a -> [b] -> m a</span><br /><span style="font-family:courier new;">nondeterministic' f s = foldl (convert' f) (return s)</span><br /><br />This function is called <span style="font-family:courier new;">foldM</span> and is available in Control.Monad.<br /><br /><span style="font-family:courier new;">foldM :: (Monad m) => (a -> b -> m a) -> a -> [b] -> m a</span><br /><br /><span style="font-weight: bold;">Unfolding</span><br />Suppose you have types a,b such that b = 1 + a b. Then, by substituting this equality into itself, we get<br /><br />b = 1 + ab = 1 + a(1 + ab) = 1 + a + aab = 1 + a + aa(1 + ab) = 1 + a + aa + aaa + aaab = ... = 1 + a + aa + aaa + ...<br /><br />b has changed into 1 + a + a a + a a a + ... This is the same as a list, [a].<br /><br />Equality of types x=y means that we can pair corresponding x's and y's. But we don't need that. Instead, we just need a map b -> 1 + a b that doesn't have to be an isomorphism. We can change all "equals" signs in above reasoning to ->:<br /><br />b -> 1 + ab -> 1 + a(1 + ab) -> ... -> 1 + a + aa + ... -> [a]<br /><br />and it stays OK. So, given a function (b -> 1 + a b), we get b -> [a]. This is known as unfolding. This name is very suggestive - we <span style="font-style: italic;">unfolded</span> b into a list of a's. Since 1 + a is called in Haskell Maybe a, we have a higher order function<br /><br />unfold :: (b -> Maybe (a, b)) -> (b -> [a])<br /><br />Exercise: Write it.<br /><br /><br /><br />Solution:<br /><br /><span style="font-family:courier new;"><pre><br />unfold f x = case f x of<br /> Nothing -> []<br /> Just (a,x') -> a:(unfold f x')<br /></pre></span><br /><br />Data.List calls this function unfoldr.<br /><br />If you invert this reasoning, given a function (f :: 1 + a b -> b) you get [a] -> b. This is folding. <span style="font-family:courier new;">f Nothing</span> is our initial value, and<span style="font-family:courier new;"> f $ Just (a,b)</span> tells how to combine a and b.<br /><br /><span style="font-weight: bold;">Fold vs unfold</span><br />Some simple exercises. Recursion is not allowed directly, use only foldl, foldr and unfold.<br /><br />1. Write factorial.<br /><br />2. Write functions<br /><br />toBinary :: Integer -> [Bool]<br />fromBinary :: [Bool] -> Integer<br /><br />that convert between a natural number and its binary representation.<br />For example, fromBinary [False, True, True] == 6.<br /><br />3. Now you have binary numbers. Write <a href="http://en.wikipedia.org/wiki/Exponentiation_by_squaring">exponentiation by squaring</a>.<br /><br />power :: (Monoid a) => a -> Integer -> a<br /><br />Exponent will be nonnegative.<br /><br /><span style="font-weight: bold;">A natural number is a list</span><br />An important degenerate case of lists are natural numbers. A list of () is really a natural number (its length). This is <a href="http://en.wikipedia.org/wiki/Unary_numeral_system">unary numeral system</a>.<br /><br />foldl :: (a -> b -> a) -> a -> [b] -> a<br /><br />If we take b = (), we get<br /><br />foldl' :: (a -> a) -> a -> Integer -> a<br /><br />This is n-th power of a function.<br /><br /><span style="font-weight: bold;">Other resources</span><br />If you're interested in fold, check out these resources. <span style="font-weight: bold;">They are really worth reading and will give you much insight and many intereresting ideas.</span><br /><br />* <a href="http://www.cs.nott.ac.uk/~gmh/fold.ps">A tutorial on the universality and expressiveness of fold</a><br />* <a href="http://www.haskell.org/sitewiki/images/1/14/TMR-Issue6.pdf">The Monad.Reader 6</a><br />* <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.125">Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire</a><br />* <a href="http://www.cs.nott.ac.uk/~gmh/methods.pdf">Proof methods for structured corecursive programs</a><br /><br />Solution to the warmup exercise:<br /><br /><span style="font-family:courier new;">map f = foldr (\a x -> f x : a) []</span><br /><span style="font-family:courier new;">compose = foldr (.) id</span><br /><span style="font-family:courier new;">foldr f a xs = compose (map f xs) a</span><br /><br />Here's another version of compose, by roconnor:<br /><br /><span style="font-family:courier new;">compose l x = foldr ($) x l</span>ghttp://www.blogger.com/profile/04686862403622560424noreply@blogger.com2