- Haskell-Cafe - Haskell.org

Re: monad subexpressions
by Brian Hulley 06 Aug '07

06 Aug '07

On Fri Aug 3 06:06:31 EDT Neil Mitchell wrote: > What are the semantics of > do b >> f (<- a) > where does the evaluation of a get lifted to? I suggest the execution of (a) should be done immediately before the action obtained by applying the monadic function whose argument it is part of: do b >> ( a >>= \ra -> f ra) Similarly, I'd desugar if (<- a) then f (<- b) else g (<- c) to a >>= \ra -> if ra then (b >>= \rb -> f rb) else (c >>= \rc -> g rc) I think it would just be confusing to have to think about lines in the "do" block since "do" blocks are just syntactic sugar. The only possible thing that might be needed by the "do" block is to define what monad the action should be evaluated in. Perhaps the rule could be that if (<- a) occurs in some expression the compiler should search for the nearest enclosing "do" block to identify which monad (a) should be evaluated in, then should again search outwards from the expression (<- a) to find the nearest enclosing expression (mexp) which yields a result in that same monad, then desugar to (a >>= \ra -> mexp') where mexp' is obtained from mexp by replacing that occurrence of (<- a) by (ra). (Evaluations would be done in the same order as depth first traversal of their occurrences in mexp) Regarding objections by others about (<- a) being confused with a section, (<-) is not a valid operator therefore it can't be part of a section so no confusion should arise imho... Best regards, Brian.

1 0

Knuth Morris Pratt for Lazy Bytestrings implementation
by Justin Bailey 05 Aug '07

05 Aug '07

I've implemented KMP string searching for lazy bytestrings, and I'd like some help improving the performance of the code. I'd also like to know if it doesn't look correct - I've tested it pretty extensively but you never know ... I've been testing on a 7 MB file, where the search sequence is not found. Using strict byestrings, lazy bytestrings, and regular strings, I've found my algorithm is about twice as slow as the strict version. Surprisingly, the strict version is a little bit *slower* than the regular strings version. Thanks for any comments or help! Justin

7 14

Haskell FCGI server.
by George Moschovitis 05 Aug '07

05 Aug '07

Dear devs, is it possible to create a FCGI server that listens to a specific port using the Haskell FCGI library? The front end web server would then communicate with this back end FCGI server through this port. A small example would be really appreciated. thanks, George. -- http://nitroproject.org http://phidz.com http://blog.gmosx.com http://cull.gr http://www.joy.gr http://www.me.gr

2 1

FreeBSD/amd64 support?
by Tim Newsham 05 Aug '07

05 Aug '07

I noticed that there is no official FreeBSD/amd64 port yet, although there's a binary with a working "ghc" but non-working "ghci." Has there been any progress on the amd64 port? Any estimate on when it will be available? Any known workarounds (is it possible to install and run an x86 ghc in FreeBSD/amd64)? Is hardware access holding anyone up? Tim Newsham http://www.thenewsh.com/~newsham/

1 0

Developing Programs and Proofs Spontaneously using GADT
by Shin-Cheng Mu 05 Aug '07

05 Aug '07

