[Haskell-cafe] Haskell philosophy question
Hello, I am confused between Haskell as delineated in the Haskell Report VS ghc pragmas which extend Haskell beyond the Haskell Report. I am sure I am not the first to ask. Caveat: on my part, I am not against innovation/extensions, but I don't like to see language bloat. This is not a negative/pegorative statement just a challenging one. Kind regards, vasili ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell philosophy question
On May 17, 2009, at 02:32 , Vasili I. Galchin wrote: I am confused between Haskell as delineated in the Haskell Report VS ghc pragmas which extend Haskell beyond the Haskell Report. I am sure I am not the first to ask. Caveat: on my part, I am not against innovation/extensions, but I don't like to see language bloat. This is not a negative/pegorative statement just a challenging one. Remember that Haskell is *also* a research language; this means it regularly gets new features intended to allow research into various type system extensions. Some of these stick (the original type classes, and later multiple parameter type classes), some flop (linear implicit parameters), some hang around for a while before being replaced by something (hopefully) better (functional dependencies vs. type families). -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon universityKF8NH PGP.sig Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Cabal, Time GHC 6.10.2
I get d...@linux-6ofq:~/asn1 runghc Setup.hs configure Configuring PER-0.0.20... Setup.hs: At least the following dependencies are missing: time -any -any but I have time d...@linux-6ofq:~/asn1 ghc-pkg list | grep time old-locale-1.0.0.1, old-time-1.0.0.2, packedstring-0.1.0.1, time-1.1.2.4 I think I can see why cabal isn't finding it: ghc-pkg dump --global | grep time-1.1.2.4 finds nothing and I believe that is what cabal uses to find things. What's not clear is what I do to fix things. Go back to 6.10.1? Thanks, Dominic. d...@linux-6ofq:~/asn1 ghc --version The Glorious Glasgow Haskell Compilation System, version 6.10.2 d...@linux-6ofq:~/asn1 ghc-pkg --version GHC package manager version 6.10.2 Here's my .cabal file. Name:PER Version: 0.0.20 License: BSD3 Author: Dominic Steinitz Maintainer: dominic.stein...@blueyonder.co.uk Copyright: Dominic Steinitz 2003 - 2009 Stability: Alpha Category:Language Homepage:http://www.haskell.org/asn1 Synopsis:ASN.1 PER support for Haskell Description: A formal and executable specification of the Packed Encoding Rules (PER) for ASN.1 build-depends: binary-strict == 0.4.2, bytestring, mtl, containers, time, pretty, base build-type: custom Exposed-Modules: Language.ASN1.PER.Integer Language.ASN1.PER.GenerateC Executable: PERTest Main-Is: PERTest.hs ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Can't install happs-tutorial because syb-with-class fails to install
Data/Generics/SYB/WithClass/Derive.hs:187:26: Couldn't match expected type `Pred' against inferred type `Type' Expected type: PredQ Inferred type: TypeQ In the first argument of `map', namely `dataCxt' In the first argument of `(++)', namely `map dataCxt dataCxtTypes' Data/Generics/SYB/WithClass/Derive.hs:198:36: Couldn't match expected type `Pred' against inferred type `Type' Expected type: Q Pred Inferred type: TypeQ In the expression: conT 'Data `appT` typ In the first argument of `map', namely `(\ typ - conT 'Data `appT` typ)' Data/Generics/SYB/WithClass/Derive.hs:227:38: Couldn't match expected type `Name' against inferred type `TyVarBndr' Expected type: [Name] Inferred type: [TyVarBndr] In the expression: ps In the first argument of `return', namely `(n, ps, map conA cs)' cabal: Error: some packages failed to install: syb-with-class-0.5.1 failed during the building phase. The exception was: exit: ExitFailure 1 -- Colin Adams Preston Lancashire ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal, Time GHC 6.10.2
On Sun, 2009-05-17 at 09:17 +0100, Dominic Steinitz wrote: I get d...@linux-6ofq:~/asn1 runghc Setup.hs configure Configuring PER-0.0.20... Setup.hs: At least the following dependencies are missing: time -any -any but I have time d...@linux-6ofq:~/asn1 ghc-pkg list | grep time old-locale-1.0.0.1, old-time-1.0.0.2, packedstring-0.1.0.1, time-1.1.2.4 I think I can see why cabal isn't finding it: ghc-pkg dump --global | grep time-1.1.2.4 finds nothing and I believe that is what cabal uses to find things. The default for runghc Setup.hs configure is --global, but the default for cabal configure is --user. So if you're using the cabal program to install packages, then you can also us it to configure other packages. If for you need to use the runghc Setup.hs interface (e.g. in some system build scripts) and you want it to pick up packages from the user package db then use the --user flag. If you're constantly having to use the runghc Setup.hs interface and doing per-user installs is a pain then you can set the default for the cabal program to be global installs in the cabal config file (~/.cabal/config). I'll add this issue to the FAQ, it come up enough. If anyone else reading would like to eliminate this FAQ, then implementing this ticket is the answer: suggest use of --user if configure fails with missing deps that are in the user db http://hackage.haskell.org/trac/hackage/ticket/384 Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Linkage errors in scenegraph
Am Sonntag, 17. Mai 2009 01:07:55 schrieb Gregory D. Weber: I'd like to get the scenegraph package (http://hackage.haskell.org/cgi-bin/hackage-scripts/package/scenegraph) to work, but am encountering linkage errors. [...] Also, I notice that in the cabal file for scenegraph, the list of exposed modules Exposed-Modules: Graphics.SceneGraph, Graphics.SceneGraph.Basic, Graphics.SceneGraph.Vector, Graphics.SceneGraph.Render, Graphics.SceneGraph.SimpleViewport, Graphics.SceneGraph.GraphViz, Graphics.SceneGraph.Library, Graphics.SceneGraph.Dump, Graphics.SceneGraph.Textures does not include Graphics.SceneGraph.Matrix, but that should only mean that I can't call functions of that module directly -- not that the other SceneGraph modules can't call them -- right? [...] That basically means that the scenegraph package is broken. ;-) Internal modules have to be listed in other-modules:, a section the Cabal file doesn't contain. As a quick fix, you can add all missing modules in this section, but this should of course be fixed in the official package, too. http://www.haskell.org/cabal/release/cabal-latest/doc/users- guide/authors.html#buildinfo Cheers, S. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Data.Binary and little endian encoding
Am Freitag, 15. Mai 2009 06:37:22 schrieb Don Stewart: timd: On a related matter, I am using Data.Binary to serialise data from haskell for use from other languages. [...] [...] Yep, it's possible, just not portably so. Google for Data.Binary IEEE discussions. I think this topic pops up over and over again, and the proposed solutions are no solutions at all, neither from a performance point of view, nor from an ease of use point of view. Proposing insane bit fiddling by hand when all one technically needs is often a peek or poke amounts to simply ignoring an API problem. ;-) I think most problems can be fixed in a rather pragmatic way by adding a few functions to the binary package: Add to Data.Binary.Builder: putFloatIEEEbe :: Float - Builder putDoubleIEEEbe :: Double - Builder putFloatIEEEle :: Float - Builder putDoubleIEEEle :: Double - Builder putFloatIEEEhost :: Float - Builder putDoubleIEEEhost :: Double - Builder Add to Data.Binary.Get: getFloatIEEEbe :: Get Float getDoubleIEEEbe :: Get Double getFloatIEEEle :: Get Float getDoubleIEEEle :: Get Double getFloatIEEEhost :: Get Float getDoubleIEEEhost :: Get Double Add to Data.Binary.Put: putFloatIEEEbe :: Float - Put putDoubleIEEEbe :: Double - Put putFloatIEEEle :: Float - Put putDoubleIEEEle :: Double - Put putFloatIEEEhost :: Float - Put putDoubleIEEEhost :: Double - Put The *host functions are basically peek/poke for most platforms. The *le/*be functions can use peek/poke if the endianess matches (compile time decision) *and* the alignment is OK for the given platform (runtime decision). Non-IEEE platforms always have to do the bit fiddling internally, but all this is hidden behind the above API. IIRC I have proposed something similar 1-2 years ago, but I can't remember any reason why this hasn't been implemented. Any comments on the above functions? One final remarks: I think the low level functions of the binary package should really keep the notions of endianess and alignment constraints separate, something which isn't done currently: The *host functions have alignment restrictions, the *be/*le functions don't. There is no good reason for this non-orthogonality. Cheers, S. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can't install happs-tutorial because syb-with-class fails to install
False alarm. It compiles OK with ghc 6.10.3. The failure was with ghc 6.11.20090404. -- Colin Adams Preston Lancashire ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Data.Binary and little endian encoding
Sven.Panne: Am Freitag, 15. Mai 2009 06:37:22 schrieb Don Stewart: timd: On a related matter, I am using Data.Binary to serialise data from haskell for use from other languages. [...] [...] Yep, it's possible, just not portably so. Google for Data.Binary IEEE discussions. I think this topic pops up over and over again, and the proposed solutions are no solutions at all, neither from a performance point of view, nor from an ease of use point of view. Proposing insane bit fiddling by hand when all one technically needs is often a peek or poke amounts to simply ignoring an API problem. ;-) I think most problems can be fixed in a rather pragmatic way by adding a few functions to the binary package: Add to Data.Binary.Builder: putFloatIEEEbe :: Float - Builder putDoubleIEEEbe :: Double - Builder putFloatIEEEle :: Float - Builder putDoubleIEEEle :: Double - Builder putFloatIEEEhost :: Float - Builder putDoubleIEEEhost :: Double - Builder Add to Data.Binary.Get: getFloatIEEEbe :: Get Float getDoubleIEEEbe :: Get Double getFloatIEEEle :: Get Float getDoubleIEEEle :: Get Double getFloatIEEEhost :: Get Float getDoubleIEEEhost :: Get Double Add to Data.Binary.Put: putFloatIEEEbe :: Float - Put putDoubleIEEEbe :: Double - Put putFloatIEEEle :: Float - Put putDoubleIEEEle :: Double - Put putFloatIEEEhost :: Float - Put putDoubleIEEEhost :: Double - Put The *host functions are basically peek/poke for most platforms. The *le/*be functions can use peek/poke if the endianess matches (compile time decision) *and* the alignment is OK for the given platform (runtime decision). Non-IEEE platforms always have to do the bit fiddling internally, but all this is hidden behind the above API. IIRC I have proposed something similar 1-2 years ago, but I can't remember any reason why this hasn't been implemented. Any comments on the above functions? Patches are welcome. One final remarks: I think the low level functions of the binary package should really keep the notions of endianess and alignment constraints separate, something which isn't done currently: The *host functions have alignment restrictions, the *be/*le functions don't. There is no good reason for this non-orthogonality. That seems reasonable. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Haskell philosophy question
vigalchin: Hello, I am confused between Haskell as delineated in the Haskell Report VS ghc pragmas which extend Haskell beyond the Haskell Report. I am sure I am not the first to ask. Caveat: on my part, I am not against innovation/extensions, but I don't like to see language bloat. This is not a negative/pegorative statement just a challenging one. They add new features, which are useful for determining what features are useful :) -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Building a better dog house?
I was just looking at my UML (Unified Modeling Language) User Guide and discovered this: The number of object-oriented methods increased from fewer than 10 to more than 50 during the period between 1989 and 1994. pg. xviii, Booch, Rumbaugh, Jacobson, 1999 Is there a modeling methodology recommended for functional languages? Michael ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] [ANN] Safe Lazy IO in Haskell
From the documentation: LI could be a strict monad and a strict applicative functor. However it is not a lazy monad nor a lazy applicative functor as required Haskell. Hopefully it is a lazy (pointed) functor at least. I'd like to understand this better -- how is LI incompatible with being a lazy monad, exactly? -- Jason Dusek ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Haskell philosophy question
Vasili I. Galchin vigalc...@gmail.com writes: Hello, I am confused between Haskell as delineated in the Haskell Report VS ghc pragmas which extend Haskell beyond the Haskell Report. Pragmas are part of the report, and while I agree that using them for extensions is stretching the meaning a bit, it's clearly the best way of doing it -- they're not supposed to change the semantics of the language as defined, but it doesn't say anything about what they do to stuff that isn't part of the language. I am sure I am not the first to ask. Caveat: on my part, I am not against innovation/extensions, but I don't like to see language bloat. Me neither, but many of the extensions are for things that hadn't been invented (or perhaps finalised, such as heirarchical modules, IIRC) when the standard was written, and which make the language more expressive, which is a worthwhile aim. Among the stated aims of Haskell was to be a platform for language development. Pragmas keep the experimental stuff separate from the stuff one can rely on because it's part of H98. -- Jón Fairbairn jon.fairba...@cl.cam.ac.uk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] ANN: TxtSushi 0.1
Hello Haskell Cafe I have released the first version of TxtSushi which is a collection of command line utils (written in haskell of course) for processing tab-delimited and CSV files. It includes a util for doing SQL SELECTs on flat files. This is my first haskell project and feedback of all kinds is appreciated. Home Page: http://www.keithsheppard.name/txt-sushi Darcs Repository: http://patch-tag.com/r/txt-sushi/home Issue Tracking: http://code.google.com/p/txt-sushi I would like to say thanks to the haskell-beginners contributors, the author of Learn you a Haskell and the author of the parsec library all of which were very helpful. Regards Keith ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: TxtSushi 0.1
This is crazy cool! I will now use your project as an example of what one can do as his first project in Haskell; I think doing SQL on CSV files definitely counts as a huge success story! 2009/5/17 Keith Sheppard keiths...@gmail.com: Hello Haskell Cafe I have released the first version of TxtSushi which is a collection of command line utils (written in haskell of course) for processing tab-delimited and CSV files. It includes a util for doing SQL SELECTs on flat files. This is my first haskell project and feedback of all kinds is appreciated. Home Page: http://www.keithsheppard.name/txt-sushi Darcs Repository: http://patch-tag.com/r/txt-sushi/home Issue Tracking: http://code.google.com/p/txt-sushi I would like to say thanks to the haskell-beginners contributors, the author of Learn you a Haskell and the author of the parsec library all of which were very helpful. Regards Keith ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: TxtSushi 0.1
Keith Sheppard wrote: I have released the first version of TxtSushi which is a collection of command line utils (written in haskell of course) for processing tab-delimited and CSV files. It includes a util for doing SQL SELECTs on flat files. This is my first haskell project and feedback of all kinds is appreciated. Home Page: http://www.keithsheppard.name/txt-sushi Darcs Repository: http://patch-tag.com/r/txt-sushi/home Issue Tracking: http://code.google.com/p/txt-sushi Nice! Have you considered putting this on Hackage? That is most useful for users of your code. I saw you already cabalized the code, so it should suffice to upload it. Cheers -- Jochem Berndsen | joc...@functor.nl GPG: 0xE6FABFAB ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: TxtSushi 0.1
By the way: As I see from the sources, your code uses external sort? But using String's much defeats the purpose of it, anyway, because their performance is so bad that if you feed your program a file that is larger than can be sorted in memory, sorting it externally using String's will anyway take much more time then you are likely to be comfortable waiting. You should consider switching to ByteString's, and beware memory leaks. 2009/5/17 Keith Sheppard keiths...@gmail.com: Hello Haskell Cafe I have released the first version of TxtSushi which is a collection of command line utils (written in haskell of course) for processing tab-delimited and CSV files. It includes a util for doing SQL SELECTs on flat files. This is my first haskell project and feedback of all kinds is appreciated. Home Page: http://www.keithsheppard.name/txt-sushi Darcs Repository: http://patch-tag.com/r/txt-sushi/home Issue Tracking: http://code.google.com/p/txt-sushi I would like to say thanks to the haskell-beginners contributors, the author of Learn you a Haskell and the author of the parsec library all of which were very helpful. Regards Keith ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: TxtSushi 0.1
Thanks for the encouraging reply! By the way, I was part way through writing my own code for external sorting which I don't actually use yet except from some test executable (joincol.hs). I'm very glad to see that there is already a library that does this though, so in my next version I will dump the custom code and use the external sort package. Also I will look into making the switch to ByteStrings. Thanks Keith On Sun, May 17, 2009 at 11:53 AM, Eugene Kirpichov ekirpic...@gmail.com wrote: By the way: As I see from the sources, your code uses external sort? But using String's much defeats the purpose of it, anyway, because their performance is so bad that if you feed your program a file that is larger than can be sorted in memory, sorting it externally using String's will anyway take much more time then you are likely to be comfortable waiting. You should consider switching to ByteString's, and beware memory leaks. 2009/5/17 Keith Sheppard keiths...@gmail.com: Hello Haskell Cafe I have released the first version of TxtSushi which is a collection of command line utils (written in haskell of course) for processing tab-delimited and CSV files. It includes a util for doing SQL SELECTs on flat files. This is my first haskell project and feedback of all kinds is appreciated. Home Page: http://www.keithsheppard.name/txt-sushi Darcs Repository: http://patch-tag.com/r/txt-sushi/home Issue Tracking: http://code.google.com/p/txt-sushi I would like to say thanks to the haskell-beginners contributors, the author of Learn you a Haskell and the author of the parsec library all of which were very helpful. Regards Keith ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: TxtSushi 0.1
Thanks! Good advice, I will do that. On Sun, May 17, 2009 at 11:49 AM, Jochem Berndsen joc...@functor.nl wrote: Keith Sheppard wrote: I have released the first version of TxtSushi which is a collection of command line utils (written in haskell of course) for processing tab-delimited and CSV files. It includes a util for doing SQL SELECTs on flat files. This is my first haskell project and feedback of all kinds is appreciated. Home Page: http://www.keithsheppard.name/txt-sushi Darcs Repository: http://patch-tag.com/r/txt-sushi/home Issue Tracking: http://code.google.com/p/txt-sushi Nice! Have you considered putting this on Hackage? That is most useful for users of your code. I saw you already cabalized the code, so it should suffice to upload it. Cheers -- Jochem Berndsen | joc...@functor.nl GPG: 0xE6FABFAB ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Free theorems for dependent types?
Hello, Is there any research on applying free theorems / parametricity to type systems more complex than System F; namely, Fomega, or calculus of constructions and alike? This seems very promising to me for the following reason: Take the free theorem for 'sort::(a-a-Bool)-[a]-[a]'. The theorem could possibly be a lot more powerful if there were a way to encode in the type of 'sort' that it accepts a reflexive transitive antisymmetric predicate, but the only way to express that is with dependent types. Looks like the only thing one needs to add to System F is the relational translation rule for a dependent product; but I haven't tried doing it myself. -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Building a better dog house?
michael rice wrote: I was just looking at my UML (Unified Modeling Language) User Guide and discovered this: The number of object-oriented methods increased from fewer than 10 to more than 50 during the period between 1989 and 1994. pg. xviii, Booch, Rumbaugh, Jacobson, 1999 Is there a modeling methodology recommended for functional languages? Michael UML of course is not a methodology, its a language. Rational Unified Process (RUP) is a methodology. There is no recommended methodology for functional programming, but large chunks of RUP and most similar methodologies have little to do with OO programming, and therefore could be used as-is. All the project planning, configuration management, requirements management and so on will work just fine. When it comes to the software design in functional languages I find it best to start by looking for a domain analysis of the problem (something that RUP includes as well, if I recall correctly). Then try to translate that domain analysis into an embedded domain specific language (EDSL). Ideally the EDSL should allow you to describe anything that is physically or logically possible in the domain, but nothing that is impossible. Then you can go ahead and create your software by translating the requirements directly into the EDSL. Paul. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Free theorems for dependent types?
On Sun, 17 May 2009 23:10:12 +0400 Eugene Kirpichov ekirpic...@gmail.com wrote: Is there any research on applying free theorems / parametricity to type systems more complex than System F; namely, Fomega, or calculus of constructions and alike? Yes. I did some research into it as part of my master's thesis, the final version of which is not quite ready yet. Basically, free theorems in the Calculus of Constructions can be substantially more complicated, because they have to exclude certain dependent types in order to be valid. So much so that I do not think that they are necessarily worthwhile to use in proofs. But that is just an intuition, and I have not done enough different kinds of proofs to state this with any confidence. -- Robin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Free theorems for dependent types?
I'm glad that someone is doing research in that direction! Are your results so far applicable to create a free theorem for that example with sortBy? 2009/5/17 Robin Green gree...@greenrd.org: On Sun, 17 May 2009 23:10:12 +0400 Eugene Kirpichov ekirpic...@gmail.com wrote: Is there any research on applying free theorems / parametricity to type systems more complex than System F; namely, Fomega, or calculus of constructions and alike? Yes. I did some research into it as part of my master's thesis, the final version of which is not quite ready yet. Basically, free theorems in the Calculus of Constructions can be substantially more complicated, because they have to exclude certain dependent types in order to be valid. So much so that I do not think that they are necessarily worthwhile to use in proofs. But that is just an intuition, and I have not done enough different kinds of proofs to state this with any confidence. -- Robin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Building a better dog house?
Hi Paul, I've been away from software design for more than a decade and have fallen behind on what's currently being used. I wasn't even aware of RUP. Thanks for the info. Michael --- On Sun, 5/17/09, Paul Johnson p...@cogito.org.uk wrote: From: Paul Johnson p...@cogito.org.uk Subject: Re: [Haskell-cafe] Building a better dog house? To: michael rice nowg...@yahoo.com Cc: haskell-cafe@haskell.org Date: Sunday, May 17, 2009, 3:26 PM michael rice wrote: I was just looking at my UML (Unified Modeling Language) User Guide and discovered this: The number of object-oriented methods increased from fewer than 10 to more than 50 during the period between 1989 and 1994. pg. xviii, Booch, Rumbaugh, Jacobson, 1999 Is there a modeling methodology recommended for functional languages? Michael UML of course is not a methodology, its a language. Rational Unified Process (RUP) is a methodology. There is no recommended methodology for functional programming, but large chunks of RUP and most similar methodologies have little to do with OO programming, and therefore could be used as-is. All the project planning, configuration management, requirements management and so on will work just fine. When it comes to the software design in functional languages I find it best to start by looking for a domain analysis of the problem (something that RUP includes as well, if I recall correctly). Then try to translate that domain analysis into an embedded domain specific language (EDSL). Ideally the EDSL should allow you to describe anything that is physically or logically possible in the domain, but nothing that is impossible. Then you can go ahead and create your software by translating the requirements directly into the EDSL. Paul. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] ANNOUNCE: mathlink-2.0.0.3
Already posted to the Haskell list but dons suggested I post to the cafe, as well... All: mathlink is a library for writing Mathematica packages in Haskell. One simply writes some functions of type: (MLGet a, MLPut b) = a - IO b and provides a package specification in a simple DSL that mimics that of Mathematica's mprep utility. The result is a program that exposes functions that can be called from Mathematica. This is a complete rewrite of my original implementation and more closely captures the functionality I originally intended. I've only tested it on my own platform (64-bit Linux), but I've taken pains to make sure the code should run on any platform. (The only real issue in the code is picking the right functions to call when marshaling Ints.) Please report any tweaks required to get it to work on your platform. (That is, of course, only if, in fact, there are any other users out there. Right now, as far as I know, I'm it.) I'd also just like to hear from any Haskellers out there that also use Mathematica on a regular basis. Ping me if you're one. --Tracy ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Free theorems for dependent types?
This word has piqued my interest, I've hear it tossed around the community quite a bit, but never fully understood what it meant. What exactly is a 'free theorem'? Eugene Kirpichov wrote: Hello, Is there any research on applying free theorems / parametricity to type systems more complex than System F; namely, Fomega, or calculus of constructions and alike? This seems very promising to me for the following reason: Take the free theorem for 'sort::(a-a-Bool)-[a]-[a]'. The theorem could possibly be a lot more powerful if there were a way to encode in the type of 'sort' that it accepts a reflexive transitive antisymmetric predicate, but the only way to express that is with dependent types. Looks like the only thing one needs to add to System F is the relational translation rule for a dependent product; but I haven't tried doing it myself. begin:vcard fn:Joseph Fredette n:Fredette;Joseph adr:Apartment #3;;6 Dean Street;Worcester;Massachusetts;01609;United States of America email;internet:jfred...@gmail.com tel;home:1-508-966-9889 tel;cell:1-508-254-9901 x-mozilla-html:FALSE url:lowlymath.net, humbuggery.net version:2.1 end:vcard ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Free theorems for dependent types?
Free theorem's are theorems about functions that rely only on parametricity. For example, consider any function f with the type forall a. a - a From its type, I can tell you directly that this theorem holds: forall g :: A - B, x :: A, f (g x) = g (f x) (Note that the f on the left is B - B, the f on the right is A - A). The term was popularized by Philip Wadler, in his paper Theorems for Free! [1]. He noticed that many of the properties of functions that one likes to prove come for free from their parametric type. For example, it's useful to know that reverse (map fromEnum xs) == map fromEnum (reverse xs) But this theorem comes for free from the type of reverse! Given any - f :: forall a. [a] - [a] - g :: A - B - xs :: [A] we have the free theorem - f (map g xs) = map g (f xs). What this is saying is that any function (forall a. [a] - [a]) can't do a whole lot; it can inspect the structure of the list it has been given, and rearrange, duplicate, and/or remove some elements. But the output list can only contain elements from the input list, without inspecting the elements themselves. Therefore, if f [1,2,3] == [1,1,2] then f abc == aab and f [True, True, False] == [True, True, True] and f [ [], [1], [1,2] ] == [ [], [], [1,2] ] and so on. Therefore mapping some pure function over the result can be done before or after applying f; and we don't have to know *anything* about f, aside from its type, to prove this. -- ryan [1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875 On Sun, May 17, 2009 at 7:51 PM, Joe Fredette jfred...@gmail.com wrote: This word has piqued my interest, I've hear it tossed around the community quite a bit, but never fully understood what it meant. What exactly is a 'free theorem'? Eugene Kirpichov wrote: Hello, Is there any research on applying free theorems / parametricity to type systems more complex than System F; namely, Fomega, or calculus of constructions and alike? This seems very promising to me for the following reason: Take the free theorem for 'sort::(a-a-Bool)-[a]-[a]'. The theorem could possibly be a lot more powerful if there were a way to encode in the type of 'sort' that it accepts a reflexive transitive antisymmetric predicate, but the only way to express that is with dependent types. Looks like the only thing one needs to add to System F is the relational translation rule for a dependent product; but I haven't tried doing it myself. ___ 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] tips on using monads
I've got one of those algorithms which threatens to march off the right edge
(in the words of Goerzen et al). I need something like a State or Maybe monad,
but this is inside the IO monad. So I presume I need StateT or MaybeT. However,
I'm still (slowly) learning about monads from first principles. I thought I
might present my code and get some pointers... maybe someone could actually show
me how to rewrite it, which would be a neat way to see MaybeT and StateT in
action. I'm hoping to get anything from a one-line response to a rewrite of my
code. Anything will help.
Here's the program:
{-
This is a program which starts with a document containing notes
about software requirements (in a particular format) and puts them
into a database. Notes include details such as the source of the
requirement (who gave it), the topic(s) to which it pertains, the
date, etc.
I have written a parser to take a text document typed up by me during a
meeting and parse it into a NoteRecord structure. Here is the
structure:
-}
data NoteRecord = NoteRecord {
recordSource :: String, -- Name of person who gave req.
recordDate :: [Int], -- Date in [year,month,date]
recordSourceType :: String, -- meeting, phone, email, etc.
recordBugNum :: Maybe Int,-- Bugzilla # (if relevant)
recordTopics :: [String], -- list of official topics pertaining
recordText :: String }-- the text of the note itself
deriving (Show)
{-
One other wrinkle. The source (person name) and topic must be one
of a set of pre-determined strings. A person has an official full name
which is stored in the database. Topics also have official descriptive
strings. If I wasn't clever, then the note, as I type it up,
must have the exact name and topic. But I hate trying to remember things
like that. So I have implemented a fuzzy string match system so
that I can type part of someone's name (or even misspell it) or part of
a topic string, and the system will find the best match to an official
string.
In pseudocode, the function to insert a note in the database must do this:
This function starts with a NoteRecord.
- If text already exists in the database, give an error and skip to end.
- Fuzzy-match strings to topics and source.
- If no potential match can be found to some of topics or source,
give error and skip to end.
- Ask user to confirm if the matched topics and source look okay.
- if user says no, skip to end.
- Actually insert the record.
-}
insertNote :: NoteRecord - Connection - IO ()
insertNote nr conn =
do -- Check if it exists in the database already.
status - checkPreExistingText nr conn
if status
then putStrLn Skipping... text exists already.
else
do -- Find best fit for all topics and source.
-- See type signatures below.
bestFitTopics - fitTopics nr conn
bestFitSource - fitSource nr conn
case any isNothing bestFitTopics of
True -
putStrLn Error... some topic couldn't be matched.
False -
case bestFitSource of
Nothing -
putStrLn Error.. source couldn't be matched.
_ -
do b - isUserOkay nr bestFitTopics bestFitSource
if b
then do
-- Create a new NoteRecord with matched
-- and validated topics/source.
nrValidated =
nr { recordTopics = bestFitTopics
, recordSource = bestFitSource }
insertRow nrValidated conn
else putStrLn Abort due to user request.
checkPreExistingText :: NoteRecord - Connection - Bool
-- There are multiple topics in the NoteRecord. For each one,
-- find the best fuzzy match, or indicate if there is no plausible
-- match at all.
fitTopics :: NoteRecord - Connection - [Maybe String]
-- There is one source. Try to find fuzzy match.
fitSource :: NoteRecord - Connection - Maybe String
-- Present user with all fuzzy matches and get a yes/no response if it's
-- okay to proceed.
isUserOkay :: NoteRecord - [Maybe String] - Maybe String - Bool
-- Do actual insert into database.
insertRow :: NoteRecord - Connection - IO ()
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: mathlink-2.0.0.3
Hi, I'm a Haskeller that uses Mathematica on a regular basis; it's one of my favourite tools. So - thanks for your work, I'll use it whenever applicable. However, during compilation I get an error that ml.h is not found, even after I added Mathematica's include dirs to Include-Dirs. Since that seems to be not a Mathematica's file (it doesn't exist in my Mathematica directories), I conclude that it might be a file that is missing from the package. Is that actually so? 2009/5/18 Tracy Wadleigh tracy.wadle...@gmail.com: Already posted to the Haskell list but dons suggested I post to the cafe, as well... All: mathlink is a library for writing Mathematica packages in Haskell. One simply writes some functions of type: (MLGet a, MLPut b) = a - IO b and provides a package specification in a simple DSL that mimics that of Mathematica's mprep utility. The result is a program that exposes functions that can be called from Mathematica. This is a complete rewrite of my original implementation and more closely captures the functionality I originally intended. I've only tested it on my own platform (64-bit Linux), but I've taken pains to make sure the code should run on any platform. (The only real issue in the code is picking the right functions to call when marshaling Ints.) Please report any tweaks required to get it to work on your platform. (That is, of course, only if, in fact, there are any other users out there. Right now, as far as I know, I'm it.) I'd also just like to hear from any Haskellers out there that also use Mathematica on a regular basis. Ping me if you're one. --Tracy ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Eugene Kirpichov Web IR developer, market.yandex.ru ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
