Re: [Haskell-cafe] SYB3 codebase
Hi Ian Ian Lynagh: > On Fri, Oct 19, 2007 at 07:59:37PM +0200, Mads Lindstrøm wrote: > > > > http://hackage.haskell.org/cgi-bin/hackage-scripts/package/syb-with-class-0.3 > > (hereafter know as HappS-SYB3). HappS-SYB3 is based on the SYB3 code > > you mention, but the code has been changed quite a bit compared to > > using the Shelarcy patch. So it will properly require some more work. > > Can you explain what you mean by "require some more work" please? > > As far as I can remember the API provided by the code has not changed, > the changes have only been improvements to the internal code. >From the original SYB3: gfoldl :: ctx () -> (forall a b. Data ctx a => c (a -> b) -> a -> c b) -> (forall g. g -> c g) -> a -> c a >From Happs-SYB3: gfoldl :: Proxy ctx -> (forall b c. Data ctx b => w (b -> c) -> b -> w c) -> (forall g. g -> w g) -> a -> w a looking at the first argument you will see a slight difference. Also the original SYB3 contains the function gfoldlAccum, which the HappS version do not contain. There are other differences too. > > > I have not been able to find any documentation for HappS-SYB3. > > The SYB3 paper describes how to use it, but other than that there is no > documentation. Of course, if anyone wanted to write some other docs then > that would be great! Yes, that would be great. > > > Thus I have no idea of his position on my usage of HappS-SYB3. > > I'm not sure exactly what you're asking. syb-with-class is > BSD3-licenced, and anyone is free to use it for whatever they want > within the terms of that licence. I was not referring to the license. To be earnest I can see that I was not clear about what I was referring to :( I was thinking about the level of support. Was this just a library to support HappS, and people could use it but there would be no help if they ran into problems. Or would it receive the same support as the HappS project gives to there users. > > Thanks > Ian > Greetings, Mads ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Hiding side effects in a data structure
I've done something similar, I think. Often, I want to output some
kind of progress indicator, just to show that the program is working.
Typically, the program works by lazily evaluating a list (lines from
an input file, say); each element of the list is wrapped with an IO
action that outputs the status when evaluated -- which typically
happens lazily from pure code.
> countIO :: String -> String -> Int -> [a] -> IO [a]
> countIO msg post step xs = sequence $ map unsafeInterleaveIO ((blank >>
> outmsg (0::Int) >> c):cs)
>where (c:cs) = ct 0 xs
> output = hPutStr stderr
> blank= output ('\r':take 70 (repeat ' '))
> outmsg x = output ('\r':msg++show x) >> hFlush stderr
> ct s ys = let (a,b) = splitAt (step-1) ys
>next = s+step
>in case b of [b1] -> map return a ++ [outmsg (s+step) >>
> hPutStr stderr post >> return b1]
> [] -> map return (init a) ++ [outmsg
> (s+length a) >> hPutStr stderr post >> return (last a)]
> _ -> map return a ++ [outmsg s >> return
> (head b)] ++ ct next (tail b)
-k
--
If I haven't seen further, it is by standing in the footprints of giants
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Hiding side effects in a data structure
Jon Fairbairn wrote: > A hyperlink of the form href="http://.../long-research-paper.html#interesting-paragraph";> interesting bit is far more useful than one of the form http://.../long-research-paper.pdf";>look for section 49.7.3. It may not seem significant, but when one is attempting to learn some new part of Haskell it's really off-putting. Pdfs are not that bad. You can hyper link into them too. It would look like: http://.../long-research-paper.pdf#page=45";> ... to open the pdf a position you on page 45 of it or like: http://.../long-research-paper.pdf#anchorName";> ... to open the pdf and position you on anchor anchorName You can do it from command line too: acrord32 /A page=45 long-research-paper.pdf acrord32 /A anchorName long-research-paper.pdf This of course requires the source to give you more precise link. But here there is no difference from html only ... possibly ... more people know about html linking than pdf linking. The above definitely works OK on windows, not sure about linux pdf viewers. Unfortunately I cannot find now how you can look at all anchors defined in a pdf (so that you can use something better than page=). Peter. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Hiding side effects in a data structure
Peter Hercek <[EMAIL PROTECTED]> writes: > Jon Fairbairn wrote: > > A hyperlink of the form > href="http://.../long-research-paper.html#interesting-paragraph";> >> interesting bit is far more useful than one of the form >> http://.../long-research-paper.pdf";>look for >> section 49.7.3. It may not seem significant, but when >> one is attempting to learn some new part of Haskell it's >> really off-putting. > > Pdfs are not that bad. No, they (or at least links to them) typically are that bad! Mind you, as far as fragment identification is concerned, so are a lot of html pages. But even if the links do have fragment ids, pdfs still impose a significant overhead: I don't want stuff swapped out just so that I can run a pdf viewer; a web browser uses up enough resources as it is. And will Hoogle link into pdfs? > The above definitely works OK on windows, not sure about linux > pdf viewers. Works perfectly on my Fedora 7 systems. While this would be a definite improvement over having to search through the pdf, the delay and the fact that pdfs aren't as good as html for on-line viewing are still enough of an overhead that it's discouraging. If I'm using PHP (an execrable language), I can type the name (or something like the name) of any function into the search box on the PHP manual webpage and get useful (albeit often extremely irritating from a Haskell programmer's point of view) results straight back. Even including my language designer's distaste for PHP, this can make writing a wee bit of PHP a less onerous event than writing the same thing in Haskell -- definitely not what we want! -- Jón Fairbairn [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Polymorphic (typeclass) values in a list?
Brandon S. Allbery KF8NH wrote: On Oct 19, 2007, at 12:11 , Sebastian Sylvan wrote: On 19/10/2007, Kalman Noel <[EMAIL PROTECTED]> wrote: data ExistsNumber = forall a. Num a => Number a I'm without a Haskell compiler, but shouldn't that be "exists a."? The problem is that "exists" is not valid in either Haskell 98 or any current extension, whereas "forall" is a very common extension. But you can simulate "exists" via "forall", which is the thrust of these approaches. When 'exists' is not a keyword, why 'forall' is needed at all? Isn't everything 'forall' qualified by default? ... or are type variables sometimes 'exists' qualified by default depending on context? That would be confusing though... I do not understand why 'forall' keyword is needed. Peter. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Hiding side effects in a data structure
Yes, htmls are better than pdfs (more lightweight, easier to work with if exact page layout is not important). I just wanted to point out that it is possible to link into some particular place of a pdf document. So the linking availability should not be the argument by itself. I would prefer html too but if pdf is required otherwise, it would be nice if link suppliers would provide more precise links. To spread the information that they can do so is the main reason I responded. Peter. Jon Fairbairn wrote: Peter Hercek <[EMAIL PROTECTED]> writes: Jon Fairbairn wrote: > A hyperlink of the form href="http://.../long-research-paper.html#interesting-paragraph";> interesting bit is far more useful than one of the form http://.../long-research-paper.pdf";>look for section 49.7.3. It may not seem significant, but when one is attempting to learn some new part of Haskell it's really off-putting. Pdfs are not that bad. No, they (or at least links to them) typically are that bad! Mind you, as far as fragment identification is concerned, so are a lot of html pages. But even if the links do have fragment ids, pdfs still impose a significant overhead: I don't want stuff swapped out just so that I can run a pdf viewer; a web browser uses up enough resources as it is. And will Hoogle link into pdfs? The above definitely works OK on windows, not sure about linux pdf viewers. Works perfectly on my Fedora 7 systems. While this would be a definite improvement over having to search through the pdf, the delay and the fact that pdfs aren't as good as html for on-line viewing are still enough of an overhead that it's discouraging. If I'm using PHP (an execrable language), I can type the name (or something like the name) of any function into the search box on the PHP manual webpage and get useful (albeit often extremely irritating from a Haskell programmer's point of view) results straight back. Even including my language designer's distaste for PHP, this can make writing a wee bit of PHP a less onerous event than writing the same thing in Haskell -- definitely not what we want! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Polymorphic (typeclass) values in a list?
Peter Hercek wrote: > When 'exists' is not a keyword, why 'forall' is needed at all? > Isn't everything 'forall' qualified by default? “forall” isn't a keyword in Haskell 98. As an extension to the language, however, it makes certain types expressible that can not be written in H98, for example f :: (forall a. a) -> T which is different from g :: forall a. a -> T although both are not particularly useful. (The only argument that f will ever take is bottom!) In the context of existentially quantified types, however, the forall keyword is used probably to make the use of an extension more explicit. Without the forall keyword, data U = C a would be an existential, while the programmer maybe really wanted the usual data U a = C a Kalman -- Find out how you can get spam free email. http://www.bluebottle.com/tag/3 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange subtract operator behavior - and lazy naturals
I wrote: Yitzchak Gale wrote: >> So why not make the laziness available >> also for cases where "1 - 2 == 0" does _not_ do >> the right thing? >> data LazyInteger = IntZero | IntSum Bool Integer LazyInteger >> or >> data LazyInteger = LazyInteger Bool Nat >> or whatever. Luke Palmer wrote: > data LazyInteger = IntDiff Nat Nat > The only value which would diverge when > compared to a constant would be infinity - infinity. Hmm. But then you could have integers that are divergent and non-infinite. What do we gain by doing it this way? -Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Hiding side effects in a data structure
On Oct 21, 2007, at 6:29 , Jon Fairbairn wrote: No, they (or at least links to them) typically are that bad! Mind you, as far as fragment identification is concerned, so are a lot of html pages. But even if the links do have fragment ids, pdfs still impose a significant overhead: I don't want stuff swapped out just so that I can run a pdf viewer; a web browser uses up enough resources as it is. And will Hoogle link into pdfs? I prefer HTML for online viewing and PDF for offline. BTW, you might consider a trick: look up the PDF on google, use the HTML view. This is generally poor for documents with significant graphics, but works reasonably well for most Haskell papers (modulo math I usually can't figure out anyway, lacking the background many Haskellers have in set theory / rings / groups/semigroups etc.). -- 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] Re: Polymorphic (typeclass) values in a list?
On Oct 21, 2007, at 6:41 , Peter Hercek wrote: Brandon S. Allbery KF8NH wrote: On Oct 19, 2007, at 12:11 , Sebastian Sylvan wrote: On 19/10/2007, Kalman Noel <[EMAIL PROTECTED]> wrote: data ExistsNumber = forall a. Num a => Number a I'm without a Haskell compiler, but shouldn't that be "exists a."? The problem is that "exists" is not valid in either Haskell 98 or any current extension, whereas "forall" is a very common extension. But you can simulate "exists" via "forall", which is the thrust of these approaches. When 'exists' is not a keyword, why 'forall' is needed at all? NB. Haskell98 doesn't have forall. All type variables are implicitly scoped to the entire type (e.g. foo :: (a -> b) -> a -> b is actually foo :: forall a b. (a -> b) -> a -> b). The point of the forall keyword is that it can be scoped. Compare runState to runST: ST carries around a bracketed forall on the state expression (forall s. ST s a), preventing it from being viewed or modified (or initialized!) outside the scope established by runST, whereas you can carry around a State (State s a) and thread the state s through an expression "by hand" via evalState / execState (or pattern matching on the State value, which is what those translate to after a pass through runState). Given scoped forall, you can simulate exists by using something very like (identical to, via Curry-Howard?) de Morgan's Rule. -- 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
[Haskell-cafe] Re: [Haskell] Re: Trying to install binary-0.4
(moving to haskell-cafe) On Sun, 2007-10-21 at 14:55 +0200, Udo Stenzel wrote: > Duncan Coutts wrote: > > New tarball releases of Cabal-1.2.1, bytestring-0.9, binary-0.4.1, tar > > and others (zlib, bzlib, iconv) will appear on hackage in the next few > > days. > > I just tried one of them, iconv. First it wants a recent cabal; that's > fine, I installed the darcs version. Then I get this: > > | Codec/Text/IConv.hs:64:17: > | Could not find module `Data.ByteString': > | it is a member of package bytestring-0.9, which is hidden > > Okay, it obviously tries to be smart, but doesn't know that I upgraded > to a separate ByteString library. Right. > So I take out the gunk about 'flag(bytestring-in-base)' and try again: > | Setup: At least the following dependencies are missing: > | base <2.0||>=2.2 > > Of course that was to be expected, since I have base-2.0 hacked to not > get in conflict with bytestring-0.9, and you (Duncan) couldn't possibly > anticipate this (or could you?). Right. It expects that if you have base >= 2.0 && < 2.2 then that version of base exports Data.ByteString. That's not an unreasonable assumption I think. You can hack the .cabal file further to make it work in your situation, but I don't suggest that's a great long term solution. If you wanted to hack it you'd change it to just: build-depends: base, bytestring >= 0.9 without any 'if' or flags and without cpp-options: -DBYTESTRING_IN_BASE. > Now what am I supposed to do? Give my messed up base a new version > number? (Which one?) Rewrite every single cabal file, hoping that > they never become Turing complete turning the exercise into a reverse > engineering fest rivaling the ICFP contest? Bite the bullet and > install GHC from darcs? So you've changed the API of base-2.1.1 so that will break packages that expect that they know what the api of base-2.1.1 actually is. You can either hack the .cabal files of things you try to install (which would be a pain, I don't recommend it) or you could revert your changes to your base package. > For the time being, I'll go with 'ghc --make'. And I think that cabal > configurations are an exceptionally bad idea carried to perfection. Don't get me wrong, I'm not claiming that the changes in what is in and what is out of the base package could not have been handled better. Configurations just happen to be one mechanism that we have available now to enable packages to build with various versions of the base package. The other alternative seemed to be that they'd only work with an old or a new version but not both. There are plenty of things that we could have done better to make the base changes less disruptive but I really don't think you can blame configurations for that or for adding to that problem. If we had made different decisions at various points we would not need configurations for this purpose right now. We'd still need configurations for other things. Configurations serve other purposes too. They're not just for managing the mess over moving modules between packages. They're generally to allow changes in the way a package is built depending on the environment in which the package is built to reduce the need for non-portable configure scripts and wadges of fragile code in Setup.hs files. > They make things worse, not better. (And that's just GHC 6.6... I don't > want to even think about what happens on Hugs, JHC and YHC.) It's mostly orthogonal to the Haskell implementation since the base package is shared by all Haskell implementations. > What would it take to talk you into giving up on supporting the broken > base-2.0 and incorporating a patch to unbreak it into the bytestring > setup? Can I stop the insanity by simply writing that patch? What kind of change are you suggesting? We have to support base 2.x because that is the versions of base that come with ghc-6.6.x. We cannot sensibly install the separate bytestring package with ghc-6.6.x because it would clash with the base package there. We cannot easily upgrade base in existing installations of ghc because ghc is just not designed with that in mind at the moment. The solution we're using at the moment is to use the separate bytestring package with ghc-6.4 and ghc-6.8 and to use the version of the bytestring code in base-2.x for ghc-6.6.x. That's what the newest versions of zlib, bzlib, iconv, binary, tar etc do. They all work with ghc-6.4, 6.6 and 6.8 (using Cabal-1.2.x). > > So all will not be plain sailing for the first few weeks after > > ghc-6.8 comes out as maintainers update their packages. People will have > > to be patient and/or stick to ghc-6.6 for a bit. > > Okay, so now we have *three* almost-stable versions of GHC in wide > circulation, all of them broken in different ways with respect to cabal > packages. I feel tears welling up... So far this weekend I've uploaded to hackage: Cabal-1.2.1, bytestring-0.9, unix-compat-0.1.1, tar-0.1.1 and Kolmodin uploaded binary-0.4.1.
[Haskell-cafe] Re: [Haskell] [Fwd: undecidable & overlapping instances: a bug?]
Hello, On 10/19/07, Martin Sulzmann <[EMAIL PROTECTED]> wrote: > Simon Peyton-Jones writes: > > ... > > Like you, Iavor, I find it very hard to internalise just why (B) and (C) > are important. But I believe the paper gives examples of why they are, and > Martin is getting good at explaining it. Martin: can you give an example, > once more, of the importance of (B) (=fullness)? > > > > Fullness (B) is a necessary condition to guarantee that the constraint > solver (aka CHR solver) derived from the type class program is confluent. > > Here's an example (taken from the paper). > > class F a b c | a->b > instance F Int Bool Char > instance F a b Bool => F [a] [b] Bool > > The FD is not full because the class parameter c is not involved in > the FD. We will show now that the CHR solver is not confluent. > > Here is the translation to CHRs (see the paper for details) > > rule F a b1 c, F a b2 d ==> b1=b2 -- (FD) > rule F Int Bool Char<==> True -- (Inst1) > rule F Int a b ==> a=Bool -- (Imp1) > rule F [a] [b] Bool <==> F a b Bool -- (Inst2) > rule F [a] c d ==> c=[b] -- (Imp2) > > > The above CHRs are not confluent. For example, > there are two possible CHR derivations for the initial > constraint store F [a] [b] Bool, F [a] b2 d > > F [a] [b] Bool, F [a] b2 d > -->_FD (means apply the FD rule) > F [a] [b] Bool, F [a] [b] d , b2=[b] > --> Inst2 > F a b Bool, F [a] [b] d , b_2=[b] (*) > > > Here's the second CHR derivation > > F [a] [b] Bool, F [a] b2 d > -->_Inst2 > F a b Bool, F [a] b2 d > -->_Imp2 > F a b Bool, F [a] [c] d, b2=[c] (**) > > > (*) and (**) are final stores (ie no further CHR are applicable). > Unfortunately, they are not logically equivalent (one store says > b2=[b] whereas the other store says b2=[c]). But what is wrong with applying the following logical reasoning: Starting with (**): F a b Bool, F [a] [c] d, b2=[c] (by inst2) F a b Bool, F [a] [c] d, b2=[c], F [a] [b] Bool (by FD) F a b Bool, F [a] [c] d, b2=[c], F [a] [b] Bool, [c] = [b] (applying equalities and omitting unnecessary predicates) F [a] [b] Bool, F [a] b2 d (...and then follow your argument to reach (*)...) Alternatively, if we start at (*): F a b Bool, F [a] [b] d , b_2=[b] (by inst2) F a b Bool, F [a] [b] d , b_2=[b], F [a] [b] Bool (applying equalities, rearranging, and omitting unnecessary predicates) F [a] [b] Bool, F [a] b_2 d (... and then follow you reasoning to reach (**) ...) So it would appear that the two sets of predicates are logically equivalent. > To conclude, fullness is a necessary condition to establish confluence > of the CHR solver. Confluence is vital to guarantee completeness of > type inference. > > > I don't think that fullness is an onerous condition. I agree with you that, in practice, many classes probably use "full" FDs. However, these extra conditions make the system more complicated, and we should make clear what exactly are we getting in return for the added complexity. -Iavor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] How much of Haskell was possible 20 years ago?
Hi, I like Haskell, and use it as my main language. However, compiling a Haskell program usually takes a lot of memory and CPU. So I was curious, and would like to know from computer scholars in this list: how much of Haskell would be possible in machines with really low CPU and memory? Which features would be feasible for a compiler to implement, and for programmers to use? Thanks, Maurício ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How much of Haskell was possible 20 years ago?
Maurício writes: ... compiling a Haskell program usually takes a lot of memory and CPU. So I was curious, and would like to know from computer scholars in this list: how much of Haskell would be possible in machines with really low CPU and memory? Which features would be feasible for a compiler to implement, and for programmers to use? Check up Gofer of Mark Jones. http://web.cecs.pdx.edu/~mpj/goferarc/index.html Choose your preferred version from: http://citeseer.ist.psu.edu/jones94implementation.html Jerzy Karczmarczuk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How much of Haskell was possible 20 years ago?
On Oct 21, 2007, at 14:40 , Maurí cio wrote: I like Haskell, and use it as my main language. However, compiling a Haskell program usually takes a lot of memory and CPU. So I was To some extent this is just a matter of Haskell not having been around that long ago: as ghc evolves, it's been getting better about this. Before ghc snapshots stopped being able to compile themselves (*grumble* --- is this fixed yet?) I found that ghc 6.7 compiling itself didn't do nearly as much violence to my desktop machine as compiling 6.7 (or 6.8pre or 6.9) with ghc 6.4 / 6.6 / 6.6.1. -- 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
[Haskell-cafe] Re: How much of Haskell was possible 20 years ago?
Brandon S. Allbery KF8NH escreveu: On Oct 21, 2007, at 14:40 , Maurí cio wrote: I like Haskell, and use it as my main language. However, compiling a Haskell program usually takes a lot of memory and CPU. So I was To some extent this is just a matter of Haskell not having been around that long ago: as ghc evolves, it's been getting better about this. Before ghc snapshots stopped being able to compile themselves (*grumble* --- is this fixed yet?) I found that ghc 6.7 compiling itself didn't do nearly as much violence to my desktop machine as compiling 6.7 (or 6.8pre or 6.9) with ghc 6.4 / 6.6 / 6.6.1. Of course. But I think of somethink like a Intel 386 with 4MB of memory. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: How much of Haskell was possible 20 years ago?
On Sun, 21 Oct 2007, [ISO-8859-1] Maurício wrote: > Of course. But I think of somethink like a Intel 386 with 4MB > of memory. According to "The History of Haskell" http://www.haskell.org/haskellwiki/History_of_Haskell (early versions of) Haskell could be used on such machines. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: How much of Haskell was possible 20 years ago?
On Oct 21, 2007, at 15:21 , Maurí cio wrote: Of course. But I think of somethink like a Intel 386 with 4MB of memory. It's kinda surprising to me how many people think that just because current/modern implementations of things use memory wastefully, this is somehow mandatory. When machines were smaller, programs used algorithms which were suited to those machines; the reason they don't now is to some extent laziness but also because those algorithms often didn't scale to larger available memory (i.e. you get *big* speedups with more profligate algorithms when the memory they want is available). -- 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
[Haskell-cafe] Re: How much of Haskell was possible 20 years ago?
Mauricio writes: ... But I think of somethink like a Intel 386 with 4MB of memory. It seems you decided to ignore my message. OK. I repeat it once more, and there will be no more. Gofer was a perfectly genuine Haskell, it run in a 640K box, and influenced considerably the type system of newer Haskell. Jerzy Karczmarczuk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: How much of Haskell was possible 20 years ago?
On Oct 21, 2007, at 15:31 , [EMAIL PROTECTED] wrote: Mauricio writes: ... But I think of somethink like a Intel 386 with 4MB of memory. It seems you decided to ignore my message. OK. Whoa there! Why assume malice? I got both his quoted response and your message at about the same time, which suggests to me he hadn't seen yours yet when he sent it. -- 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
[Haskell-cafe] Re: How much of Haskell was possible 20 years ago?
Brandon S. Allbery KF8NH writes: [EMAIL PROTECTED] wrote: It seems you decided to ignore my message. OK. Whoa there! Why assume malice? I got both his quoted response and your message at about the same time, ... Gosh, I am not assuming any malice, I am too old for that... I could have thought, since it has happened already, that Mauricio, or whoever *dismisses* Gofer, as something so old that it couldn't be possibly related to modern languages. Mind you, Mark Jones did it before 1994, when the paper reporting the implementation has been written. Several guys here were not born yet. OK, don't shout, I know I exaggerate... What I found somehow funny, with all respect, is the combination: 20 years ago, which means '87, and miserable 4M of memory. At that time 4M on a personal computer was not so frequent, at least in Europe. Jerzy Karczmarczuk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Automatic file closing after readFile
Magnus Therning wrote: I'll certainly try to look into all of that. However, I suspect your suggestion doesn't scale very well. On my original code it's easy, it was less than 10 lines, but how do I know where to start looking if it's a program of 100 lines, or 1000 lines? The problem could occur in an updated library that I just use... Well you get the idea :-) A library function is supposed to tell you its time usage, memory usage, file usage, ... generally resource usage, as part of its specification. A 100-line program is not supposed to be a monolith. It is supposed to be a combination of 10 functions (or 10 parts; I'll call them functions anyway), 10 lines each. Each function is supposed to come with its specification too, which again tells you its resource usage. To reason about the 100-line program, you only need to reason about 10 lines of specifications. To reason about a program that calls a library function, you only need to plug its specification --- emphatically not its code! --- at the call site, and proceed. (It remains to reason that each 10-line function conforms to its 1-line specification, but we agreed that 10 lines are ok. It also remains to reason that the library function conforms to its documented specification, but that is the author's job, and again the author can apply the same divide-and-conquer to stay tractable.) To reason about a 1000-line program, again it is not supposed to be a monolith. It is supposed to be a combination of 10 functions, each 100 lines. The 1000-line program is 10 lines of specifications combined. We already know how to deal with each 100-line function... You get the idea. Divide-and-conquer. Abstraction. Modularization. Separation of Concerns. That is how reasoning about programs scales. That is how writing programs in the first place scales. That is how anything at all scales. Some suggested musings: "Rome is not built in one day" or whatever the proverb's wording is. Intelligent Design vs Random Mutation. Is your program invented or discovered? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Automatic file closing after readFile
On Sun, 2007-10-21 at 17:15 -0400, Albert Y. C. Lai wrote: > Magnus Therning wrote: > > I'll certainly try to look into all of that. However, I suspect your > > suggestion doesn't scale very well. On my original code it's easy, it > > was less than 10 lines, but how do I know where to start looking if it's > > a program of 100 lines, or 1000 lines? The problem could occur in an > > updated library that I just use... Well you get the idea :-) > > A library function is supposed to tell you its time usage, memory usage, > file usage, ... generally resource usage, as part of its specification. > > A 100-line program is not supposed to be a monolith. It is supposed to > be a combination of 10 functions (or 10 parts; I'll call them functions > anyway), 10 lines each. Each function is supposed to come with its > specification too, which again tells you its resource usage. > > To reason about the 100-line program, you only need to reason about 10 > lines of specifications. I'm not sure what semantics we would use to reason about resource use in specifications like this. Our standard semantics abstract over space, time and sharing properties of our programs. For a lazy language, resource specifications of functions do not compose in a simple way. For example we might naively say that [1..m] uses m time and space and that take n takes at most n time and space but then take n [1..m] does not take the sum of these two time/space specifications. In more complex examples the connection is even less obvious. One more accurate way to look at resource use is to say that we only consider time and space to reduce to WHNF and then ask that question when we apply various evaluation functions to the expression. Different evaluation functions would force various parts of the value. Then when we plug an expression into different contexts we see what kind of evaluation function that context is and use that in our question about the resource use to evaluate the expression. Still, that only gives you total resource use, not maximum resource use at any point during evaluation which is important for space. Summary: it's not so simple. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
On Wed, 2007-10-17 at 15:06 -0700, Dan Weston wrote: > That is a great tutorial. Thanks! But in the last two sentences of the > introduction you say: > > > We just need to find any program with the given type. > > The existence of a program for the type will be a proof > > of the corresponding proposition! > > Maybe you should make explicit that > > 1) the type is inhabited > > undefined :: forall p . p > > does not prove that all propositions are true Yes it does. > > 2) the function must halt for all defined arguments > > fix :: forall p . (p -> p) -> p > fix f = let x = f x in x > > does not prove the (false) theorem > > (p => p) => p Yes it does. Terms in Haskell prove the propositions that the types of Haskell correspond to. *The logic that Haskell's type systems corresponds to is inconsistent.* This is what you are missing. Haskell's type systems does not correspond to intuitionistic propositional logic. Indeed, in the actual statement of the Curry-Howard correspondence, it's a correspondence between intuitionistic propositional logic and the simply typed lambda calculus which Haskell quite certainly is not. As is well known, it (CH) can be generalized beyond that, but generally you need a strongly normalizing language (or at least prove strong normalization for your particular term and note normalization means -normal form- not weak head normal form) to actually use the "programs" as proofs. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Polymorphic (typeclass) values in a list?
TJ: > After all, sometimes all you need to know about a list is that > all the elements support a common set of operations. If I'm > implementing a 3d renderer for example, I'd like to have > > class Renderable a where > render :: a -> RasterImage > > scene :: Renderable a => [a] Everyone has launched into explanations of how to use existentials to do this, but you may be happy in just haskell 98. In the above, you could just have: scene :: [RasterImage] Laziness will ensure that the computation/storage of the images will not occur until they are used. Tim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How much of Haskell was possible 20 years ago?
All of Haskell was possible 20 years ago. The LML compiler (written in LML) compiled a language similar to Haskell, the only real differences is syntax and the type system (and monadic IO wasn't invented yet). It was a bit slow to recompile itself, but not bad. A 16MHz 386 and 8M of memory certainly sufficed. -- Lennart On 10/21/07, Maurício <[EMAIL PROTECTED]> wrote: > > Hi, > > I like Haskell, and use it as my main > language. However, compiling a Haskell program > usually takes a lot of memory and CPU. So I was > curious, and would like to know from computer > scholars in this list: how much of Haskell would > be possible in machines with really low CPU and > memory? Which features would be feasible for a > compiler to implement, and for programmers to use? > > Thanks, > Maurício > > ___ > 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] Using Haddock to document ADTs
Hi all, I'm beginning to get familiar with Haddock and I want to document a library which, as usually happens, has some ADT definitions. I'd like to document the ADTs both for the end-user (who shouldn't be told about its internal implementation) and future developers. Let's imagine my library is called FooLib, defines an ADT whose implementation is hidden by an outer module. === FooLib/ADT1.hs = -- | This module defines my type ADT1 module ADT1 -- | This type implements whatever and. As you can see it's implemented -- using blah blah so that is more efficient because of blah blah data ADT1 a = ... == Foolib.hs -- | This is Foolib which is aimed at whatever module Foolib (ADT) where import ADT === Generating documentation for Foolib.hs with this Haddock annotations will unfortunatelly reveal implementation details since the annotation of ADT1 is forwarded. My question is, How can I generate documentation for both developers and the end-users using the same Haddock annotations? I'm beginning to think it would be a good idea to distinguish those two cases (documentation for end-users and internal developers) in Haddock, but I'm probably wrong since it seems a common thing and wasn't implemented yet. Best Regards, Alfonso ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Using Haddock to document ADTs
On 10/22/07, Alfonso Acosta <[EMAIL PROTECTED]> wrote: > == Foolib.hs > -- | This is Foolib which is aimed at whatever > module Foolib (ADT) where > > import ADT > > === Sorry, I meant (although my error was probably obvious) == Foolib.hs -- | This is Foolib which is aimed at whatever module Foolib (ADT1) where import ADT1 === ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
There's nothing wrong with Haskell types. It's the terms that make Haskell types an inconsistent logic. But that doesn't mean that the C-H correspondence doesn't have any insight to offer. -- Lennart On 10/21/07, Derek Elkins <[EMAIL PROTECTED]> wrote: > > On Wed, 2007-10-17 at 15:06 -0700, Dan Weston wrote: > > That is a great tutorial. Thanks! But in the last two sentences of the > > introduction you say: > > > > > We just need to find any program with the given type. > > > The existence of a program for the type will be a proof > > > of the corresponding proposition! > > > > Maybe you should make explicit that > > > > 1) the type is inhabited > > > > undefined :: forall p . p > > > > does not prove that all propositions are true > > Yes it does. > > > > > 2) the function must halt for all defined arguments > > > > fix :: forall p . (p -> p) -> p > > fix f = let x = f x in x > > > > does not prove the (false) theorem > > > > (p => p) => p > > Yes it does. > > Terms in Haskell prove the propositions that the types of Haskell > correspond to. *The logic that Haskell's type systems corresponds to is > inconsistent.* This is what you are missing. Haskell's type systems > does not correspond to intuitionistic propositional logic. Indeed, in > the actual statement of the Curry-Howard correspondence, it's a > correspondence between intuitionistic propositional logic and the simply > typed lambda calculus which Haskell quite certainly is not. As is well > known, it (CH) can be generalized beyond that, but generally you need a > strongly normalizing language (or at least prove strong normalization > for your particular term and note normalization means -normal form- not > weak head normal form) to actually use the "programs" as proofs. > > ___ > 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] Tutorial: Curry-Howard Correspondence
Hello, On 10/17/07, Lennart Augustsson <[EMAIL PROTECTED]> wrote: > Check Wikipedia. Peirce law, law of excluded middle, double negation, ... > they are all equivalent and it can be instructive to see how one can derive > one from the other. Apparently these axioms are not all equivalent (I was quite surprised to learn that :-). Here is some interesting---but perhaps a bit advanced for a tutorial on CH---reading which studies the relation between classical logic and computation: http://coq.inria.fr/~herbelin/publis/icalp-AriHer03-minimal-classical.ps.gz -- Iavor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-level arithmetic
Manuel M T Chakravarty writes: > Ross Paterson wrote, > > On Tue, Oct 16, 2007 at 10:56:27AM +1000, Manuel M T Chakravarty wrote: > >> Lennart Augustsson wrote, > >>> And Haskell embedded a logical programming language on accident. > >> Well, we are just trying to fix that :) > > > > Since types are inferred using unification, and classes are still present, > > adding functions yields a functional logic programming language at the > > type level. > > I used to agree with that, but I changed my opinion. Or more > precisely, I'd say that it is a very weak functional logic language. > "Weak" in the sense that it's logic component is essential nil. > > Let me justify this statement. We have type variables that are like > "logical variables" in logic programming languages. However, we > never use function definitions to guess values for type variables. > Instead, function evaluation simplify suspends when it depends on an > uninstantiated variable and resumes when this variable becomes > instantiated. (The functional logic people call this evaluation > strategy "residuation".) For example, if we have > >type family T a >type instance T Int = Char > > then, given (T a ~ Char), we do *not* execute T backwards and infer > (a = Int). Instead, we leave (T a ~ Char) as it is and evaluate 'T' > only when 'a' becomes fixed. > Explained slightly differently. The above type function is open (hence, we only apply matching) whereas in functional logic programming type functions are closed (therefore, we use unification/residuation). Such an approach fits well together with "open" type classes as found in Haskell. Martin > There have been proposals for truely functional logic languages > using residuation, but they include support for backtracking and > producing multiple solutions to a single query. We support neither > on the type level. > > So, the only interaction between type functions and unification left > is that function evaluation suspends on uninstantiated type > variables and resumes when they become instantiated. This is not > functional logic programming, it is *concurrent* functional > programming with single-assignment variables. In fact, languages > such as Id and pH, which are routinely characterised as concurrent > functional, use exactly this model. > > I don't think the presence of type classes *without* functional > dependencies changes this. > > Manuel > > PS: You get a *real* functional logic language by truly performing > unification modulo an equational theory. This leads to the > concept of E-unification and, in our constructor-based context, > to "narrowing" as an evaluation strategy. > ___ > 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] Re: [Haskell] [Fwd: undecidable & overlapping instances: a bug?]
Hi All, Here are my responses to the recent messages, starting with some summary comments: - I agree with Martin that the condition I posted a few days ago is equivalent to the "*refined* weak coverage condition" in your paper. The "refined" tag here is important---I missed it the first time and thought he was referring to the WCC at the start of Section 6.1, and I would strongly recommend against using that (unrefined) version. I confess that I haven't read the paper carefully enough to understand why you included that first WCC at all; I don't see any reason why you would want to use that particular condition in a practical implementation, and I don't see any advantages to it from a theoretical perspective either. (Maybe you just used it as a stepping stone to help motivate the refined WCC?) - I believe that the refined WCC (or the CC or even the original WCC if you really want) are sufficient to ensure soundness. I don't agree that the (B) restriction to "full" FDs is necessary. - I think it is dangerous to tie up soundness with questions about termination. The former is a semantic property while the latter has to do with computability. Or, from a different perspective, soundness is essential, while termination/decidability is "only" desirable. I know that others have thought more carefully than I have about conditions on the form of class and instance declarations that will guarantee decidability and I don't have much to say on that topic in what follows. However, I will suggest that one should start by ensuring soundness and then, *separately*, consider termination. (Of course, it's perfectly ok---just not essential---if conditions used to ensure soundness can also be used to guarantee termination.) Stop reading now unless you're really interested in the details! I'm going to start by explaining some key (but hopefully unsurprising) ideas before I respond in detail to the example that Martin posted. Interpreting Class, Instance, and Dependency Decls: --- I'll start by observing that Haskell's class, instance, and functional dependency declarations all map directly to formulas in standard predicate logic. The correspondence is straightforward, so I'll just illustrate it with some examples: Declaration Formula --- --- class Eq a => Ord a forall a. Ord a => Eq a instance Eq a => Eq [a] forall a. Eq a => Eq [a] class C a b | a -> b forall a, b. C a b /\ C a c => b = c This correspondence between declarations and formulas seems to be very similar to what you did in the paper using CHRs. I haven't read the paper carefully enough to know what extra mileage and/or problems you get by using CHRs. To me, predicate logic seems more natural, but I don't think that matters here---I just wanted to acknowledge that essentially the same idea is in your paper. In the following, assuming some given program P, I'll write I(P) for the conjunction of all the instance declaration formulas in P; C(P) for the conjunction of all the class declaration formulas; and F(P) fo the conjunction of all the dependency declaration formulas. Semantics and Soundness: We'll adopt a simple and standard semantics in which each n-parameter type class is described by an n-place relation, that is, a set of n-tuples of types. Of course, in the most common, one parameter case, this is equivalent to viewing the class as a set of types. Each tuple in this relation is referred to as an "instance" of the class, and the predicate syntax C t1 ... tn is just a notation for asserting that the tuple (t1, ..., tn) is an instance of C. We can assign a meaning to each of the classes in a given program P by using the smallest model of the instance declaration formulas, I(P). (Existence of such a model is guaranteed; it is the union of an increasing chain of approximations.) What about the superclass properties in C(P)? We expect to use information from C(P) to simplify contexts during type inference. For example, if we're using the standard Haskell prelude, then we know that we can simplify (Eq a, Ord a) to (Ord a). But how do we know this is sound? Haskell answers this by imposing restrictions (third bullet in Section 4.3.2 of the report) on the use of instance declarations to ensure that our (least) model of I(P) is also a model of C(P). This guarantees, for example, that every type in the semantics of "Ord" will, as required, also be included in the semantics of "Eq". That should all seem pretty standard, but I've included it here to make the point that we need to something very similar when we introduce functional dependencies. Specifically, we want to be able to use properties from F(P) to simplify/improve contexts during type inference, so we have to ensure that this is sound. If we follow the strategy that was used to ensure soundness of
[Haskell-cafe] Re: How much of Haskell was possible 20 years ago?
>>> It seems you decided to ignore my message. OK. >> >> Whoa there! Why assume malice? I got both his >> quoted response and your message at about the >> same time (...) > > (...) *dismisses* Gofer, as something so old > that it couldn't be possibly related to modern > languages. Mind you, Mark Jones did it before > 1994,(...) OK, don't shout, I know I > exaggerate... What I found somehow funny, with > all respect, is the combination: 20 years ago, > which means '87, and miserable 4M of memory. At > that time 4M on a personal computer was not so > frequent, at least in Europe. Jerzy > Karczmarczuk Sorry, Jerzy. Brandon message was just faster to answer, I'll need some time to check Gofer. I also wrote PC-AT with 256KB in my original message, but I changed it to 386 since I didn't want you guys to feel under an attack from reactionarys. People feelings are easy to hurt, and it's difficult to please everyone :) 20 years ago, I wrote a brute force attack on a magazine game, but when my TK-3000 Apple found an answer the due date had long passed and I could not get a prize from the magazine. In '92, when my family got a PC-AT, the same game was solved in 5 minutes, so to this day that PC is still my psicological reference of "all the power I need". I enjoyed a Prolog compiler in that system, and my intuition says Haskell could also fit there. And, at the same time, today operating systems are happy to announce how easily they turn your dual-core into a great video cassette :( Anyway, what I would like would be a "theoretical" answer. Is there something fundamentally diferent between a C compiler and a Haskell one that makes the former fits into 30Kb but not the other? If so, what compiler algorithms are those, and what are they theorical needs? I really don't need an easy answer. If you guys just sugest me computer theory books I will be happy to look for them, but today I wouldn't know what to read. Best, Maurício ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
On Mon, 2007-10-22 at 01:12 +0100, Lennart Augustsson wrote: > There's nothing wrong with Haskell types. It's the terms that make > Haskell types an inconsistent logic. Logics are what are consistent or not, so saying the logic Haskell's type system corresponds to is inconsistent is all that can be said. Somewhere there is an axiom in it that makes forall a.(a -> a) -> a hold. Usually, we just take that directly as the axiom (i.e. the existence of fix). > But that doesn't mean that the C-H correspondence doesn't have any > insight to offer. Which is certainly not what I said at all. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: How much of Haskell was possible 20 years ago?
On Oct 21, 2007, at 21:31 , Maurí cio wrote: Anyway, what I would like would be a "theoretical" answer. Is there something fundamentally diferent between a C compiler and a Haskell one that makes the former fits into 30Kb but not the other? If I am not sure *modern* C would have fit into 30KB. Back then, C was the original K&R C, which was in many ways much lower level than ANSI C; those compilers could be quite compact. (I remember playing with SmallC, which compiled a subset of C which covered 95% of what features programmers actually used back then and was extremely compact.) There are two reasons ANSI C would be unlikely to fit: modern C compilers do optimization, which (aside from very simplistic "peephole" optimization, needs lots of memory), and the ANSI C type system (such as it is) is complex enough to require more memory to deal with properly. In early K&R C (which was still relatively close to its untyped predecessor BCPL), many things were "untyped" and effectively (int) (a machine word); non-(int) integral types were promoted to (int), and (float) was promoted to (double), wherever possible to simplify things for the compiler. You could use more complex types to some extent, but they tended to perform poorly enough that much effort went into avoiding them. Even in later K&R C (which still did type promotion but deprecated "untyped" functions and removed "untyped" variables), people avoided using even (long int) except through pointers because they were so expensive to use as function arguments and return values (and some compilers, mostly on some mainframe architectures, *couldn't* return (long int) safely). Both of these also apply to Haskell. In particular, you can do a naive compilation of Haskell code but it will perform very poorly --- Haskell *needs* a good optimizer. (Compare the performance of code compiled with unregisterised GHC to that compiled with normal, highly optimized GHC sometime.) Additionally, even Haskell98 can need quite a bit of memory to do type unification if you don't explicitly specify every type everywhere; and this gets much worse with the extensions in modern Haskell (in particular, functional dependencies complicate type unification). There may be theory issues which also impact the question, but in large part it's not theory so much as practical concerns. -- 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] Re: How much of Haskell was possible 20 years ago?
On Sun, Oct 21, 2007 at 10:02:25PM -0400, Brandon S. Allbery KF8NH wrote: > On Oct 21, 2007, at 21:31 , Maurí cio wrote: >> Anyway, what I would like would be a "theoretical" >> answer. Is there something fundamentally diferent >> between a C compiler and a Haskell one that makes >> the former fits into 30Kb but not the other? If Another large part of the issue is that C compilers tend to be written in C, while Haskell compilers tend to be written in Haskell. C, as a lower level language, strongly encourages programmers to think about issues such as space and time usage, at the cost of much more development time. In terms of simple complexity, the difference isn't all that big - the original NHC (a minimalistic haskell compiler) weighed in at around 9 kloc. How big is your favorite C compiler in source-code terms? Stefan signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] [Fwd: undecidable & overlapping instances: a bug?]
Iavor Diatchki writes: > Hello, > > On 10/19/07, Martin Sulzmann <[EMAIL PROTECTED]> wrote: > > Simon Peyton-Jones writes: > > > ... > > > Like you, Iavor, I find it very hard to internalise just why (B) and > > (C) are important. But I believe the paper gives examples of why they > > are, and Martin is getting good at explaining it. Martin: can you give an > > example, once more, of the importance of (B) (=fullness)? > > > > > > > Fullness (B) is a necessary condition to guarantee that the constraint > > solver (aka CHR solver) derived from the type class program is confluent. > > > > Here's an example (taken from the paper). > > > > class F a b c | a->b > > instance F Int Bool Char > > instance F a b Bool => F [a] [b] Bool > > > > The FD is not full because the class parameter c is not involved in > > the FD. We will show now that the CHR solver is not confluent. > > > > Here is the translation to CHRs (see the paper for details) > > > > rule F a b1 c, F a b2 d ==> b1=b2 -- (FD) > > rule F Int Bool Char<==> True -- (Inst1) > > rule F Int a b ==> a=Bool -- (Imp1) > > rule F [a] [b] Bool <==> F a b Bool -- (Inst2) > > rule F [a] c d ==> c=[b] -- (Imp2) > > > > > > The above CHRs are not confluent. For example, > > there are two possible CHR derivations for the initial > > constraint store F [a] [b] Bool, F [a] b2 d > > > > F [a] [b] Bool, F [a] b2 d > > -->_FD (means apply the FD rule) > > F [a] [b] Bool, F [a] [b] d , b2=[b] > > --> Inst2 > > F a b Bool, F [a] [b] d , b_2=[b] (*) > > > > > > Here's the second CHR derivation > > > > F [a] [b] Bool, F [a] b2 d > > -->_Inst2 > > F a b Bool, F [a] b2 d > > -->_Imp2 > > F a b Bool, F [a] [c] d, b2=[c] (**) > > > > > > (*) and (**) are final stores (ie no further CHR are applicable). > > Unfortunately, they are not logically equivalent (one store says > > b2=[b] whereas the other store says b2=[c]). > > But what is wrong with applying the following logical reasoning: > Well, you apply the above CHRs from left to right *and* right to left. In contrast, I apply the CHRs only from left to right. > Starting with (**): > F a b Bool, F [a] [c] d, b2=[c] > (by inst2) > F a b Bool, F [a] [c] d, b2=[c], F [a] [b] Bool > (by FD) > F a b Bool, F [a] [c] d, b2=[c], F [a] [b] Bool, [c] = [b] > (applying equalities and omitting unnecessary predicates) > F [a] [b] Bool, F [a] b2 d > (...and then follow your argument to reach (*)...) > > Alternatively, if we start at (*): > F a b Bool, F [a] [b] d , b_2=[b] > (by inst2) > F a b Bool, F [a] [b] d , b_2=[b], F [a] [b] Bool > (applying equalities, rearranging, and omitting unnecessary predicates) > F [a] [b] Bool, F [a] b_2 d > (... and then follow you reasoning to reach (**) ...) > > So it would appear that the two sets of predicates are logically equivalent. > I agree that the two sets F a b Bool, F [a] [b] d , b_2=[b] (*) and F a b Bool, F [a] [c] d, b2=[c] (**) are logically equivalent wrt the above CHRs (see your proof). The problem/challenge we are facing is to come up with a confluent and terminating CHR solver. Why is this useful? (1) We get a deterministic solver (2) We can decide whether two constraints C1 and C2 are equal by solving (a) C1 -->* D1 and (b) C2 -->* D2 and then checking that D1 and D2 are equivalent. The equivalence is a simple syntactic check here. The CHR solving strategy applies rules in a fixed order (from left to right). My example shows that under such a strategy the CHR solver becomes non-confluent for type class programs with non-full FDs. We can show non-confluence by having two derivations starting with the same initial store leading to different final stores. Recall: F [a] [b] Bool, F [a] b2 d -->* F a b Bool, F [a] [b] d , b_2=[b] (*) F [a] [b] Bool, F [a] b2 d -->* F a b Bool, F [a] [c] d, b2=[c] (**) I said > > (*) and (**) are final stores (ie no further CHR are applicable). > > Unfortunately, they are not logically equivalent (one store says > > b2=[b] whereas the other store says b2=[c]). More precisely, I meant here that (*) and (**) are not logically equivalent *not* taking into account the above CHRs. This means that (*) and (**) are different (syntactically). > > To conclude, fullness is a necessary condition to establish confluence > > of the CHR solver. Confluence is vital to guarantee completeness of > > type inference. > > > > > > I don't think that fullness is an onerous condition. > > I agree with you that, in practice, many classes probably use "full" > FDs. However, these extra conditions make the system more > complicated, and we should make clear what exactly are we getting in > return for the added complexity. > You can get rid of non-full FDs (see the paper). BTW, type fu
Re: [Haskell-cafe] Polymorphic (typeclass) values in a list?
On 10/22/07, Tim Docker <[EMAIL PROTECTED]> wrote: > TJ: > > > After all, sometimes all you need to know about a list is that > > all the elements support a common set of operations. If I'm > > implementing a 3d renderer for example, I'd like to have > > > > class Renderable a where > > render :: a -> RasterImage > > > > scene :: Renderable a => [a] > > > Everyone has launched into explanations of how to use existentials > to do this, but you may be happy in just haskell 98. In the above, > you could just have: > > scene :: [RasterImage] > > Laziness will ensure that the computation/storage of the images > will not occur until they are used. > > Tim > Ah... indeed it can, in this case. It won't work if class Renderable also has a method for saving to file, etc, I suppose, unless scene :: [(RasterImage,IO (),...whatever other operations...)] Thanks for the heads up :) TJ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] [Fwd: undecidable & overlapping instances: a bug?]
Mark P Jones writes: > Hi All, > > Here are my responses to the recent messages, starting with some > summary comments: > > - I agree with Martin that the condition I posted a few days ago is >equivalent to the "*refined* weak coverage condition" in your >paper. The "refined" tag here is important---I missed it the >first time and thought he was referring to the WCC at the start of >Section 6.1, and I would strongly recommend against using that >(unrefined) version. I confess that I haven't read the paper >carefully enough to understand why you included that first WCC at >all; I don't see any reason why you would want to use that >particular condition in a practical implementation, and I don't >see any advantages to it from a theoretical perspective either. >(Maybe you just used it as a stepping stone to help motivate the >refined WCC?) > It's a stepping stone but WCC on it's own is useful to recover termination (see the "zip" example in the paper). > - I believe that the refined WCC (or the CC or even the original WCC >if you really want) are sufficient to ensure soundness. I don't >agree that the (B) restriction to "full" FDs is necessary. > > - I think it is dangerous to tie up soundness with questions about >termination. The former is a semantic property while the latter >has to do with computability. Or, from a different perspective, >soundness is essential, while termination/decidability is "only" >desirable. I know that others have thought more carefully than >I have about conditions on the form of class and instance >declarations that will guarantee decidability and I don't have >much to say on that topic in what follows. However, I will >suggest that one should start by ensuring soundness and then, >*separately*, consider termination. (Of course, it's perfectly >ok---just not essential---if conditions used to ensure soundness >can also be used to guarantee termination.) > Well, decidability and completeness matters if we care about automatic type inference. Given some input program we'd like that to have a *decidable* algorithm which computes a type for every well-typed program (*soundness*) and yields failure if the program is ill-typed (*completeness*). In "Simplifying and Improving Qualified Types." you give indeed a sound, decidable and complete type inference algorithm *if* the proof theory among constraints in some theory of qualified types is sound, decidable and complete. My main concern is to establish sufficient conditions such that the proof theory is sound, decidable and complete. That is, there's a decidable algorithm which says yes if QT |= C1 -> C2 and otherwise no where QT |= C1 -> C2 means that in the qualified theory QT constraint C1 entails constraint C2. I think that our works are fairly complementary. Or are you saying you've already given such an algorithm (which I indeed must have missed). I believe that you are offended by my statement that > Confluence is vital to guarantee completeness of type inference. Let me clarify. Confluence is one of the suffient conditions to guarantee completeness of CHR-based type inference. Apologies for any confusion caused by my previous statement. There are clearly other approaches possible to obtain a sound, decidable and complete proof theory (and therefore to obtain sound, decidable and complete type inference). But I yet need to see concrete results which match the CHR-based approach/results described in: Understanding Functional Dependencies via Constraint Handling Rules Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones and Peter J. Stuckey In Journal of Functional Programming, 2007 Martin > Stop reading now unless you're really interested in the details! > I'm going to start by explaining some key (but hopefully > unsurprising) ideas before I respond in detail to the example > that Martin posted. > > Interpreting Class, Instance, and Dependency Decls: > --- > I'll start by observing that Haskell's class, instance, and > functional dependency declarations all map directly to formulas in > standard predicate logic. The correspondence is straightforward, so > I'll just illustrate it with some examples: > >Declaration Formula >--- --- >class Eq a => Ord a forall a. Ord a => Eq a >instance Eq a => Eq [a] forall a. Eq a => Eq [a] >class C a b | a -> b forall a, b. C a b /\ C a c => b = c > > This correspondence between declarations and formulas seems to be > very similar to what you did in the paper using CHRs. I haven't > read the paper carefully enough to know what extra mileage and/or > problems you get by using CHRs. To me, predicate logic seems more > natural, but I don't think that matters here---I just wanted to > acknowled
RE: [Haskell-cafe] Polymorphic (typeclass) values in a list?
TJ:
> Ah... indeed it can, in this case. It won't work if class Renderable
> also has a method for saving to file, etc, I suppose, unless scene ::
> [(RasterImage,IO (),...whatever other operations...)]
In this case I would generally create a record:
data Renderable = Renderable {
image :: RasterImage,
saveToFile :: FilePath -> IO (),
... etc ...
}
scene :: [Renderable]
You may then like to add a type class to turn things into renderables:
class IsRenderable where
toRenderable :: a -> Renderable
instance IsRendeable Point where ...
instance IsRenderable Line where ...
It depends on your needs, but in my limited experience, records are
often more convenient for emulating OO-style programming than are type
classes.
Tim
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