I am curious about the possibility of developing Haskell programs spontaneously with proofs about their properties and have the type checker verify the proofs for us, in a way one would do in a dependently typed language. In the exercise below, I tried to redo part of the merge-sort example in Altenkirch, McBride, and McKinna's introduction to Epigram [1]: deal the input list into a binary tree, and fold the tree by the function merging two sorted lists into one. The property I am going to show is merely that the length of the input list is preserved. Given that dependent types and GADTs are such popular topics, I believe the same must have been done before, and there may be better ways to do it. If so, please give me some comments or references. Any comments are welcomed. > {-# OPTIONS_GHC -fglasgow-exts #-} To begin with, we define the usual type-level representation of natural numbers and lists indexed by their lengths. > data Z = Z deriving Show > data S a = S a deriving Show > data List a n where > Nil :: List a Z > Cons :: a -> List a n -> List a (S n) 1. Append To warm up, let us see the familiar "append" example. Unfortunately, unlike Omega, Haskell does not provide type functions. I am not sure which is the best way to emulate type functions. One possibility is to introduce the following GADT: > data Plus m n k where --- m + n = k > PlusZ :: Plus Z n n > PlusS :: Plus m n k -> Plus (S m) n (S k) such that Plus m n k represents a proof that m + n = k. Not having type functions, one of the possible ways to do append is to have the function, given two lists of lengths m and n, return a list of length k and a proof that m + n = k. Thus, the type of append would be: append :: List a m -> List a n -> exists k. (List a k, Plus m n k) In Haskell, the existential quantifier is mimicked by forall. We define: > data DepSum a p = forall i . DepSum (a i) (p i) The term "dependent sum" is borrowed from the Omega tutorial of Sheard, Hook, and Linger [2] (why is it called a sum, not a product?). The function append can thus be defined as: > append :: List a m -> List a n -> DepSum (List a) (Plus m n) > append Nil ys = DepSum ys PlusZ > append (Cons x xs) ys = > case (append xs ys) of > DepSum zs p -> DepSum (Cons x zs) (PlusS p) Another possibility is to provide append a proof that m + n = k. The type and definition of of append would be: < append :: Plus m n k -> List a m -> List a n -> List a k < append PlusZ Nil ys = ys < append (PlusS pf) (Cons x xs) ys = Cons x (append pf xs ys) I thought the second append would be more difficult to use: to append two lists, I have to provide a proof about their lengths! It turns out that this append actually composes easier with other parts of the program. We will come to this later. 2. Some Lemmas Here are some lemmas represented as functions on terms. The function, for example, converts a proof of m + (1+n) = k to a proof of (1+m) + n = k. > incAssocL :: Plus m (S n) k -> Plus (S m) n k > incAssocL PlusZ = PlusS PlusZ > incAssocL (PlusS p) = PlusS (incAssocL p) > incAssocR :: Plus (S m) n k -> Plus m (S n) k > incAssocR (PlusS p) = plusMono p > plusMono :: Plus m n k -> Plus m (S n) (S k) > plusMono PlusZ = PlusZ > plusMono (PlusS p) = PlusS (plusMono p) For example, the following function revcat performs list reversal by an accumulating parameter. The invariant we maintain is m + n = k. To prove that the invariant holds, we have to use incAssocL. > revcat :: List a m -> List a n -> DepSum (List a) (Plus m n) > revcat Nil ys = DepSum ys PlusZ > revcat (Cons x xs) ys = > case revcat xs (Cons x ys) of > DepSum zs p -> DepSum zs (incAssocL p) 3. Merge Apart from the proof manipulations, the function merge is not very different from what one would expect: > merge :: Ord a => List a m -> List a n -> DepSum (List a) (Plus m n) > merge Nil ys = DepSum ys PlusZ > merge (Cons x xs) Nil = append (Cons x xs) Nil > merge (Cons x xs) (Cons y ys) > | x <= y = case merge xs (Cons y ys) of > DepSum zs p -> DepSum (Cons x zs) (PlusS p) > | otherwise = case merge (Cons x xs) ys of > DepSum zs p -> DepSum (Cons y zs) (plusMono p) The lemma plusMono is used to convert a proof of m + n = k to a proof of m + (1+n) = 1+k. 4. Sized Trees We also index binary trees by their sizes: > data Tree a n where > Nul :: Tree a Z > Tip :: a -> Tree a (S Z) > Bin :: Tree a n1 -> Tree a n -> > (Plus p n n1, Plus n1 n k) -> Tree a k The two trees given to the constructor Bin have sizes n1 and n respectively. The resulting tree, of size k, comes with a proof that n1 + n = k. Furthermore, we want to maintain an invariant that n1 either equals n, or is bigger than n by one. This is represented by the proof Plus p n n1. In the definition of insertT later, p is either PlusZ or PlusS PlusZ. 5. Lists to Trees The function insertT inserts an element into a tree: > insertT :: a -> Tree a n -> Tree a (S n) > insertT x Nul = Tip x > insertT x (Tip y) = Bin (Tip x) (Tip y) (PlusZ, PlusS PlusZ) > insertT x (Bin t u (PlusZ, p)) = > Bin (insertT x t) u (PlusS PlusZ, PlusS p) > insertT x (Bin t u (PlusS PlusZ, p)) = > Bin t (insertT x u) (PlusZ, PlusS (incAssocR p)) Note that whenever we construct a tree using Bin, the first proof, corresponding to the difference in size of the two subtrees, is either PlusZ or PlusS PlusZ. The counterpart of foldr on indexed list is defined by: > foldrd :: (forall k . (a -> b k -> b (S k))) -> b Z > -> List a n -> b n > foldrd f e Nil = e > foldrd f e (Cons x xs) = f x (foldrd f e xs) The result is also an indexed type (b n). The function deal :: List a n -> Tree a n, building a tree out of a list, can be defined as a fold: > deal :: List a n -> Tree a n > deal = foldrd insertT Nul 6. Trees to Lists, and Merge Sort The next step is to fold through the tree by the function merge. The first two clauses are simple: > mergeT :: Ord a => Tree a n -> List a n > mergeT Nul = Nil > mergeT (Tip x) = Cons x Nil For the third clause, one would wish that we could write something as simple as: mergeT (Bin t u (_,p1)) = case merge (mergeT t) (mergeT u) of DepSum xs p -> xs However, this does not type check. Assume that t has size n1, and u has size n. The DepSum returned by merge consists of a list of size i, and a proof p of type Plus m n i, for some i. The proof p1, on the other hand, is of type P m n k for some k. Haskell does not know that Plus m n is actually a function and cannot conclude that i=k. To explicitly state the equality, we assume that there is a function plusFn which, given a proof of m + n = i and a proof of m + n = k, yields a function converting an i in any context to a k. That is: plusFn :: Plus m n i -> Plus m n k -> (forall f . f i -> f k) The last clause of mergeT can be written as: > mergeT (Bin t u (_,p1)) = > case merge (mergeT t) (mergeT u) of > DepSum xs p -> plusFn p p1 xs How do I define plusFn? I would like to employ the techniques related to equality types [3,4,5], but currently I have not yet figured out how. I've merely produced a version of plusFn specialised to List a: > plusFn :: Plus m n h -> Plus m n k -> List a h -> List a k > plusFn PlusZ PlusZ xs = xs > plusFn (PlusS p1) (PlusS p2) (Cons x xs) = > Cons x (plusFn p1 p2 xs) Needless to say this is not satisfactory. Now that we have both deal and mergeT, merge sort is simply their composition: > msort :: Ord a => List a n -> List a n > msort = mergeT . deal The function mergeT can be defined using a fold on trees as well. Such a fold might probably look like this: > foldTd :: (forall m n k . Plus m n k -> b m -> b n -> b k) > -> (a -> b (S Z)) -> b Z > -> Tree a n -> b n > foldTd f g e Nul = e > foldTd f g e (Tip x) = g x > foldTd f g e (Bin t u (_,p)) = > f p (foldTd f g e t) (foldTd f g e u) mergeT :: Ord a => Tree a n -> List a n mergeT = foldTd merge' (\x -> Cons x Nil) Nil where merge' p1 xs ys = case merge xs ys of DepSum xs p -> plusFn p p1 xs I am not sure whether this is a "reasonable" type for foldTd. 7. Passing in the Proof as an Argument Previously I thought the second definition of append would be more difficult to use, because we will have to construct a proof about the lengths before calling append. In the context above, however, it may actually be more appropriate to use this style of definitions. An alternative definition of merge taking a proof as an argument can be defined by: < merge :: Ord a => Plus m n k -> List a m -> < List a n -> List a k < merge PlusZ Nil ys = ys < merge pf (Cons x xs) Nil = append pf (Cons x xs) Nil < merge (PlusS p) (Cons x xs) (Cons y ys) < | x <= y = Cons x (merge p xs (Cons y ys)) < | otherwise = Cons y (merge (incAssocL p) (Cons x xs) ys) A definition of mergeT using this definition of merge follows immediately because we can simply use the proof coming with the tree: < mergeT :: Ord a => Tree a n -> List a n < mergeT Nul = Nil < mergeT (Tip x) = Cons x Nil < mergeT (Bin t u (_,p1)) = < merge p1 (mergeT t) (mergeT u) I don't know which approach can be called more "natural". References [1] Thorsten Altenkirch, Conor McBride, and James McKinna. Why Dependent Types Matter. http://www.e-pig.org/downloads/ydtm.pdf [2] Tim Sheard, James Hook, and Nathan Linger. GADTs + Extensible Kinds = Dependent Programming. http://web.cecs.pdx.edu/~sheard/papers/GADT+ExtKinds.ps [3] James Cheney, Ralf Hinze. A lightweight implementation of generics and dynamics. [4] Stephanie Weirich, Type-safe cast: (functional pearl), ICFP 2000. [5] Arthur I. Baars , S. Doaitse Swierstra, Typing dynamic typing, ACM SIGPLAN Notices, v.37 n.9, p.157-166, September 2002 Appendix. Auxiliary Functions > instance Show a => Show (List a n) where > showsPrec _ Nil = ("[]"++) > showsPrec _ (Cons x xs) = shows x . (':':) . shows xs > instance Show (Plus m n k) where > showsPrec _ PlusZ = ("pZ"++) > showsPrec p (PlusS pf) = showParen (p>=10) (("pS " ++) . > showsPrec 10 pf) > instance Show a => Show (Tree a n) where > showsPrec _ Nul = ("Nul"++) > showsPrec p (Tip x) = showParen (p >= 10) (("Tip " ++) . shows x) > showsPrec p (Bin t u pf) = > showParen (p>=10) > (("Bin "++) . showsPrec 10 t . (' ':) . showsPrec 10 u . > (' ':) . showsPrec 10 pf)

