Re: [Haskell-cafe] Haskell maximum stack depth
Neil Mitchell wrote: Hi If you mean an example of coding style and choice of stack vs. heap, I already have.. http://www.haskell.org/pipermail/haskell-cafe/2008-January/038832.html I'm at a loss as why you want a strict version of take. It's clearly not for performance, as it performs slower. I'd say both the gobbler programs have a bug, namely that they are not sufficiently lazy. I have already partially scanned the list looking for the first element that satisfies some condition, using a tail recursive search. If such an element is found I want to split the list at that point. If such an element is not found the entire list has been scanned without using any extra stack or heap (other than that used by the list itself and the condition test). I could build the reversed list accumulator on the heap as I did the search, but I don't because this will be completely wasted effort in the case where such an element is not found. So instead I just use an unboxed Int to count how far I get and have the search return this and the unsearched suffix (in the case where a matching element is found). But the lifetimes of the list prefix and suffix from this point on are completely unrelated so I don't want the prefix thunk to be hanging on to the unknown sized suffix. As I already know that the list has been evaluated at least up to the point that it gets chopped off, I choose to use a strict (eager) take. As an aside, my version of this function would be: neilGobbler :: Int - [x] - [x] neilGobbler n xs = length res `seq` res where res = take n xs I have no idea if it takes the heap or the stack, or if it performs faster or slower. If you still have whatever test you used on the gobbler, perhaps you could tell us. My guess is it will use O(1) stack and burn O(n) heap (in addition that actually used by the result), so assymptotic complexity wise same as heapGobbler, but probably higher constant factors with ghc due to lazy building of take thunks and subsequent reduction and indirection costs. If you mean an example of it biting with lazy code, this is discussed so often you'd be spoiled for choice if you search the mailing list archives. Here's a good one.. http://www.haskell.org/pipermail/haskell-cafe/2005-December/013521.html This example actually shows the problem twice. In one case it's solvable by using foldl' instead of foldl. Which reduces the memory from O(n) to O(1). Are you sure about that? Using foldl' here eliminates one of the two possible sources of stack overflow, but it doesn't eliminate a space leak. It's O(n) either way. Using strict Map insertion will eliminate a space leak (in this case) and also a possible source stack overflow. Surely thats a good thing, Would be if it was true :-) and the code before had a space leak. Space leak is bad, therefore telling people about it is good. There are plenty of space leaks that won't cause stack overflows, and plenty of stack overflows that aren't caused by space leaks (see above for one example). Again I have to say that even if true, I think this is a pretty lame justification for the current implementation. The *default* behaviour of any useful program should surely be to make best effort to carry on working (and in due course deliver an answer or whatever), even if there is unexpectedly high stack use for some reason (that may or may not be a bug). I think its sensible to let people set their own stack bound (which is possible), I have no objection to people bounding their stack if that's their choice. I can't imagine why anybody who stopped to think about this would actually want this feature, but it's free world. What I object to is it being bounded by default to something other than overall program memory limit. I know that I could probably achieve this effect myself with +RTS options, but I also want to be able to write libraries that other people are going to use safely without having to add a appropriate warning in the documentation to the effect that some parts use O(n) stack space deliberately, by design. But of course this all assumes that underlying implementation is sufficiently robust to make unbounded stacks safe (at least as safe as any other unbounded data structure). Unfortunately it seems this isn't the case at present if what various folk have told me is true. but that clearly just from taking an informal poll of respondants to this thread, the current default should indeed be the default. You seem to be the only person clamouring for an unlimited stack, Yes, this is strange. Same thing happened in the global variables debate despite it being obvious to any thinking person that I was correct. Denial of the reality of some very simple examples of the problem was typical of that debate too. :-) Regards -- Adrian Hey ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: bimap 0.2
Stuart Cook wrote: [EMAIL PROTECTED] wrote: We've called it injective maps. Does surjectivity make sense a all? In my mind, surjectivity is the property that each key in the right-hand map is a value in the left-hand map (and vice-versa). This Still, injectivity (one-to-one) is the only interesting property. The inverse (on the range) is then injective, too. Christian ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] background question about IO monad
Uwe Hollerbach wrote: lispUTCTime [] = doIOAction (getClockTime) toS allErrs where toS val = String (calendarTimeToString (toUTCTime val)) here you use liftIO (hidden in doIOAction) to use an IO action (getClockTime) inside of a different monad wich contains IO at it's base. so your custom SchemeInterpreterMonad (however it's called) is basically just an extended IO monad. lispUTCTime [IntNumber n] = return (String (calendarTimeToString (toUTCTime (TOD n 0 here you use a pure computation to produce the result string, but then you use return to put it in the monad, too. since IO lives at the base of your custom monad, return will put the String into IO, too. you can't take the IO String out of the IO monad, but you can put the pure String in the IO monad using return. But after that, it sure seems to me as if I've taken data out of the IO monad... haven't I? Given that the second alternative never entered doIOAction and that after both are done I have a string of characters, prettily formatted to indicate a time, that's what it feels like to this unwashed C programmer. As explained above, the second alternative uses return instead of doIOAction to enter the monad. From a Haskell programmers point of view, you don't have a pure string of characters, but you have a monadic action producing such a string in both cases. That is fine, since your program is inside a REPL anyway, and the very next thing you want to do is to print the computed value, wich is another IO action. but from the point of view of the Scheme programmer using your interpreter, there is no special IO monad around, since the whole Scheme interpreter lives in IO and IO is available to him everywhere. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell maximum stack depth
Hi I have already partially scanned the list looking for the first element that satisfies some condition, using a tail recursive search. If such an element is found I want to split the list at that point. span/break? I really can't believe the memory overhead of span is that terrible, you are only duplicating the (:)'s and its only one traversal. As an aside, my version of this function would be: neilGobbler :: Int - [x] - [x] neilGobbler n xs = length res `seq` res where res = take n xs My guess is it will use O(1) stack and burn O(n) heap (in addition that actually used by the result), so assymptotic complexity wise same as heapGobbler, but probably higher constant factors with ghc due to lazy building of take thunks and subsequent reduction and indirection costs. Sure? Guessing constant factors related to strictness and laziness is incredibly hard! My guess based on gut feeling is that the program will take less time, and use half the memory. But given my initial comment, that guess is not very reliable. Yes, this is strange. Same thing happened in the global variables debate despite it being obvious to any thinking person that I was correct. Denial of the reality of some very simple examples of the problem was typical of that debate too. The particular world I live in is special, but I like it :-) Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] background question about IO monad
Hello Uwe, Wednesday, February 6, 2008, 7:44:27 AM, you wrote: But after that, it sure seems to me as if I've taken data out of the IO monad... this means that you can't use results of IO actions in pure functions. your code works in some transformed version of IO monad, so you don't escaped it if we call pure functions as functions and non-pure ones as procedures, the rule is functions can't call procedures, but all other activity is possible. in your do_action you calls procedure (to format current time) and call a function (to format given time). do_action is procedure (because it works in transformed IO monad), so you don't break any rules -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Inverting a Monad
Hello, Is there a way to 'invert' an arbitrary Monad? By 'inverting' I mean to turn success into failure and failure into success. Here are some specific inversions of the Maybe and List Monad: invM :: Maybe a - Maybe () invM Nothing = Just () invM (Just _) = Nothing invL :: [] a - [] () invL []= [()] invL (_:_) = [] How can I define this for an arbitrary Monad m? More specifically, I would like to define: inv :: (Monad m, M.MonadPlus m, ???) = m a - m () inv m = if m failsthen return () if m succeeds then fail The following obviously doesn't work: inv m = (m mzero) `mplus` return () because it will always return (). There's also a 'inversion' for natural numbers: invN :: Int - Int invN 0 = 1 invN n = 0 but how can I define that without pattern matching, so only using arithmetic operations, +, -, *, ^, ...? The reason I ask this is that I'm writing a parser combinator library to understand parser a bit better. And I would like to define the combinator: notFollowedBy :: P t m a - P t m () 'notFollowedBy p' fails when p succeeds and returns () when p fails. I will share the code when it's a bit more polished. Thanks, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
On Feb 6, 2008 9:39 AM, Miguel Mitrofanov [EMAIL PROTECTED] wrote: How can I define this for an arbitrary Monad m? Such as Identity? An arbirtrary monad can't be inverted, however there's Error and ErrorT that provide throwing and catching abilities. I guess your parser is a monad transformer, so *maybe* the solution is to require MonadError from the inner monad. Cheers, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
On Feb 6, 2008 12:39 PM, Miguel Mitrofanov [EMAIL PROTECTED] wrote: invM :: Maybe a - Maybe () invM Nothing = Just () invM (Just _) = Nothing invL :: [] a - [] () invL []= [()] invL (_:_) = [] How can I define this for an arbitrary Monad m? Such as Identity? Well in: inv :: (Monad m, ...) = m a - m () inv m = ... I don't mind that there are more constraints on 'm' than just Monad maybe a MonadPlus constraint or others are needed. (I was even thinking about a MonadTimes class as in: class MonadPlus m = MonadTimes m where mone :: m () mtimes :: m a - m a - m a ) Thanks, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
On Feb 6, 2008 12:50 PM, Miguel Mitrofanov [EMAIL PROTECTED] wrote: class Monad m = MonadInv m where inv :: m a - m () With this constraint you certainly can have your inv. Yes indeed. But I was kind of hoping that I could use standard Haskell classes without adding my own. (BTW I would like to know of other possible applications of 'inv' besides my parser. So yell if you find one please) Thanks, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] classes for data structures
Hi, I've been working a lot with maps, sets and lists. While the process of getting things out of them is abstracted by foldable, traversable and friends, the process of building one up is not. Would it be possible to have something like: class Buildable b where empty :: b a --makes an empty b with elements of type a insert :: a - b a - b a --inserts the new element into the buildable I'm not particularly wedded to the names. It's just that it would be very convenient sometimes to collect data items into e.g. a list or a set, without pushing in some klunky foralled insert function. I see that this is realted to MonadPlus, but the space of possible container classes is wider than that of monads e.g. set. Matthew ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
invM :: Maybe a - Maybe () invM Nothing = Just () invM (Just _) = Nothing invL :: [] a - [] () invL []= [()] invL (_:_) = [] How can I define this for an arbitrary Monad m? Such as Identity? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
Such as Identity? Well in: inv :: (Monad m, ...) = m a - m () inv m = ... I don't mind that there are more constraints on 'm' than just Monad class Monad m = MonadInv m where inv :: m a - m () With this constraint you certainly can have your inv. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
On Feb 6, 2008 12:45 PM, Felipe Lessa [EMAIL PROTECTED] wrote: I guess your parser is a monad transformer, so *maybe* the solution is to require MonadError from the inner monad. Indeed my parser 'P t m a' is a monad transformer. I will try out requiring 'm' to have a 'MonadError' constraint and see how far I come with that. I'll let you know. Thanks, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
On Feb 6, 2008 11:32 AM, Bas van Dijk [EMAIL PROTECTED] wrote: The following obviously doesn't work: inv m = (m mzero) `mplus` return () because it will always return (). How about: inv m = do success - (m return True) `mplus` return False if success then mzero else return () Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
On Feb 6, 2008 10:04 AM, Luke Palmer [EMAIL PROTECTED] wrote: How about: inv m = do success - (m return True) `mplus` return False if success then mzero else return () Prelude Control.Monad inv [] [()] Prelude Control.Monad inv [10] [()] -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: weird ghci behavior with gadts and existentials
Let me add: data ExpGADT t where ExpInt :: Int - ExpGADT Int ExpChar :: Char - ExpGADT Char Which type do you think 'unHide' and 'wierd' should have: unHide h = case h of Hidden (_,e) - e wierd = unHide (Hidden (TyInt,ExpInt 3)) either: unHide :: HiddenTypeExp - ExpGADT t-- Choice 1: Polymorphic t unHide :: HiddenTypeExp - ExpGADT Int -- Choice 2: Monomorphic Int Note that TypeGADT/TyInt are irrelevant to unHide and wierd. Clearly the first choice to unHide violates the encapsulation of 't'. Clearly I cannot choose the 2nd choice, since it might be an ExpChar. So unHide is impossible to write. Chris Casinghino wrote: Hi all, I've been playing a bit with gadts and existentials lately, and I have an example where I don't quite understand the behavior of ghc. The expression in question typechecks sometimes in some versions of ghc, depending on where you write it, and not in other versions. Some other people I've asked report not getting any errors, even when using apparently one of the same versions of ghc I checked. If I create a file which contains: data TypeGADT t where TyInt :: TypeGADT Int data ExpGADT t where ExpInt :: Int - ExpGADT Int data HiddenTypeExp = forall t . Hidden (TypeGADT t, ExpGADT t) weird = case Hidden (TyInt, ExpInt 3) of Hidden (TyInt, e) - e I am able to :load it into ghci just fine (with -fglasgow-exts) with version 6.8.2. However, if I then copy the line: let weird2 = case Hidden (TyInt, ExpInt 3) of Hidden (TyInt, e) - e into ghci, I get a type error. In the HEAD version 6.9, I get a type error on the definition of weird right away when I :load the file. The type error goes away if I add the line weird :: ExpGADT Int before the definition of weird. The type error in question is this: interactive:1:46: Inferred type is less polymorphic than expected Quantified type variable `t' escapes When checking an existential match that binds e :: ExpGADT t The pattern(s) have type(s): HiddenTypeExp The body has type: ExpGADT t In a case alternative: Hidden (TyInt, e) - e In the expression: case Hidden (TyInt, ExpInt 3) of Hidden (TyInt, e) - e So, several questions. 1) Why the discrepancy in behavior between :loading the file and copying in the definition in 6.8.2. It seems like, one way or the other, this should be consistent. 2) Several other people report not getting any errors at all, even people with ghc 6.8.2, one of the versions I tested. What's the right behavior? My guess would be that this should cause no type error, even without the type annotation. The GADT pattern match against TyInt in the case statement should refine the existential type variable t to Int, so no existential type variables are escaping. Is that right? 3) Is there a bug here? Are there two bugs (one, the typing error, two, the difference between ghc and ghci)? Or, do I just not understand what is going on? Sorry for the length of this email! --Chris Casinghino ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Linear algebra
On Thu, 31 Jan 2008, Denis Bueno wrote: On Thu, Jan 31, 2008 at 7:11 PM, Jon Harrop [EMAIL PROTECTED] wrote: Has anyone written anything on the use of FP (e.g. point free style) in linear algebra problems? I'm not sure how relevant this is to you, but John Backus wrote foundationally on it and related topics. http://www.stanford.edu/class/cs242/readings/backus.pdf Can Programming Be Liberated from the von Neumann Style? It's an excellent read, regardless. http://www.haskell.org/haskellwiki/Linear_algebra http://darcs.haskell.org/numeric-quest/Orthogonals.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
On Feb 6, 2008 1:49 PM, Lutz Donnerhacke [EMAIL PROTECTED] wrote: inv m = if m == mzero then return () else mzero `asTypeOf` m Interesting! :t inv inv :: (MonadPlus m, Eq (m ())) = m () - m () The 'Eq' constraint on 'm ()' is a bit problemetic I think in case 'm' is a function like a 'State'. Thanks, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] lazy evaluation
Can anybody give me a simple explanation why the second definition of a palindrome checker does not terminate, although the first one does? pal :: Eq a = [a] - Bool pal s = b where (b,r) = eqrev s r [] eqrev :: Eq a = [a] - [a] - [a] - (Bool,[a]) eqrev (x:s1) ~(y:s2) acc = (x==yb,r) where (b,r) = eqrev s1 s2 (x:acc) eqrev _ _ acc = (True,acc) pal :: Eq a = [a] - Bool pal s = b where (b,r) = eqrev' s r eqrev' :: Eq a = [a] - [a] - (Bool,[a]) eqrev' (x:s1) ~(y:s2) = (x==yb,r++[y]) where (b,r) = eqrev' s1 s2 eqrev' _ _ = (True,[]) Peter ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lazy evaluation
On Wed, 6 Feb 2008, Peter Padawitz wrote: Can anybody give me a simple explanation why the second definition of a palindrome checker does not terminate, although the first one does? Just another question, what about x == reverse x ? - You can still optimize for avoiding duplicate equality tests. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] classes for data structures
On Wed, 6 Feb 2008, Matthew Pocock wrote: Hi, I've been working a lot with maps, sets and lists. While the process of getting things out of them is abstracted by foldable, traversable and friends, the process of building one up is not. Would it be possible to have something like: class Buildable b where empty :: b a --makes an empty b with elements of type a insert :: a - b a - b a --inserts the new element into the buildable How can this interface be used both for lists and maps? I'm afraid it is difficult to find an interface that fits the needs of many different data structures. Maybe at least a generalized 'unfoldr' is possible. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] fmap vs. liftM
On Tue, 5 Feb 2008, Felipe Lessa wrote:
On Feb 5, 2008 6:06 PM, Dan Weston [EMAIL PROTECTED] wrote:
Can you do this with a GHC rule? Something like:
{-# RULES
join_dot_fmap_return/id forall x . join (fmap return x) = x
#-}
Dan
I guess this would make use of the rule (otherwise the transformation
would change the code's semantic) but would not enforce that the rule
itself is valid (which is undecidable).
I have already thought about (ab)using GHC rules for forcing programmers
to take care. :-) That is, if the rule would be stated as above, then
programmers _have_ to ensure that the law is satisfied, and the optimizer
will penalize violations of the rules with non-working code.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Signature for non-empty filter
On Tue, 5 Feb 2008, Bulat Ziganshin wrote: Hello Henning, Tuesday, February 5, 2008, 6:01:27 PM, you wrote: Is Haskell's type system including extensions strong enough for describing a function, that does not always return a trivial value? E.g. (filter (\x - x==1 x==2)) such things may be detected by (too) smart compiler, but in general it's undecidable: filter (if LifeHasMeaning then const True else odd) ;) As I said, if the programmer could specify an input on the type level for which the output is non-trivial, then this would solve the problem. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] classes for data structures
On Feb 6, 2008 9:00 AM, Henning Thielemann [EMAIL PROTECTED] wrote: On Wed, 6 Feb 2008, Matthew Pocock wrote: class Buildable b where empty :: b a --makes an empty b with elements of type a insert :: a - b a - b a --inserts the new element into the buildable How can this interface be used both for lists and maps? [...] One solution is to change the class slightly: class Buildable t x where empty :: t insert :: x - t - t instance Buildable (Map k a) (k, a) where empty = Map.empty insert = uncurry Map.insert -- Denis ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] fmap vs. liftM
On Feb 6, 2008 11:50 AM, Henning Thielemann [EMAIL PROTECTED] wrote: That is, if the rule would be stated as above, then programmers _have_ to ensure that the law is satisfied, and the optimizer will penalize violations of the rules with non-working code. Be careful. For much less (blowing up when stack 8MiB) we already had 42 messages =). -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
On Feb 6, 2008 12:51 PM, Bas van Dijk [EMAIL PROTECTED] wrote: I will try out requiring 'm' to have a 'MonadError' constraint and see how far I come with that. I'm now trying to define 'inv' using 'catchError` but I can't get it to work. The following obviously doesn't work: import Control.Monad.Error inv :: MonadError e m = m a - m () inv m = (m fail ) `catchError` \_ - (return ()) Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Signature for non-empty filter
Hello Henning, Wednesday, February 6, 2008, 5:09:56 PM, you wrote: Is Haskell's type system including extensions strong enough for describing a function, that does not always return a trivial value? E.g. (filter (\x - x==1 x==2)) such things may be detected by (too) smart compiler, but in general it's undecidable: filter (if LifeHasMeaning then const True else odd) ;) As I said, if the programmer could specify an input on the type level for which the output is non-trivial, then this would solve the problem. it's another question: you can describe trivial values using type system, but can't prohibit them using it - it's impossible because you can't check for arbitrary algorithm whether it will be finally stopped -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] classes for data structures
On Wed, 6 Feb 2008, Denis Bueno wrote: On Feb 6, 2008 9:00 AM, Henning Thielemann [EMAIL PROTECTED] wrote: On Wed, 6 Feb 2008, Matthew Pocock wrote: class Buildable b where empty :: b a --makes an empty b with elements of type a insert :: a - b a - b a --inserts the new element into the buildable How can this interface be used both for lists and maps? [...] One solution is to change the class slightly: class Buildable t x where empty :: t insert :: x - t - t instance Buildable (Map k a) (k, a) where empty = Map.empty insert = uncurry Map.insert ok, maybe with functional dependency t - x ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lazy evaluation
On Feb 6, 2008 3:06 PM, Miguel Mitrofanov [EMAIL PROTECTED] wrote:
On 6 Feb 2008, at 16:32, Peter Padawitz wrote:
Can anybody give me a simple explanation why the second definition
of a palindrome checker does not terminate, although the first one
does?
pal :: Eq a = [a] - Bool
pal s = b where (b,r) = eqrev s r []
eqrev :: Eq a = [a] - [a] - [a] - (Bool,[a])
eqrev (x:s1) ~(y:s2) acc = (x==yb,r) where (b,r) = eqrev s1 s2
(x:acc)
eqrev _ _ acc = (True,acc)
I.eqrev (_|_) acc = (True, acc)
II.a. eqrev 1 (_|_) = ('1' == (_|_) b, r) where (b,r) = eqrev
(_|_) 1
By (I), (b,r) = (True, 1), so eqrev 1 (_|_) = ((_|_),1)
II.b. eqrev 1 1 = ('1' == '1' b, r) where (b,r) = eqrev
1
(b,r) = (True,1), so eqrev 1 1 = (True,1)
Therefore, the least fixed point of \r - eqrev 1 r is 1 and
the answer is True.
pal :: Eq a = [a] - Bool
pal s = b where (b,r) = eqrev' s r
eqrev' :: Eq a = [a] - [a] - (Bool,[a])
eqrev' (x:s1) ~(y:s2) = (x==yb,r++[y]) where (b,r) = eqrev' s1 s2
eqrev' _ _ = (True,[])
I. eqrev' (_|_) = (True,[])
II.a. eqrev' 1 (_|_) = ('1' == (_|_) b, r ++ [(_|_)]) where (b,r)
= eqrev' (_|_)
By (I), (b,r) = (True,[]), so eqrev' 1 (_|_) = ((_|_),[(_|_)])
II.b. eqrev' 1 [(_|_)] = ('1' == (_|_) b, r ++ [(_|_)]) where
(b,r) = eqrev' []
(b,r) = (True,[]), so eqrev' 1 [(_|_)] = ((_|_),[(_|_)])
Therefore, the least fixed point of \r - eqrev' 1 r is [(_|_)] and
the answer is (_|_). No wonder it hangs.
This proof also shows us where the problem lies and how to fix it. It
turns out to be really easy: change 'r++[y]' to 'r++[x]' and the
program works.
Cheers,
Josef
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Data.Ord and Heaps
Roberto Zunino wrote:
I'd really like to write
class (forall a . Ord p a) = OrdPolicy p where
but I guess that's (currently) not possible.
Actually, it seems that something like this can be achieved, at some price.
data O a where O :: Ord a = O a
data O1 p where O1:: (forall a . Ord a = O (p a)) - O1 p
Ah, very nice :)
First, I change the statement ;-) to
class (forall a . Ord a = Ord p a) = OrdPolicy p
since I guess this is what you really want.
Right, modulo the fact that I also forgot the parenthesis
class (forall a . Ord a = Ord (p a)) = OrdPolicy p
So, the intention is to automatically have the instance
instance (OrdPolicy p, Ord a) = Ord (p a) where
which can be obtained from your GADT proof
compare = case ordAll of
O1 o - case o of
(O :: O (p a)) - compare
This instance declaration is a bit problematic because it contains only
type variables. Fortunately, the phantom type approach doesn't have this
problem:
data OrdBy p a = OrdBy { unOrdBy :: a }
data O a where O :: Ord a = O a
class OrdPolicy p where-- simplified O1
ordAll :: Ord a = O (OrdBy p a)
instance (Ord a, OrdPolicy p) = Ord (OrdBy p a) where
compare = case ordAll of { (O :: O (OrdBy p a)) - compare }
By making the dictionary in O explicit, we can even make this Haskell98!
class OrdPolicy p where
compare' :: Ord a = OrdBy p a - OrdBy p a - Ordering
instance (Ord a, OrdPolicy p) = Ord (OrdBy p a) where
compare = compare'
On second thought, being polymorphic in a is probably too restrictive:
the only usable OrdPolicy besides the identity is Reverse :) After
all, there aren't so many useful functions with type
compare' :: forall a. (a - a - Ordering) - (a - a - Ordering)
So, other custom orderings usually depend on the type a . Did you have
any specific examples in mind, Stephan? At the moment, I can only think
of ordering Maybe a such that Nothing is either the largest or the
smallest element
on f g x y = g x `f` g y
data Up
instance Ord a = Ord (OrdBy Up (Maybe a)) where
compare = f `on` unOrdBy
where
f Nothing Nothing = EQ
f xNothing = LT
f Nothing y= GT
f (Just x) (Just y) = compare x y
data Down
instance Ord a = Ord (OrdBy Down (Maybe a)) where
compare = f `on` unOrdBy
where
f Nothing Nothing = EQ
f xNothing = GT
f Nothing y= LT
f (Just x) (Just y) = compare x y
But I think that those two orderings merit special data types like
data Raised a = Bottom | Raise a deriving (Eq, Ord)
data Lowered a = Lower a | Top deriving (Eq, Ord)
instead of
type Raised a = OrdBy Down (Maybe a)
type Lowered a = OrdBy Up (Maybe a)
Regards,
apfelmus
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Signature for non-empty filter
On Wed, 6 Feb 2008, Bulat Ziganshin wrote: Hello Henning, Wednesday, February 6, 2008, 5:09:56 PM, you wrote: Is Haskell's type system including extensions strong enough for describing a function, that does not always return a trivial value? E.g. (filter (\x - x==1 x==2)) such things may be detected by (too) smart compiler, but in general it's undecidable: filter (if LifeHasMeaning then const True else odd) ;) As I said, if the programmer could specify an input on the type level for which the output is non-trivial, then this would solve the problem. it's another question: you can describe trivial values using type system, but can't prohibit them using it - it's impossible because you can't check for arbitrary algorithm whether it will be finally stopped I could consider the function buggy, if it does not terminate on the given example. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] classes for data structures
Matthew Pocock wrote: Hi, I've been working a lot with maps, sets and lists. While the process of getting things out of them is abstracted by foldable, traversable and friends, the process of building one up is not. Would it be possible to have something like: class Buildable b where empty :: b a --makes an empty b with elements of type a insert :: a - b a - b a --inserts the new element into the buildable Another approach uses : singleton :: a - b a and then just mappend :: b a - b a - b a i.e. make b a into a Monoid. singleton = pure = return, if there happens to be a Monad/Applicative instance around. And indeed there *will* be a Monad, if there is a sensible way of defining concat :: b (b a) - b a, which there probably is. Jules ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] classes for data structures
On Feb 6, 2008 9:40 AM, Henning Thielemann
[EMAIL PROTECTED] wrote:
On Wed, 6 Feb 2008, Denis Bueno wrote:
On Feb 6, 2008 9:00 AM, Henning Thielemann
[EMAIL PROTECTED] wrote:
On Wed, 6 Feb 2008, Matthew Pocock wrote:
class Buildable b where
empty :: b a --makes an empty b with elements of type a
insert :: a - b a - b a --inserts the new element into the buildable
How can this interface be used both for lists and maps? [...]
One solution is to change the class slightly:
class Buildable t x where
empty :: t
insert :: x - t - t
instance Buildable (Map k a) (k, a) where
empty = Map.empty
insert = uncurry Map.insert
ok, maybe with functional dependency t - x
I'm not sure about that. It's often convenient to have two instances,
one like the one I gave above, and others involving something that
embeds a key-value pair:
type SomethingWithKV k a = KV {getKV :: (k, a)}
instance Buildable (Map k a) (SomethingWithKV k a) where
empty = Map.empty
insert s m = uncurry Map.insert (getKV s) m
I have done this before -- it's very convenient, and I think makes the
code that uses empty and insert more robust, and easier to read.
--
Denis
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] classes for data structures
On Wed, 6 Feb 2008, Denis Bueno wrote:
On Feb 6, 2008 9:40 AM, Henning Thielemann
ok, maybe with functional dependency t - x
I'm not sure about that. It's often convenient to have two instances,
one like the one I gave above, and others involving something that
embeds a key-value pair:
type SomethingWithKV k a = KV {getKV :: (k, a)}
instance Buildable (Map k a) (SomethingWithKV k a) where
empty = Map.empty
insert s m = uncurry Map.insert (getKV s) m
I have done this before -- it's very convenient, and I think makes the
code that uses empty and insert more robust, and easier to read.
But why do you want to have the special type SomethingWithKV, but not
MapSomething ?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] classes for data structures
On Feb 6, 2008 10:36 AM, Henning Thielemann
[EMAIL PROTECTED] wrote:
type SomethingWithKV k a = KV {getKV :: (k, a)}
instance Buildable (Map k a) (SomethingWithKV k a) where
empty = Map.empty
insert s m = uncurry Map.insert (getKV s) m
I have done this before -- it's very convenient, and I think makes the
code that uses empty and insert more robust, and easier to read.
But why do you want to have the special type SomethingWithKV, but not
MapSomething ?
Do you mean a map that maps SomethingWithKV to whatever, instead of k to v?
My point is that if you add the functional dependency, you can't write
instances for types which wrap what you're really interested in. You
have to manually unwrap those types everywhere they interact with a
map. This is tedious and error-prone. Being able to write such
instances is useful, I think, though not always clearer in all cases.
--
Denis
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Data.Ord and Heaps (Was: Why functional programming matters)
Stephan Friedrichs wrote:
I'm sorry it took me so long to respond!
No worries :)
In conclusion: the ordering policy stuff should not be part of
Data.Heap, this is a job for Data.Ord.
This sounds really useful. How about you propose
this to the base-package maintainers? :)
What, me? :D
Where? :)
Proposals for the base package go to [EMAIL PROTECTED] . A
proposal is a darcs patch + a deadline. Unfortunately, ghc 6.8.* isn't
yet available on Macports, I'd have to install 6.6.1 again on my wiped
disk to get a haskell compiler and darcs.
I'm currently leaning towards code like
data OrdBy p a = OrdBy { unOrdBy :: a }
instance Eq a = Eq (OrdBy p a) where
(==) = (==) `on` unOrdBy
data Reverse
type Reversed a = OrdBy Reverse a
instance Ord a = Ord (OrdBy Reverse a) where
compare = flip $ comparing unOrdBy
and probably another example for custom orderings. Do you now a good one?
I'm not so happy about the names. In particular, I don't like unOrdBy ,
too much cAmelCase. Any other ideas? Maybe
data Rearrange p a = Rearrange { unRearrange :: a }
data ReOrd p a = ReOrd { unReOrd :: a }
But I guess it can't be helped and it's not too bad either.
The class constraint
Ord (OrdBy p a) =
will be common in user code, but it's a bit bulky for my taste. However,
its main problem is that it's not Haskell98 :( A multi-parameter class
(just like in the original heap-0.1)
class OrdPolicy p a where ...
instance OrdPolicy p a = Ord (OrdBy p a) where ...
is shorter but not H98 either. The name could be a mot juste, too.
class Rearranged p a where ...
class Ord' p a where ...
class OrdBy p a where ... -- clashes with the name of the type
Regards,
apfelmus
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] classes for data structures
On Wed, 6 Feb 2008, Denis Bueno wrote:
On Feb 6, 2008 10:36 AM, Henning Thielemann
[EMAIL PROTECTED] wrote:
type SomethingWithKV k a = KV {getKV :: (k, a)}
instance Buildable (Map k a) (SomethingWithKV k a) where
empty = Map.empty
insert s m = uncurry Map.insert (getKV s) m
I have done this before -- it's very convenient, and I think makes the
code that uses empty and insert more robust, and easier to read.
But why do you want to have the special type SomethingWithKV, but not
MapSomething ?
Do you mean a map that maps SomethingWithKV to whatever, instead of k to v?
I mean a Map that is specialised for storing SomethingWithKV instead of
plain pairs. (If I imagine a Map as a list of pairs that is optimized for
efficiency.)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
On Feb 6, 2008 1:18 AM, Jonathan Cast [EMAIL PROTECTED] wrote: On 5 Feb 2008, at 10:14 PM, Jeff φ wrote: On Feb 5, 2008 4:58 PM, Chaddaï Fouché [EMAIL PROTECTED] wrote: 2008/2/5, Jeff φ [EMAIL PROTECTED]: This is interesting. I've been programming in Concurrent Clean for a while. Instead of monads, Clean supports unique types for mutable arrays and IO. In Clean, I can write code that iterates through a mutable array by converting it to a lazy list. This is convenient because I can use all the nice list processing functions that are available. You could absolutely write something like that in Haskell, but as some have pointed out, this is probably _not a Good Idea_, even though it works in your particular case, the array could be modified between the time you get the lazy list and the time you actually read it... And there's no way to insure it's not happening in Haskell, and I strongly doubt there is in Concurrent Clean, could you confirm ? Concurrent Clean can handle this in a safe way. Here's a code snippet for normalize_2D_ary from ArrayTest.icl: uToList_2D :: *(a u:(b c)) - (.[c],*(a u:(b c))) | Array a (b c) Array b c map_in_place_2d_arr :: (a - a) *(b *(c a)) - *(b *(c a)) | Array b (c a) Array c a normalize_2D_ary :: *(a *(b c)) - *(a *(b c)) | Array a (b c) Array b c / c Ord c normalize_2D_ary ary = let (lst,ary2) = uToList_2D ary max_elem = foldl1 max lst in map_in_place_2d_arr (\ x - x / max_elem) ary2 uToList_2D takes a unique array, ary, and returns a tuple containing a list of the array elements and a new array, ary2. uToList_2D does not modify ary, but Clean's type system forces any function that accesses a unique array to thread the array through and return a new array. Under the hood the new array actually uses the same memory storage as the original array. So, it is effecient. Threading the array serializes access insuring the array won't be modified until the list is complete. I'm confused --- does uToList_2D return the head of the list before or after it finishes reading the array? If before, then I don't see how the type system prevents me from modifying the array before I finish examining the list, as you claim. If after, then the list isn't truly lazy. uToList_2D can return the head of the list before it finishes reading the array. I could modify the code so that it is ambiguous whether the array is modified before the list processing is finished. normalize_2D_ary ary = let (lst,ary2) = uToList_2D ary max_elem = foldl1 max lst in map_in_place_2d_arr (\ x - x / max_elem) ary // I changed ary2 to ary However, the type system will generate an error with this code because ary is no longer unique because it is referenced in two expressions. Clean produces this error message: Uniqueness error [ArrayTest.icl,55,normalize_2D_ary]: ary demanded attribute cannot be offered by shared object I should mention that a problem with the code I've shown is that it is very sensitive to the order in which the expression graph is evaluated. Simple changes can cause lst to become strict and the program to run out of heap. By the way, Clean has it's share of rough edges. The reason I'm hanging out on Haskell-Cafe is because I'm trying to get away from those rough edges. But, I am missing Clean's uniqueness types. I'm starting to see Haskell's unsafe functions as a blunt work around that could be fixed elegantly and safely by implementing uniqueness types. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
jeff1.61803: On Feb 6, 2008 1:18 AM, Jonathan Cast [EMAIL PROTECTED] wrote: On 5 Feb 2008, at 10:14 PM, Jeff I* wrote: On Feb 5, 2008 4:58 PM, ChaddaA- FouchA(c) [EMAIL PROTECTED] wrote: 2008/2/5, Jeff I* [EMAIL PROTECTED]: This is interesting. I've been programming in Concurrent Clean for a while. Instead of monads, Clean supports unique types for mutable arrays and IO. In Clean, I can write code that iterates through a mutable array by converting it to a lazy list. This is convenient because I can use all the nice list processing functions that are available. You could absolutely write something like that in Haskell, but as some have pointed out, this is probably _not a Good Idea_, even though it works in your particular case, the array could be modified between the time you get the lazy list and the time you actually read it... And there's no way to insure it's not happening in Haskell, and I strongly doubt there is in Concurrent Clean, could you confirm ? Concurrent Clean can handle this in a safe way. Here's a code snippet for normalize_2D_ary from ArrayTest.icl: uToList_2D :: *(a u:(b c)) - (.[c],*(a u:(b c))) | Array a (b c) Array b c map_in_place_2d_arr :: (a - a) *(b *(c a)) - *(b *(c a)) | Array b (c a) Array c a normalize_2D_ary :: *(a *(b c)) - *(a *(b c)) | Array a (b c) Array b c / c Ord c normalize_2D_ary ary = let (lst,ary2) = uToList_2D ary max_elem = foldl1 max lst in map_in_place_2d_arr (\ x - x / max_elem) ary2 uToList_2D takes a unique array, ary, and returns a tuple containing a list of the array elements and a new array, ary2. uToList_2D does not modify ary, but Clean's type system forces any function that accesses a unique array to thread the array through and return a new array. Under the hood the new array actually uses the same memory storage as the original array. So, it is effecient. Threading the array serializes access insuring the array won't be modified until the list is complete. I'm confused --- does uToList_2D return the head of the list before or after it finishes reading the array? If before, then I don't see how the type system prevents me from modifying the array before I finish examining the list, as you claim. If after, then the list isn't truly lazy. uToList_2D can return the head of the list before it finishes reading the array. I could modify the code so that it is ambiguous whether the array is modified before the list processing is finished. normalize_2D_ary ary = let (lst,ary2) = uToList_2D ary max_elem = foldl1 max lst in map_in_place_2d_arr (\ x - x / max_elem) ary // I changed ary2 to ary However, the type system will generate an error with this code because ary is no longer unique because it is referenced in two expressions. Clean produces this error message: Uniqueness error [ArrayTest.icl,55,normalize_2D_ary]: ary demanded attribute cannot be offered by shared object I should mention that a problem with the code I've shown is that it is very sensitive to the order in which the expression graph is evaluated. Simple changes can cause lst to become strict and the program to run out of heap. By the way, Clean has it's share of rough edges. The reason I'm hanging out on Haskell-Cafe is because I'm trying to get away from those rough edges. But, I am missing Clean's uniqueness types. I'm starting to see Haskell's unsafe functions as a blunt work around that could be fixed elegantly and safely by implementing uniqueness types. That's a reasonable critique : its hard to enforce uniqueness, in the type system in Haskell, -- I'd be interesting to see approaches that avoid extending the compiler. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Mutable arrays
That's a reasonable critique : its hard to enforce uniqueness, in the type system in Haskell, -- I'd be interesting to see approaches that avoid extending the compiler. Isn't the compiler already modified in a way to deal with the RealWorld type that is used in the IO monad? Surely the RealWorld is unique... Regards, Peter Verswyvelen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
On Feb 6, 2008, at 12:12 , Peter Verswyvelen wrote: That's a reasonable critique : its hard to enforce uniqueness, in the type system in Haskell, -- I'd be interesting to see approaches that avoid extending the compiler. Isn't the compiler already modified in a way to deal with the RealWorld type that is used in the IO monad? Surely the RealWorld is unique... You might want to look at the definition of unsafePerformIO before asserting that. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [EMAIL PROTECTED] system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED] electrical and computer engineering, carnegie mellon universityKF8NH ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
On Feb 6, 2008, at 12:23 , Brandon S. Allbery KF8NH wrote: You might want to look at the definition of unsafePerformIO before asserting that. On second thought I think I haven't had enough sleep to claim anything of the sort with any confidence. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [EMAIL PROTECTED] system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED] electrical and computer engineering, carnegie mellon universityKF8NH ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
Hi Isn't the compiler already modified in a way to deal with the RealWorld type that is used in the IO monad? Surely the RealWorld is unique... No. The monad and the primitive operations ensure it is unique, the IO monad is abstracted away properly, and it all works neatly so you can't violate the uniqueness. However, the realWorld thing is not actually unique, for example unsafeInterleaveIO and unsafePerformIO violate this. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Mutable arrays
Yeah, I also believed that, but then I'm confused: Don Stewart wrote: That's a reasonable critique : its hard to enforce uniqueness, in the type system in Haskell, -- I'd be interesting to see approaches that avoid extending the compiler. Neil Mitchell wrote: No. The monad and the primitive operations ensure it is unique, the IO monad is abstracted away properly, and it all works neatly so you can't violate the uniqueness. So monads *do* enforce uniqueness... So what is the difference between Haskell's monad approach and Clean's uniqueness typing? I always thought these were just two different ways to tackle the same problem, and I had the feeling Haskell's approach was actually more general. Thanks, Peter -Original Message- From: Neil Mitchell [mailto:[EMAIL PROTECTED] Sent: Wednesday, February 06, 2008 6:25 PM To: Peter Verswyvelen Cc: Don Stewart; Jeff φ; haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] Mutable arrays Hi Isn't the compiler already modified in a way to deal with the RealWorld type that is used in the IO monad? Surely the RealWorld is unique... No. The monad and the primitive operations ensure it is unique, the IO monad is abstracted away properly, and it all works neatly so you can't violate the uniqueness. However, the realWorld thing is not actually unique, for example unsafeInterleaveIO and unsafePerformIO violate this. Thanks Neil -- No virus found in this incoming message. Checked by AVG Free Edition. Version: 7.5.516 / Virus Database: 269.19.20/1261 - Release Date: 2/5/2008 8:57 PM ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
On Feb 6, 2008 4:32 AM, Bjorn Buckwalter [EMAIL PROTECTED] wrote: Well, could you elaborate a little on joining efforts? The effort I was planning to invest in my package consists mainly of creating a .cabal file plus some logistics to get tarballs to where they have to be. I understand that you (and Wolfgang) are creating a library of type level decimals for the purpose of constraining vector (list?) lengths. After that I haven't been paying attention fully to the thread. Is the goal to create a general-purpose library for type-level programming and my module would fit into that grander scheme? Yes,the idea is to create a Cabal-ready wide-scope type-level programming library, joining the operations implemented in the different type-level libraries which are around. The goal (or at least mine) is to provide a common reusable type-level library which saves constantly reinventing the wheel. I'll provide an initial implementation (just including naturals in decimal representation) soon. Wolfgang suggested adding booleans at a later point too if I recall properly. Any useful type-level operation should have a place in the library. Or did you have something else in mind with joining efforts? E.g. help reviewing your code or writing new code? This would certainly help too. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] Extensible records: Static duck typing
[redirecting to haskell-cafe] On 2/6/08, Barney Hilken [EMAIL PROTECTED] wrote: This is what I was trying to do with the wiki page. I stopped because the only other contributor decided he could no longer contribute, and I felt I was talking to myself. If we want to be rational about the design, we need real examples to demonstrate what is genuinely useful, and I don't have that many of them. It's obvious that records are a language feature that people besides just you care about. And so everybody would benefit from your effort if you chose to continue adding more examples to the wiki page. Records clearly seem to be an important issue if so many people have replied to your thread, and your comment expressing frustration at arbitrary decisions getting made about design seems to suggest you have some passion about the issue. On the other hand, if you can't think of real examples offhand, and no one else can either, maybe it's not that important... (Examples don't have to be very complicated to be useful, by the way. Simpler is better.) Cheers, Tim -- Tim Chevalier * http://cs.pdx.edu/~tjc * Often in error, never in doubt If pots couldn't call kettles black, there'd be a lot less talking going on. -- Larissa Ranbom ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
On 2/6/08, Peter Verswyvelen [EMAIL PROTECTED] wrote: Yeah, I also believed that, but then I'm confused: So monads *do* enforce uniqueness... So what is the difference between Haskell's monad approach and Clean's uniqueness typing? I always thought these were just two different ways to tackle the same problem, and I had the feeling Haskell's approach was actually more general. IO and mutable array monads could be implemented on top of Clean's unique arrays and world objects. So, I'd argue that Clean is at least as general as Haskell. On the other hand, I've posted two similar problems to this list. In Haskell I want to . . . 1) turn a mutable array into a lazy list 2) turn the contents of a file into a lazy list The responses I've received are typically: 1) Use unsafeFreeze / unsafeThaw 2) Use hGetContents. (which uses unsafePeformIO under the hood.) 3) Don't use a lazy list. Rewrite the code to break the data up into smaller chunks and process the chunks in a loop. I have solved both of these problems in Clean using a lazy list without resorting to unsafe operations. So, it seems to me that uniqueness types are more general than monads. By the way, I'm not good enough to use unsafe functions. My code would crash for sure. :-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
Bas van Dijk wrote: The following obviously doesn't work: import Control.Monad.Error inv :: MonadError e m = m a - m () inv m = (m fail ) `catchError` \_ - (return ()) What about this? inv :: MonadError e m = m a - m () inv m = join $ (m return mzero) `catchError` \_ - return (return ()) Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] classes for data structures
Am Mittwoch, 6. Februar 2008 16:12 schrieb Jules Bean: And indeed there *will* be a Monad, if there is a sensible way of defining concat :: b (b a) - b a, which there probably is. Not with sets. “concat” on Set would have type Ord a = Set (Set a) - Set a instead of Set (Set a) - Set a. Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
jeff1.61803: On 2/6/08, Peter Verswyvelen [EMAIL PROTECTED] wrote: Yeah, I also believed that, but then I'm confused: So monads *do* enforce uniqueness... So what is the difference between Haskell's monad approach and Clean's uniqueness typing? I always thought these were just two different ways to tackle the same problem, and I had the feeling Haskell's approach was actually more general. IO and mutable array monads could be implemented on top of Clean's unique arrays and world objects. So, I'd argue that Clean is at least as general as Haskell. On the other hand, I've posted two similar problems to this list. In Haskell I want to . . . 1) turn a mutable array into a lazy list 2) turn the contents of a file into a lazy list The responses I've received are typically: 1) Use unsafeFreeze / unsafeThaw 2) Use hGetContents. (which uses unsafePeformIO under the hood.) 3) Don't use a lazy list. Rewrite the code to break the data up into smaller chunks and process the chunks in a loop. I have solved both of these problems in Clean using a lazy list without resorting to unsafe operations. So, it seems to me that uniqueness types are more general than monads. They solve a specific issue in the type system that goes statically unchecked. Monads are a separate issue (and kind of a non-sequitor here). Uniquness doesn't give you more than the IO monad. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
2008/2/6, Jeff φ [EMAIL PROTECTED]: I have solved both of these problems in Clean using a lazy list without resorting to unsafe operations. So, it seems to me that uniqueness types are more general than monads. Are you aware that your code in Clean has some issues, like the lst not being so lazy if you operate on ary2 before you operate on lst (it is completely put in memory in this case) ? You've effectively created a big uncertainty on the space taken by your function. Is this ok with you ? The monadic fold (like I and some others proposed) guarantee you a constant amount of memory consumed and is perfectly safe too, is the Clean solution really so much better ? Jonathan Cast : I'm confused --- does uToList_2D return the head of the list before or after it finishes reading the array? If before, then I don't see how the type system prevents me from modifying the array before I finish examining the list, as you claim. If after, then the list isn't truly lazy. What happens here is that the array can't be modified without evaluating ary2 and ary2 can't be evaluated without completely evaluating the list before, so you effectively get the list lazily as long as you don't touch ary2 before touching the list, and you can't damage the list by modifying the array (because in this case, lst would be completely evaluated in the first place). You can do the same in Haskell in fact, but you'll need to discipline yourself to evaluate the witness before modifying the array. So uniqueness here seems to have an advantage over monads, still, the monads look much cleaner (sic) than Clean code with all those unique value passing around... -- Jedaï ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Mutable arrays
I see. Unfortunately I did not spent enough time playing with Clean, and I'm still learning Haskell, so I can't give any feedback on your questions J Now from the little time I've spent in the company of Clean, I must say there's another advantage of uniqueness typing: it is very easy to understand. While monads are a tiny bit more demanding! But monads give such a mental satisfaction once you see the light ;-) So you say uniqueness typing might be more general. Can one make list monads and all the other funky Haskell monads with Clean's uniqueness typing then? Peter From: Jeff φ [mailto:[EMAIL PROTECTED] Sent: woensdag 6 februari 2008 20:21 To: Peter Verswyvelen; Neil Mitchell; Don Stewart Cc: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] Mutable arrays On 2/6/08, Peter Verswyvelen [EMAIL PROTECTED] wrote: Yeah, I also believed that, but then I'm confused: So monads *do* enforce uniqueness... So what is the difference between Haskell's monad approach and Clean's uniqueness typing? I always thought these were just two different ways to tackle the same problem, and I had the feeling Haskell's approach was actually more general. IO and mutable array monads could be implemented on top of Clean's unique arrays and world objects. So, I'd argue that Clean is at least as general as Haskell. On the other hand, I've posted two similar problems to this list. In Haskell I want to . . . 1) turn a mutable array into a lazy list 2) turn the contents of a file into a lazy list The responses I've received are typically: 1) Use unsafeFreeze / unsafeThaw 2) Use hGetContents. (which uses unsafePeformIO under the hood.) 3) Don't use a lazy list. Rewrite the code to break the data up into smaller chunks and process the chunks in a loop. I have solved both of these problems in Clean using a lazy list without resorting to unsafe operations. So, it seems to me that uniqueness types are more general than monads. By the way, I'm not good enough to use unsafe functions. My code would crash for sure. :-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
Peter Verswyvelen wrote:
So monads *do* enforce uniqueness... So what is the difference between
Haskell's monad approach and Clean's uniqueness typing? I always thought
these were just two different ways to tackle the same problem, and I had the
feeling Haskell's approach was actually more general.
Yes (1), and no (2).
! Long pedantic post follows
(1)
They are two different ways to tackle the same problem: how to have
I/O in a pure functional language when I/O neccessarily requires the
world state to be destructively updated (e.g. we can't copy the entire
filesystem, or the (truly) global internet state).
The solution is based on the following observation: imagine we
a have a large datastructure (e.g. big tree) and a function that
updates it, then, *in general*, pure functional semantics requires the
implementation to return a copy of its argument with the update applied,
leaving the original argumment intact.
However, if in a given program, we know that the old value of the
big structure is never referenced once the function is applied,
then we can *implement* the function application under the hood
as a true destructive update, without breaking the pure referential
semantics of the language.
Such a use of a structure in a program is said to single-threaded.
For example, the program
f (g (h bigThing))
makes single-threaded use of bigThing, so *in this program*,
we could implement f, g and h using destructive update without altering
the outcome as predicted by a copy semantics.
However, the program
(bigThing,h bigThing)
does not have a single-threaded use of bigThing, so h *must* be
implemented using copying, because we have access to both values.
The upshot of all of this is that a program that restricts itself
to single-threaded use of a (large) structure can use a desctructive
implementation, so if we can ensure that our patterns of I/O access
are single-threaded, then we can:
- implement I/O as we must, i.e with destructive update
- yet still maintain the illusion that our program is pure (copying).
What's the catch? Well, in general, the question of wether or not
a given structure's use is single-threaded, is undecidable. So what
we have are two (partial) solutions: Clean's uniqueness types, and
Haskell's monads.
Let us assume that the entire I/O state is captured by
a variable world :: World
Invent-and-Verify: Clean allows you to write a program that
explicity mentions world, and the uses the type-system to check
that accesses to world are single-threaded. Essentially the
destructive functions have type annotations that insist
their World arguments and results are singly-threaded (a.k.a. unique).
So program
writefile a.dat Text A (writefile b.dat Text B world)
typechecks, but program
(world,writefile b.dat Text B world)
doesn't.
Because of undecidability, the type-checker is not totally accurate,
but behaves conservatively, so may report a program as ill-typed,
even if it is actually single-threaded, but will always spot
a program that is truly bad - not single-threaded.
Correctness-by-Construction: Haskell approaches the problem by hiding
the world inside an abstract data-type called a monad. Haskell programs
do not mention the world explicitly at all. The monad, with its return,
bind and basic monadic I/O operations is setup so that the hidden world
state is always accessed in a single-threaded fashion,so the underlying
implementation is free to use desctructive update.
So we can write a monadic form of the first program above, as
do writefile b.dat Text B
writefile a.dat Text A
We cannot begin to express the second (ill-typed) program at all !
(2)
Leaving aside the fact that the monad concept is more general than just
I/O (Maybe monad, List monad, etc..),
we can state categorically that as far as I/O is concerned, that Clean's
uniqueness type approach is more general than Haskell's monads, i.e.:
- any Haskell monad-IO program can be re-written as a correctly typed
Clean IO program (simply implement the IO monad as a state monad
over a state world :: World).
- not all Clean IO programs can be directly written in monadic style.
The issue has to do with the fact that the IO monad over-sequences
IO actions, because the monad encapsulates the entire world in one
lump.
(see slides 37/38 of
http://research.microsoft.com/~simonpj/papers/haskell-retrospective/HaskellRetrospective.pdf).
So if we have two functions, one, f1 :: IO (), reading from file
f1.in and writing to f1.out, and the other, f2 :: IO () reading
from f2.in and writing to f2.out, we must decide as programmers
what order to use - either do{ f1 ; f2 } or do { f2; f1 }.
If we generalise to f1 .. fn, we have to sequence these,
which is why the function in Haskell of type [IO a] - IO [a], is called
sequence.
In Clean, we not only have explicit access to the world, but
we can partition it. Simplifying somewhat, we could open up
pairs of file-handle (f1.in,f1.out),
Re[3]: [Haskell-cafe] Signature for non-empty filter
Hello Henning, Wednesday, February 6, 2008, 6:09:28 PM, you wrote: it's another question: you can describe trivial values using type system, but can't prohibit them using it - it's impossible because you can't check for arbitrary algorithm whether it will be finally stopped I could consider the function buggy, if it does not terminate on the given example. it's impossible to check for *arbitrary* function call whether it will be terminated. seems that you don't have formal CS education? :) so one can develop set of functions that are guaranteed to be terminated or guaranteed to be non-trivial. but it's impossible to check for arbitrary function whether it's trivial and even whether it will terminate for particular data this means that answer to original question - one can ensure that argument for filter is non-terminating function only if these functions are written using some special notation which doesn't allow to write arbitrary turing-complete algorithms -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
Peter Verswyvelen wrote: So you say uniqueness typing might be more general… Can one make list monads and all the other funky Haskell monads with Clean’s uniqueness typing then? As my long post pointed out - as far IO is concerned, Clean is more general than Haskell (less over-sequencing). However in a general setting, monads are very general, much more so than Clean's I/O uniqueness types. Monads capture a fundamental pattern of sequential side-effecting computation in a pure referentially transparent way - IO is just a specific instance of this. Having said that, it's worth noting that list and maybe monads can be introduced in Clean, but these would have nothing to do with the I/O infrastructure in that language. -- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Foundations and Methods Research Group Director. Department of Computer Science, Room F.13, O'Reilly Institute, Trinity College, University of Dublin, Ireland. http://www.cs.tcd.ie/Andrew.Butterfield/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is this so inefficient?
Jefferson Heard wrote: I thought this was fairly straightforward, but where the marked line finishes in 0.31 seconds on my machine, the actual transpose takes more than 5 minutes. I know it must be possible to read data in [snip] dataFromFile :: String - IO (M.Map String [S.ByteString]) dataFromFile filename = do f - S.readFile filename print . length . map (S.split ',' $!) . S.lines $ f -- finishes in 0.31 seconds The S.split applications will never be evaluated - the list that you produce is full of thunks of the form (S.split ',' $! some bytestring) The $! will only take effect if those thunks are forced, and length doesn't do that. Try print . sum . map (length . S.split ',') . S.lines $ f instead, to force S.split to produce a result. (In fact, S.split is strict in its second argument, so the $! shouldn't have any effect on the running time at all. I didn't measure that though.) return . transposeCSV . map (S.split ',' $!) . S.lines $ f -- this takes 5 minutes and 6 seconds HTH, Bertram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[3]: [Haskell-cafe] Signature for non-empty filter
On Wed, 6 Feb 2008, Bulat Ziganshin wrote: Hello Henning, Wednesday, February 6, 2008, 6:09:28 PM, you wrote: it's another question: you can describe trivial values using type system, but can't prohibit them using it - it's impossible because you can't check for arbitrary algorithm whether it will be finally stopped I could consider the function buggy, if it does not terminate on the given example. it's impossible to check for *arbitrary* function call whether it will be terminated. seems that you don't have formal CS education? :) so one can develop set of functions that are guaranteed to be terminated or guaranteed to be non-trivial. but it's impossible to check for arbitrary function whether it's trivial and even whether it will terminate for particular data If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Signature for non-empty filter
On Tue, 5 Feb 2008, Dan Licata wrote: [CC'ed to the agda mailing list as well] On Feb05, Henning Thielemann wrote: Is Haskell's type system including extensions strong enough for describing a function, that does not always return a trivial value? E.g. (filter (\x - x==1 x==2)) will always compute an empty list. Using an appropriate signature for the function it shall be rejected at compile time, because it is probably a mistake - probably (filter (\x - x==1 || x==2) xs) was meant. I assume that the type must contain somehow an example input for which the function value is non-trivial. If Haskell's type system is not strong enough, what about dependently typed languages like Cayenne or Epigram? (I know, theorem provers have no problem with such types.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe You can definitely do this with dependent types. Here's a way to do it in Agda 2: Thanks for your detailed answer! I don't fully understand the Agda code, but I record that there is another system which allows such kind of types. Now, 'filter' was a particular example where the type constraint can be reformulated as constraint on the element test 'f'. However there might be a composed function like stupidFilter = filter odd . map (2*) I assume that Agda lets me forbid such functions by properly designed types, too. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
On Feb 6, 2008 8:27 PM, Tillmann Rendel [EMAIL PROTECTED] wrote: What about this? inv :: MonadError e m = m a - m () inv m = join $ (m return mzero) `catchError` \_ - return (return ()) Beautiful! That's the one I'm looking for! I was already defining a 'MonadInvert' class and a bunch of instances like below but this is a much more flexible solution. - -- | A Monad that supports inversion. -- Turning success into failure and failure into success. class Monad m = MonadInvert m where -- | @invert m@ fails when @m@ is successfull (returns a value) -- and returns @()@ when @m@ fails . invert :: m a - m () instance MonadInvert Maybe where invert Nothing = Just () invert (Just _) = Nothing instance MonadInvert [] where invert []= [()] invert (_:_) = [] instance E.Error e = MonadInvert (Either e) where invert (Left _) = Right () invert (Right _) = Left E.noMsg instance (E.Error e, MonadInvert m) = MonadInvert (E.ErrorT e m) where invert = T.lift . invert . E.runErrorT instance MonadInvert m = MonadInvert (S.StateT st m) where invert m = S.StateT $ \s - (invert $ S.runStateT m s) = \u - return (u, s) ... - Thanks very much. Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Signature for non-empty filter
On Wednesday 06 February 2008, Henning Thielemann wrote: If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok. Can't fault this logic. The problem is that you may have to wait quite a long time to discover this non-termination. Matthew ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
On Wed, Feb 06, 2008 at 08:57:43PM +, Andrew Butterfield wrote: In Clean, we not only have explicit access to the world, but we can partition it. Simplifying somewhat, we could open up pairs of file-handle (f1.in,f1.out), (f2.in,f2,out) ... (fn.in,fn.out), which does have to be done sequentially, since each file opening modifies the (global) filesystem. However, once this is done, we could, in principle, execute the fn in any order, and indeed in such a way that the implementation could choose to do them in parallel - this potential for (admittedly limited) deterministic parallel execution of I/O actions is possible with uniqueness types, but not epxressible in the monadic world as currently formulated. What if f1.out is a symlink to f2.out? I don't think Clean satisfies the evaluation order independance that is so treasured here. Stefan signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
On 2/6/08, Chaddaï Fouché [EMAIL PROTECTED] wrote: 2008/2/6, Jeff φ [EMAIL PROTECTED]: I have solved both of these problems in Clean using a lazy list without resorting to unsafe operations. So, it seems to me that uniqueness types are more general than monads. Are you aware that your code in Clean has some issues, like the lst not being so lazy if you operate on ary2 before you operate on lst (it is completely put in memory in this case) ? You've effectively created a big uncertainty on the space taken by your function. Is this ok with you ? Yes, I'm aware of this. In a previous post, I wrote, I should mention that a problem with the code I've shown is that it is very sensitive to the order in which the expression graph is evaluated. Simple changes can cause lst to become strict and the program to run out of heap. However, I think your description of this issue is much more succinct than mine. I'm not sure, but I _think_ this problem can be solved using Clean's strict let-before notation. normalize_2D_ary ary = # (lst,ary) = uToList_2D ary #! max_elem = foldl1 max lst // max_elem is strict -- lst is consumed. = map_in_place_2d_arr (\ x - x / max_elem) ary The monadic fold (like I and some others proposed) guarantee you a constant amount of memory consumed and is perfectly safe too, is the Clean solution really so much better ? I'm looking forward to spending a few free hours this weekend playing with the monadic fold code. I've written a lot of image processing code in Clean that treats images as lists of RGBA tuples. It's a very useful abstraction. But, I've spent more time than I care to admit fixing unexpected stack and heap overflows that were caused by seemingly unrelated code change. I hope to find other abstractions that aren't so fragile. Peter Verswyvelen [EMAIL PROTECTED] wrote: Now from the little time I've spent in the company of Clean, I must say there's another advantage of uniqueness typing: it is very easy to understand. While monads are a tiny bit more demanding! But monads give such a mental satisfaction once you see the light ;-) For me, the light is a faint distant flicker. I hope to see it clearer someday. At the risk of starting a flame war, being labeled a troll, having Godwin's law invoked, and suffering a life time ban from Haskell-Cafe, I'd like to broach another subject. I noticed that GHC implements mutable arrays in the IO monad. This seems odd to me. Arrays aren't related to IO. Are there obstacles to mixing code that uses IO monads and array monads that are most easily worked around by sticking mutable arrays into the IO monad? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Signature for non-empty filter
Am Mittwoch, 6. Februar 2008 18:39 schrieb Bulat Ziganshin: […] this means that answer to original question - one can ensure that argument for filter is non-terminating function only if these functions are written using some special notation which doesn't allow to write arbitrary turing-complete algorithms And this is exactly what Agda, Epigram, Coq, etc. do. Note however that those systems are not very restrictive. It’s possible, for example, to define Ackermann’s function in Agda: module Ackermann where data Nat : Set where O : Nat ↑_ : Nat - Nat ackermann : Nat - Nat - Nat ackermann Om= ↑ m ackermann (↑ n) O= ackermann n (↑ O) ackermann (↑ n) (↑ m) = ackermann n (ackermann (↑ n) m) Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
G'day all. On Feb 6, 2008 12:45 PM, Felipe Lessa [EMAIL PROTECTED] wrote: I guess your parser is a monad transformer, so *maybe* the solution is to require MonadError from the inner monad. Quoting Bas van Dijk [EMAIL PROTECTED]: Indeed my parser 'P t m a' is a monad transformer. I will try out requiring 'm' to have a 'MonadError' constraint and see how far I come with that. I've occasionally found this useful: class (Monad m) = MonadNegate m where mtrue :: m () mfalse :: m () mnot :: m a - m () mtrue = return () mfalse = fail False Cheers, Andrew Bromage ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
Am Mittwoch, 6. Februar 2008 23:31 schrieb Jeff φ: At the risk of starting a flame war, being labeled a troll, having Godwin's law invoked, and suffering a life time ban from Haskell-Cafe, I'd like to broach another subject. I noticed that GHC implements mutable arrays in the IO monad. This seems odd to me. Arrays aren't related to IO. Are there obstacles to mixing code that uses IO monads and array monads that are most easily worked around by sticking mutable arrays into the IO monad? IO(U)Arrays are only one variant of mutable Array, there are also ST(U)Arrays, which are often preferred. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Signature for non-empty filter
On Feb06, Henning Thielemann wrote:
On Tue, 5 Feb 2008, Dan Licata wrote:
On Feb05, Henning Thielemann wrote:
Is Haskell's type system including extensions strong enough for describing
a function, that does not always return a trivial value? E.g.
(filter (\x - x==1 x==2))
will always compute an empty list. Using an appropriate signature for
the function it shall be rejected at compile time, because it is probably
a mistake - probably (filter (\x - x==1 || x==2) xs) was meant. I assume
that the type must contain somehow an example input for which the function
value is non-trivial. If Haskell's type system is not strong enough, what
about dependently typed languages like Cayenne or Epigram? (I know,
theorem provers have no problem with such types.)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
You can definitely do this with dependent types. Here's a way to do it
in Agda 2:
Thanks for your detailed answer! I don't fully understand the Agda code,
but I record that there is another system which allows such kind of types.
Now, 'filter' was a particular example where the type constraint can be
reformulated as constraint on the element test 'f'. However there might
be a composed function like
stupidFilter = filter odd . map (2*)
I assume that Agda lets me forbid such functions by properly designed
types, too.
I think what you want to say now is not just
(filter f l) is type correct when there is some argument on which f
returns true
but
(filter f l) is type correct when there is some *element of l* on
which f returns true
Here is one way to say this with dependent types:
data SatBy {A : Set} : (A - Bool) - List A - Set where
Here : {f : A - Bool} {x : A} {xs : List A} - Check (f x) - SatBy f (x
:: xs)
There : {f : A - Bool} {x : A} {xs : List A} - SatBy f xs - SatBy f (x
:: xs)
fancyfilter2 : {A : Set} (f : A - Bool) (l : List A) - SatBy f l - List A
fancyfilter2 f l _ = stdfilter f l
The idea is that SatBy f l proves that there is some element of l on
which (f x) is true. 'Here' says that this is true if (f x) is true on
the head of the list; 'There' says that this is true of (x :: xs) if
it's true of xs.
Of course, now to call fancyfilter2, you need to prove this property of
your f and your l. You won't be able to do this for 'odd' and 'map (2*)
x', but you would be able to do this for, e.g., 'even' and 'map (2*) xs
where xs is non-nil'.
-Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Signature for non-empty filter
Hi I think what you want to say now is not just (filter f l) is type correct when there is some argument on which f returns true but (filter f l) is type correct when there is some *element of l* on which f returns true or in Haskell: filterNonEmpty f x = assert (not $ null res) res where res = filter f x If you give that definition to the Catch tool (http://www-users.cs.york.ac.uk/~ndm/catch/) it will try and prove each call is safe. For certain examples, Catch will do the job very well - for example if your filter is something structural like isJust or null. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] parsec3 pre-release [attempt 2]
Probably a weird idea but could this be useful? class (Monad m) = Stream s m t | s - t where uncons :: s - m (m (t,s)) for example: instance (Monad m) = Stream [t] m t where uncons [] = return $ fail uncons [] uncons (t:ts) = return $ return (t,ts) One small advantage is that Streams can have custom error messages when there's no input. Also, using 'uncons' could be as simple as: 'join . uncons'. Bas On Feb 2, 2008 6:15 AM, Derek Elkins [EMAIL PROTECTED] wrote: [Now with 100% more correct darcs get URLs.] I'm currently getting Paolo Martini's Google Summer of Code project, an updated version of Parsec, into a releasable state, and I will be maintaining it for at least a while. Paolo's major additions are: * The Parser monad has been generalized into a Parser monad transformer * The parsers have been generalized to work over a stream of any type, in particular, with bytestrings. I have made a few minor additions as well: * There is Haddock documentation for almost all functions * The Parser monad now has Applicative/Alternative instances Currently, I am looking for people to give it a go reporting any bugs in the library or documentation, troubles building it, or changes/features they would like. I'm also interested in performance information. Most old Parsec code should be relatively easy but not trivial to port. There is a darcs repository on code.haskell.org. If nothing comes up, I'll put a package on Hackage in about a week or so. To get the code: darcs get http://code.haskell.org/parsec3 To build it, the standard cabal commands should work: http://haskell.org/haskellwiki/Cabal/How_to_install_a_Cabal_package Alternatively, you can use the cabal-install application: http://hackage.haskell.org/trac/hackage/wiki/CabalInstall The documentation can be generated also via the normal cabal routine, or via cabal-install. The Text.Parsec modules should be preferred to the Text.ParserCombinators.Parsec modules. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Signature for non-empty filter
Let's be careful here: decidability is only relevant if you want to *automatically* prove calls to filter correct. It is certainly possible to give a type system/specification logic for reasoning about all functions written in a Turing-complete language (e.g., all Haskell functions). In such a type system/logic, you will be able to prove that particular functions have particular results (e.g., that function f over there maps 4 to true). If you give filter the type/specification that Henning wants, you may not be able to get a computer to automatically validate all correct calls to filter, where correct means that I can prove, in the specification logic, that the predicate is satisfiable. However, you can get a computer to validate some calls to filter, and a human may be able to validate others by hand. I.e., it's not necessary to restrict the class of functions you consider if you're willing to give up on full automation. So I disagree with the only if below. -Dan On Feb06, Bulat Ziganshin wrote: Hello Henning, Wednesday, February 6, 2008, 6:09:28 PM, you wrote: it's another question: you can describe trivial values using type system, but can't prohibit them using it - it's impossible because you can't check for arbitrary algorithm whether it will be finally stopped I could consider the function buggy, if it does not terminate on the given example. it's impossible to check for *arbitrary* function call whether it will be terminated. seems that you don't have formal CS education? :) so one can develop set of functions that are guaranteed to be terminated or guaranteed to be non-trivial. but it's impossible to check for arbitrary function whether it's trivial and even whether it will terminate for particular data this means that answer to original question - one can ensure that argument for filter is non-terminating function only if these functions are written using some special notation which doesn't allow to write arbitrary turing-complete algorithms ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
IO(U)Arrays are only one variant of mutable Array, there are also ST(U)Arrays, which are often preferred. I should have worded my question better. The MArray interface is implemented in both the ST and IO monad. A state monad seems like a logical place for mutable arrays. However, I don't understand the motivation for implementing it in IO. Were mutable arrays added to IO because it would be difficult to write code that does both IO and manipulates arrays otherwise? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
On Feb 6, 2008 1:03 PM, Alfonso Acosta [EMAIL PROTECTED] wrote: On Feb 6, 2008 4:32 AM, Bjorn Buckwalter [EMAIL PROTECTED] wrote: I understand that you (and Wolfgang) are creating a library of type level decimals for the purpose of constraining vector (list?) lengths. After that I haven't been paying attention fully to the thread. Is the goal to create a general-purpose library for type-level programming and my module would fit into that grander scheme? Yes,the idea is to create a Cabal-ready wide-scope type-level programming library, joining the operations implemented in the different type-level libraries which are around. The goal (or at least mine) is to provide a common reusable type-level library which saves constantly reinventing the wheel. Ok. Is this what people want -- one big hold-all library with everything, as opposed to smaller more specialized packages? I guess I can see advantages (real or perceived) to both approaches. The other library I use for type-level programming is HList. It has type-level booleans already so you might what to take a look at it if you're not already familiar with it. In fact, if you are serious about creating the de facto(?) type-level programming library trying to get Oleg involved would be very beneficial both in terms of innovation and credibility. Or did you have something else in mind with joining efforts? E.g. help reviewing your code or writing new code? This would certainly help too. I'm sure it would. ;) I didn't mean to imply that I have plenty of spare time to invest in this but I'll certainly be paying attention when you start releasing code. Thanks, Bjorn ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
On Feb 7, 2008 2:30 AM, Bjorn Buckwalter [EMAIL PROTECTED] wrote: Ok. Is this what people want -- one big hold-all library with everything, as opposed to smaller more specialized packages? I guess I can see advantages (real or perceived) to both approaches. Apart from Dockins' typenats library there are no other user-friendly specific type-level libraries that know, so I cannot really tell if people would prefer a hold-all library or a couple of more granular specialized ones. Right now is not hold-all at all (it is still vaporware actually :)), so I think there's no reason to discuss that at this point. Let's see what people think. The other library I use for type-level programming is HList. It has type-level booleans already so you might what to take a look at it if you're not already familiar with it. Thanks I'll have a look at it. In fact, if you are serious about creating the de facto(?) type-level programming library trying to get Oleg involved would be very beneficial both in terms of innovation and credibility. Sure. I've actually been exchanging mail with Oleg. He has given me some useful suggestions and contributed with some code. He didn't mention to what point he wanted to get involved though, but I'm sure he will try to help. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Signature for non-empty filter
On 6 Feb 2008, at 1:54 PM, Matthew Pocock wrote: On Wednesday 06 February 2008, Henning Thielemann wrote: If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok. Can't fault this logic. The problem is that you may have to wait quite a long time to discover this non-termination. I would second this --- letting the compiler go only to discover that it's been running for the last 3 hours because it's diverging seems like a wasted 3 hours. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
On 6 Feb 2008, at 11:56 AM, Chaddaï Fouché wrote:
2008/2/6, Jeff φ [EMAIL PROTECTED]:
I have solved both of these problems in Clean using a lazy list
without
resorting to unsafe operations. So, it seems to me that
uniqueness types
are more general than monads.
Are you aware that your code in Clean has some issues, like the lst
not being so lazy if you operate on ary2 before you operate on lst (it
is completely put in memory in this case) ? You've effectively created
a big uncertainty on the space taken by your function. Is this ok with
you ? The monadic fold (like I and some others proposed) guarantee you
a constant amount of memory consumed and is perfectly safe too, is the
Clean solution really so much better ?
Jonathan Cast :
I'm confused --- does uToList_2D return the head of the list
before or after it finishes reading
the array? If before, then I don't see how the type system
prevents me from modifying the
array before I finish examining the list, as you claim. If after,
then the list isn't truly lazy.
What happens here is that the array can't be modified without
evaluating ary2 and ary2 can't be evaluated without completely
evaluating the list before,
I see. I would agree that Clean's system is more powerful (and
concomitantly more dangerous) in this case.
so you effectively get the list lazily as
long as you don't touch ary2 before touching the list, and you can't
damage the list by modifying the array (because in this case, lst
would be completely evaluated in the first place). You can do the same
in Haskell in fact, but you'll need to discipline yourself to evaluate
the witness before modifying the array.
So uniqueness here seems to have an advantage over monads,
True.
still, the
monads look much cleaner (sic)
Some might argue this.
than Clean code with all those unique
value passing around...
The same thing could be implemented in Haskell, of course:
data MySafeArray a i e = MSA{
touchThisFirst :: IORef (),
realArray :: a i e
}
instance MArray a e IO = MArray (MySafeArray a) e IO where
unsafeRead a i = do
x - readIORef $ touchThisFirst a
eval x
touchThisFirst a `writeIORef` ()
unsafeRead $ realArray a
Then your getContents looks like this:
getArrayElems a = do
x - readIORef $ touchThisFirst a
eval x
ls - get elements unsafely
touchThisFirst a `writeIORef` deepSeq ls
return ls
Ugly, but it can be encapsulated in a library somewhere.
jcc
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
On 6 Feb 2008, at 5:17 PM, Jeff φ wrote: IO(U)Arrays are only one variant of mutable Array, there are also ST (U)Arrays, which are often preferred. I should have worded my question better. The MArray interface is implemented in both the ST and IO monad. A state monad seems like a logical place for mutable arrays. However, I don't understand the motivation for implementing it in IO. Were mutable arrays added to IO because it would be difficult to write code that does both IO and manipulates arrays otherwise? Yes. As I understand it, the reasons are roughly as follows: (a) The ST monad is a fairly clever hack, and is some years (4 or 5?) younger than IO. (b) You can't have an ST-mutable array as a global variable, but you can do this with IO. It's ugly, but some libraries are rumored to require it (see the discussion in http://haskell.org/haskellwiki/ Top_level_mutable_state). (c) In particular, libraries that need to do I/O and/or FFI are rumored to be particularly in need of top-level mutable state, so it's natural to combine the two (or three). (d) It's very difficult to combine monads. Clean's uniqueness types / can/ be combined (as could arbitrary state monads). In general, IMHO what you normally want when combining monads is their coproduct. A general coproduct is quite ugly, but it simplifies nicely in particular cases. Clean, by restricting the problem to combining uniqueness-type-based state monads, can combine monads more easily than Haskell can in the general case. 15 years ago, when these decisions were made, it seemed easier to have a single monad. (e) To a certain extent, IO is the monad in Haskell for `everything other languages can do that we can't'. That's just the nature of the beast; the name IO is simply taken from the most prominent example. So IO's mandate is to do everything C can do better. (f) Some of use consider the IO monad (and mutable arrays in general) deprecated for precisely this reason; the rest seem to want C with a nicer syntax. They use IO, we try to avoid it entirely. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] background question about IO monad
Hi, all, thanks for the responses. I understand the distinction between pure functions and impure functions/procedures/IO actions, it just felt to me in the samples that I quoted that I was in fact starting from basically the starting point, eventually getting to the same endpoint (or at least a pair of endpoints that are not easily distinguished from each other by looking just at code), and inbetween one path was going through liftIO and the other not. But I guess it comes down to the fact that, since I'm in a REPL, I'm wallowing in impurity all the time (or something like that :-) ) regards, Uwe On 2/6/08, Bulat Ziganshin [EMAIL PROTECTED] wrote: Hello Uwe, Wednesday, February 6, 2008, 7:44:27 AM, you wrote: But after that, it sure seems to me as if I've taken data out of the IO monad... this means that you can't use results of IO actions in pure functions. your code works in some transformed version of IO monad, so you don't escaped it if we call pure functions as functions and non-pure ones as procedures, the rule is functions can't call procedures, but all other activity is possible. in your do_action you calls procedure (to format current time) and call a function (to format given time). do_action is procedure (because it works in transformed IO monad), so you don't break any rules -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] background question about IO monad
On 6 Feb 2008, at 7:30 PM, Uwe Hollerbach wrote: Hi, all, thanks for the responses. I understand the distinction between pure functions and impure functions/procedures/IO actions, Um, I'm not sure of that, given what you go on to say. it just felt to me in the samples that I quoted that I was in fact starting from basically the starting point, Not really. The key difference to understand is that between difference between getCurrentTime and toUTCTime 42. These are your `starting points' --- the rest is just pure code. eventually getting to the same endpoint (or at least a pair of endpoints that are not easily distinguished from each other by looking just at code), and inbetween Well, the in-between paths are pure (or can be) either way. It's the starting point that needs liftIO or not. one path was going through liftIO and the other not. But I guess it comes down to the fact that, since I'm in a REPL, I'm wallowing in impurity all the time (or something like that :-) ) jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inverting a Monad
On Feb 6, 2008 6:32 AM, Bas van Dijk [EMAIL PROTECTED] wrote: Is there a way to 'invert' an arbitrary Monad? By 'inverting' I mean to turn success into failure and failure into success. Here are some specific inversions of the Maybe and List Monad: invM :: Maybe a - Maybe () invM Nothing = Just () invM (Just _) = Nothing invL :: [] a - [] () invL []= [()] invL (_:_) = [] How can I define this for an arbitrary Monad m? If you're doing any kind of backtracking or non-determinism, you might consider the msplit operation defined in Backtracking, Interleaving, and Terminating Monad Transformers http://okmij.org/ftp/Computation/monads.html#LogicT. Essentially, this defines a class of monads with zero, plus, and a split operation: class (MonadPlus m) = MonadSplit m where msplit :: m a - m (Maybe (a, m a)) Essentially, if 'm' returns no results, then 'msplit m' returns Nothing, otherwise it returns Just (a, m'), where a is the first result, and m' is a computation which produces the remaining results (if any). There is an obvious implementation for the list monad, but msplit can also be defined for a monad transformer. There are a bunch of useful operations using msplit, such as the soft cut, ifte :: (MonadSplit m) = m a - (a - m b) - m b - m b ifte p th el = msplit p = maybe el (\(a,m) - th a `mplus` (m = th)) 'ifte p th el' is equivalent to 'p = th' if p returns any results, and 'el' otherwise. Note that it is *not* the same as (p = th) `mplus` el. Here's your inverse operation: mnot :: (MonadSplit m) = m a - m () mnot m = msplit m = maybe (return ()) mzero -- Dave Menendez [EMAIL PROTECTED] http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] background question about IO monad
Well, you may well be right! Just think of me as a planarian at the opera... :-) On 2/6/08, Jonathan Cast [EMAIL PROTECTED] wrote: On 6 Feb 2008, at 7:30 PM, Uwe Hollerbach wrote: Hi, all, thanks for the responses. I understand the distinction between pure functions and impure functions/procedures/IO actions, Um, I'm not sure of that, given what you go on to say. it just felt to me in the samples that I quoted that I was in fact starting from basically the starting point, Not really. The key difference to understand is that between difference between getCurrentTime and toUTCTime 42. These are your `starting points' --- the rest is just pure code. eventually getting to the same endpoint (or at least a pair of endpoints that are not easily distinguished from each other by looking just at code), and inbetween Well, the in-between paths are pure (or can be) either way. It's the starting point that needs liftIO or not. one path was going through liftIO and the other not. But I guess it comes down to the fact that, since I'm in a REPL, I'm wallowing in impurity all the time (or something like that :-) ) jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Best practice for embedding files in a GHC-compiled tool?
What is the best way to embed an arbitrary file in a Haskell program? I would like to use GHC to compile command-line tools to be used with OS X. I want the tool to be a single file, not a package or a directory, that makes no assumptions about what else is present. For example, it should be able to run as part of an OS X install disk. I want this tool to be self reproducing in the sense that one of its options causes it to output its own documentation and source code. I want this data to be stored as a compressed file within the tool binary itself. The distribution model I'm imagining here is where one writes a program anonymously, that isn't hosted anywhere but is passed from user to user because it is useful, and eventually reaches another user who wants to modify the code. Assume that intermediate users will care less about this, and will try to delete anything that they can. That rules out storing the data in a separate file. Think of the M.I.T. game Core Wars from the dawn of the computer age. I'm looking for a strategy here that will be evolutionarily successful in a fairly hostile environment. In other words, I want to be able to write in Haskell, without losing the automatic distribution of source code enjoyed by interpreted languages. No one deletes the source code for a Perl script, because by doing so they're killing the program. There must be some library I'm overlooking that would make this very easy. All I can think of is to use Template Haskell to read a compressed tar file into a Haskell variable. Is that what one does, or is there a better way? Thanks in advance, Dave ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] FP and Quality
How about the following papers on real-world Haskell programming results: - text follows immediately after this line - Haskell vs. Ada vs. C++ vs. Awk vs. ... An Experiment in Software Prototyping Productivity (1994), by Paul Hudak and Mark P. Jones: http://citeseer.ist.psu.edu/41732.html Why Functional Programming Matters (1984), by John Hughes: http://www.md.chalmers.se/~rjmh/Papers/whyfp.html Why Haskell matters (date unknown) (Web page), originally by Sebastian Sylvan: http://www.haskell.org/haskellwiki/Why_Haskell_matters - text ends immediately before this line - The following resource page may also be useful: Haskell in industry: http://www.haskell.org/haskellwiki/Haskell_in_industry The following site may also be useful: Commercial Users of Functional Programming: Functional Programming As a Means, Not an End: http://cufp.galois.com/ Barring time constraints, I may post additional findings later. Benjamin L. Russell --- PR Stanley [EMAIL PROTECTED] wrote: Thanks, keep the tips coming. I like the ones about the type safety and line counts. Cheers, Paul At 23:33 04/02/2008, you wrote: Good luck with this - I'd love to see the outcome. My experience is that FP tends to result in a lot less code, so if there are x bugs per line of code, FP has less bugs per complete application. Talking about haskell, the typesystem dissalows whole classes of bugs. Things simply do not compile if you stitch the innards together in the wrong order (particuarly if you are agressive about using the most general types possible). Since this accounts for perhaps 90% of where I do things wrong in Java, I get a corresponding decrease in run-time bugs in haskell. However, this is somewhat compensated for by the effort needed to get haskell programs through the compiler in the first place - debug at compile or debug at runtime is the tradeoff here. FP is easier to verify mechanically than imperative programming - more of the logic is exposed directly. It's easier to do by-case proofs, even if they are by-hand rather than mechanical. However, all of this is annecdotal. Good luck collecting real stats, or peer-reviewed annecdotes. You may have luck looking at bug-fix times vs number of developers for equivalent FP and Java apps/libs. Worth a shot, given that the bug-trackers tend to be public. You could probably tie it back to the size of the 'fix' patches. Get some nice graphs? Matthew On Monday 04 February 2008, you wrote: Hi folks I'm thinking of writing a little essay arguing the case for the advantages of FP for producing quality software. Can the list recommend any papers/articles which I can use as sources of my argument? I have access to the IEEE database too although earlier I couldn't find anything on the subject. Thanks, Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] parsec3 pre-release [attempt 2]
Is it good or bad to add: instance (MonadIO m) = MonadIO (ParsecT s u m) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] background question about IO monad
All right, after a bit of dinner and some time to mess about, here's another attempt to check my understanding: here is a simplified version of the lisp-time example: module Main where import System.Time pure_fn :: Integer - String pure_fn n = calendarTimeToString (toUTCTime (TOD n 0)) wicked_fn :: IO String wicked_fn = getClockTime = return . pure_fn . toI where toI (TOD n _) = n make_wicked :: String - IO String make_wicked str = return str -- use of pure_fn -- main = putStrLn (pure_fn 123000) -- use of wicked_fn -- main = wicked_fn = putStrLn -- use of make_wicked main = (make_wicked (pure_fn 1234567890)) = putStrLn If I use the first of the three main alternatives, I'm calling a pure function directly: it takes an integer, 123..., and produces a string. If I pass the same integer to the pure function, I'll get the same value, every time. This string is passed to putStrLn, an IO action, in order that I may gaze upon it, but the string itself is not thereby stuck in the IO monad. If I use the second of the three main alternatives, I'm calling an IO action: wicked_fn, which returns the current time formatted as UTC. In principle, every time I call wicked_fn, I could get a different answer. Because it's an IO action, I can't just pass it to putStrLn in the same way I passed in the previous pure_fn value, but instead I have to use the bind operator =. If I use the third of the main alternatives, I am starting with a pure function: it's that number formatted as UTC (it happens to come to Fri Feb 13 of next year), but then I pass it through the make_wicked function, which transmogrifies it into the IO monad. Therefore, as in the above, I have to use = in order to get it to work; putStrLn (make_wicked (pure_fn 123...)) doesn't work. deep breath OK, after all that, my original question, in terms of this example: the IO monad is one-way is equivalent to saying there is no haskell function that I could write that would take (make_wicked (pure_fn 123456)) and make it into something that could be used in the same way and the same places as just plain (pure_fn 123456) ? And, coming back to my scheme interpreter, this is at least somewhat irrelevant, because, since I am in a REPL of my own devising, I'm firmly in IO-monad-land, now and forever. Right? thanks, Uwe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] background question about IO monad
On Feb 7, 2008 7:32 AM, Uwe Hollerbach [EMAIL PROTECTED] wrote: pure_fn :: Integer - String pure_fn n = calendarTimeToString (toUTCTime (TOD n 0)) make_wicked :: String - IO String make_wicked str = return str -- use of make_wicked main = (make_wicked (pure_fn 1234567890)) = putStrLn OK, after all that, my original question, in terms of this example: the IO monad is one-way is equivalent to saying there is no haskell function that I could write that would take (make_wicked (pure_fn 123456)) and make it into something that could be used in the same way and the same places as just plain (pure_fn 123456) ? Spot on! Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] problem with collection (container) class
Hi! I'm pretty (not to say very) new to haskell and i've to create a new class named container that includes types that hold other values, more specific, i have created this two types: data Abb a b = Branch a b (Abb a b) (Abb a b) | Leaf and data ListAssoc a b = Node a b (ListAssoc a b) | Empty and implemented some common functions (add, search, delete, empty,etc). So when I was asked to create this new class I crashed against a big problem, or at least for me. My first attempt was: class Container c where empty :: c but when I had to implement add I tried add :: c - a - b - c although I was almost sure that it wouldn't work, so I realized that I had to give Container not one but three parameters, the container and the types of values that the container saved so I started searching and I found similar cases, but the difference iis that in this cases the class was defined as follows: class Container c e | c-e where empty :: c insert :: c - e - c member :: c - e - Bool but my particular problem here is that the types I designed hold two values of different type and these holds just one value. Besides I knew nothing about functional dependency used in here and I keep knowing almost nothing about them, but I tried something like this: class Container c a b |c - a, c - b where empty :: c add :: c - a - c search :: c - a - Maybe b del :: c - a - c toListPair :: c - [(a,b)] instance Container Abb a b where empty = Leaf add Leaf x y = Branch x y Leaf Leaf add arb@(Branch ni nd ri rd) x y|x == ni = arb |x ni = Branch ni nd ri (add rd x y) |otherwise = Branch ni nd (add ri x y) rd search Leaf x = Nothing search (Branch ni nd ri rd) x|x == ni = Just nd |x ni = search rd x |x ni = search ri x but when I try to load it in WinHugs I get the following error message: - Instance is more general than a dependency allows *** Instance : Container Abb a b *** For class: Container a b c *** Under dependency : a - b and as I have stated above my knowledge about dependencies is almost null, not to say null, so I don´t even have an idea where the error is. A suggestion that I've received was to change the type of Abb for data Abb (a,b) = Branch a b (Abb (a,b)) (Abb (a,b)) | Leaf and declare container class with just two parameters like I found in all pages I visited. I have not tried this yet, as I still have hope that what I intend to do is possible. Well if you have any suggestions I'd appreciate you send it to me and sorry for bothering you and my english, but i'm spanish-speaker. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