5 4

Question about arrows
by Lewis-Sandy, Darrell 04 Aug '07

04 Aug '07

Is there a class property of the Control.Arrow class that represents the evaluatation of an arrow: eval :: (Arrow a)=>a b c->b->c I am writing some higher order code that I would like to work with either functions or partial functions (implemented as balanced binary search trees) and don't want to write separate instances for each concrete arrow type. For example, consider the example below: divideAndConquer::( Arrow a, Bifunctor m)=>(m c y->y)->a b c->(x->m b x)->x->y divideAndConquer combine solve divide = combine.(bimap (eval solve) (divideAndConquer combine solve divide)).divide that implements datatype generic divide and conquer. divide encodes how to decompose a problem of type x into subproblems, solve encodes how to solve indivisible sub-problems, and combine encodes how to put the sub-solutions together. The branching strategy is encoded in the bifunctor, and the use of eval faciliatates either evaluating a function or looking up solutions in a table.

3 2

Re: [Haskell-cafe] Re: Re: monad subexpressions
by david48 04 Aug '07

04 Aug '07

Sorry for the double post, I posted with the wrong email address and haskell-cafe rejected it. On 8/3/07, Neil Mitchell <ndmitchell(a)gmail.com> wrote: > > Right. In effect, as a matter of fact, the notation > > > > x <- a > > > > would become equivalent to > > > > let x = (<- a) > > Hmm, interesting. Consider: > > let x = 12 > let x = (<- x) Wouldn't that be forbidden ? I'd expect the x in ( <- x ) have to be of type m a. If you meant : x <- return 12 let x = ( <- x ) Then I imagine it would turn into x <- return 12 x >>= \tx -> let x = tx in .... Isn't that correct ?

4 3

When is waitForProcess not necessary?
by Dave Bayer 04 Aug '07

04 Aug '07

If one is calling runInteractiveCommand for a "sure-thing" returning a small amount of output (say, "ls" for a modest directory"), is it necessary to call waitForProcess? My waitForProcess calls came under scrutiny when I tried to GHC profile a threaded process, which isn't possible. It turns out that my programs run faster if they don't call waitForProcess, and it sure seems empirically that they never fail to run correctly. It would seem to me that in a lazy language, later code wouldn't presume it was looking at an entire string until the actual EOF came through, completing the string. So at the end of a program, with nothing else to do but wait, why not wait "implicitly" rather than via an explicit call to waitForProcess? What am I missing? (I've searched this forum; an interesting example is runCommand in http://happs.org/HAppS/src/HAppS/Util/Common.hs but I'm asking why this isn't overkill in my scenario. I'm actually calling Markdown.pl on tiny files (source code of lengths a human would read), and it is certainly sluggish enough to be a fair test.)

6 8

Re: RE [Haskell-cafe] Monad Description For Imperative
by Greg Meredith 04 Aug '07

04 Aug '07

Haskellians, i am delighted to see vigorous exchange that actually resulted in change of positions. i confess i was going to give up, but glad others stepped into the breach. This is yet another indication of what an unusual community this is. Best wishes, --greg Date: Fri, 3 Aug 2007 13:43:32 +1200 From: ok <ok(a)cs.otago.ac.nz> Subject: Re: RE [Haskell-cafe] Monad Description For Imperative To: haskell-cafe Cafe <haskell-cafe(a)haskell.org> Message-ID: <8575BD1C-2113-4D48-A3D4-BDFF41238BB9(a)cs.otago.ac.nz> Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed I asked "How is IO a functor"? On 3 Aug 2007, at 11:50 am, Dan Piponi wrote: > IO is a fully paid up Monad in the categorical sense. The category is > the category whose objects are types and whose arrows are functions > between those types. IO is a functor. The object a maps to IO a. An > arrow f::a->b maps to (>>= return . f)::IO a -> IO b and that can be > used to make IO an instance of Functor. The natural transforms eta and > mu are called return and join. Please go over this again, but slowly this time. You have convinced me, but I'd like to understand the details a little better. I see that any type constructor TC :: * -> * is halfway to being a functor on this category of types. It acts on the objects in the obvious way, so the next step is to see about the arrows. If f :: a -> b then we want TC f :: TC a -> TC b such that TC (f . g) = TC f . TC g and TC (id::a->a) = id :: TC a -> TC a Now this is precisely the Haskell Functor class, so TC is the object part and fmap is the arrow part. You say that (>>= return . f) can be used to make [a Monad] an instance of Functor. Try it... by golly it's true. I see: fmap f = (>>= return . f). So why *aren't* Monads already set up using the type class machinery to always *be* Functors in Haskell? Isn't it bound to confuse people if monads are functors but Monads are not Functors? This is especially puzzling because Maybe, [], and IO already *are* Functors, but the way this is done makes it look accidental, not like the fundamental property of Monads it apparently is. (By the way, I note that the on-line documentation for Control.Monad glosses >>= as "Sequentially composes two actions...".) -- L.G. Meredith Managing Partner Biosimilarity LLC 505 N 72nd St Seattle, WA 98103 +1 206.650.3740 http://biosimilarity.blogspot.com

1 0

Re: [Haskell-cafe] Re: monad subexpressions
by Mirko Rahn 03 Aug '07

03 Aug '07

>>> rewrite *p++=*q++ in haskell? >> *p = *(p+1) ; *q = *(q+1) > If that's true then GCC has gone insane, because they are completely different. Of course you are right, I just observed at the wrong place..., sorry for that. > Though, as any C programmer knows, you really should be using > memcpy() I like to hear that you would reject it either. /BR -- -- Mirko Rahn -- Tel +49-721 608 7504 -- --- http://liinwww.ira.uka.de/~rahn/ ---

1 0