Re: [Haskell-cafe] Hi can u explain me how drop works in Haskell
On 2/26/07, Thomas Hartman [EMAIL PROTECTED] wrote: Here's my, probably very obvious, contribution. What I'd like feedback on is 1) code seem ok? (hope so!) Hi Thomas, tail [] raises an error, therefore your code will fail when n length xs ( e.g. mydrop 3 [1,2] will raise an exception, where [] is the expected result). Your function is also limited to list of Int only (mydrop :: Int - [Int] - [Int]). 2) What do you think of the tests I did to verify that this behaves the way I want? Is there a better / more idiomatic way to do this? You may be interested in the following projects: QuickCheck: http://www.cs.chalmers.se/~rjmh/QuickCheck/ HUnit: http://sourceforge.net/projects/hunit Regards, Antonio -- http://antoniocangiano.com Zen and the Art of Ruby Programming ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A real Haskell Cookbook
On 2/26/07, Chris Eidhof [EMAIL PROTECTED] wrote: Hey everyone, we added some examples to this page. There are some topics that don't have any examples, notably: # 11 Network Programming # 12 XML * 12.1 Parsing XML # 13 Databases * 13.1 MySQL * 13.2 PostgreSQL * 13.3 SQLite # 14 FFI * 14.1 How to interface with C If anyone feels like filling up some of those sections, that would be great. I'd also suggest adding * 4.4 Regular expressions * 4.5 Interpolation martin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Hi can u explain me how drop works in Haskell
I'd heard of quick check, but haven't got my head around it. This seems like a good place to start. I understand you have to build an invariant and then you can automate against it, eg reverse of reverse is your original string prop_RevRev xs = reverse (reverse xs) == xs where types = xs::[Int] (from http://www.kimbly.com/blog/42.html) but what would be your invariant with the drop function? At first I thought prop_HeadConsDropped xs = (head xs) : (drop 1 xs) == xs where types = xs::[a] But I think then you have the issue of head nil being an error. So, is there a better strategy? Or is using quickcheck here overkill? 2007/2/26, Antonio Cangiano [EMAIL PROTECTED]: On 2/26/07, Thomas Hartman [EMAIL PROTECTED] wrote: Here's my, probably very obvious, contribution. What I'd like feedback on is 1) code seem ok? (hope so!) Hi Thomas, tail [] raises an error, therefore your code will fail when n length xs ( e.g. mydrop 3 [1,2] will raise an exception, where [] is the expected result). Your function is also limited to list of Int only (mydrop :: Int - [Int] - [Int]). 2) What do you think of the tests I did to verify that this behaves the way I want? Is there a better / more idiomatic way to do this? You may be interested in the following projects: QuickCheck: http://www.cs.chalmers.se/~rjmh/QuickCheck/ HUnit: http://sourceforge.net/projects/hunit Regards, Antonio -- http://antoniocangiano.com Zen and the Art of Ruby Programming ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] OO Design in Haskell Example (Draft)
Hello Tim, Monday, February 26, 2007, 2:26:44 AM, you wrote: Rather than using existential types, a simple record of functions can be often be useful. ie: data Component = Component { draw :: String add :: Component - Component } Steve, you can look at the pages http://haskell.org/haskellwiki/OOP_vs_type_classes http://haskell.org/haskellwiki/IO_inside which describes some alternatives to OO approach used in functional programming world and Haskell in partial. because first page is just about switching from OOP to Haskell, you may consider adding to this page patterns you've designed -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Safe lists with GADT's
Stefan O'Rear wrote: How do I get my original function back which just turns a standard list to one of the funky lists, or is that just impossible with GADT's? Do I now have to wrap all the fuctions I use, i.e. pass safeMap in CPS? AFAIK you can't. Fortunately the CPS transform can be very local: Indeed, you can't. I mean, given fromList [] = Nil fromList (a:as) = Cons a (fromList as) what type would it have? One of fromList :: forall t . [a] - List a t fromList ::[a] - List a NilT fromList :: forall t . [a] - List a (ConsT t) ? No, because the second argument depends on the input list. The only thing we know is that there is a type t but we don't know which one. Thus fromList :: [a] - (exists t . List a t) is the correct type. As Haskell currently doesn't have first class existentials, we have to either pack it into a data type or appeal to the equivalence exists a . f a ~= forall r . (forall a . f a - r) - r Both have of course the problem that we cannot simply write safeMap (fromList [1,2,3]) :: exists t . List a t Regards, apfelmus Exercise: Why is fromList :: exists t . [a] - List a t wrong as well? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] How you can help improve Haskell implementations!
Just a quick note to say that the Haskell implementation shootout is progressing, now supporting jhc, fixing a range of bugs, and providing more benchmark programs. Nice average numbers are also reported for the relative performance of each compiler or interpreter. On x86: http://www.cse.unsw.edu.au/~dons/nobench/i686/results.html On amd64: http://www.cse.unsw.edu.au/~dons/nobench/x86_64/results.html Several bugs in our beloved Haskell compilers have been spotted, and most of them already fixed! ** I'd like to invite contributions of benchmark programs**. If you have a nice benchmarky program, that's reasonably portable (mostly h98 + base libs is ok), and freely licensed, let me know, and we can add it to the benchmark suite. Programs that show up interesting results between systems or that were difficult to get to perform well are particuarly welcome. 3 kinds of programs are welcome: * small artificial programs that illustrate particular issues e.g. (prime sieves, FFT, great language shootout programs) * 'kernels' from larger programs, that illustrate some functionality e.g. a mandelbrot generator, or some other core algorithm * larger real programs. These are particularly welcome. Limited to around 25 modules maximum, and capable of being run with simple stdin/args, producing simple output. Raytracers, chess programs, and small theorem provers are existing examples. So send me your unwashed code. Whatever code doesn't kill them will only make our compilers stronger! :-) The darcs repo for nobench/nofib is at: http://www.cse.unsw.edu.au/~dons/nobench.html Happy hacking! Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How you can help improve Haskell implementations!
ndmitchell: Hi And also I guess the compilers will do more optimisations, etc. So this suggests an obvious extra feature for nobench which would be the ability to view a graph of each compiler's performance over a period of time, obviously this probably wouldn't be useful for at least a few months. We hope to add experimental -O to Yhc within the next week or so, very soon would help us :) Its easy enough to run two or more versions of a compiler. So we can check ghc against ghc-head , or yhc against yhc-old. Just ping me if you want something checked like that. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] haskell-art mailing list
On Sat, Feb 24, 2007 at 12:47:19PM +0100, Henk-Jan van Tuyl wrote: Is this something for the list at http://haskell.org/mailman/listinfo That's generated by mailman, and as far as I know can't be easily altered. (Maybe this page could be moved to haskellwiki?) Perhaps adding a list of links to Haskell-related-lists on http://www.haskell.org/haskellwiki/Mailing_lists would be best? Thanks Ian ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe lists with GADT's
On Sun, Feb 25, 2007 at 10:40:13PM +, Neil Mitchell wrote: data ConsT a data NilT data List a t where Cons :: a - List a b - List a (ConsT b) Nil :: List a NilT ... Defining safeMap was trivial, but one thing I couldn't figure out was how to write something like fromList: fromList [] = Nil fromList (a:as) = Cons a (fromList as) fromList could obviously be anything such as reading from a file etc, where the input is not known in advance. Are there any techniques for this? My favorite ways to wrap an existential is with another GADT: data Existential a where Existential :: a b - a (Yes, properly speaking this isn't a GADT, just an existential ADT, but it's easier for me to understand this way.) Then fromList [] = Existential Nil fromList (a:as) = case fromList as of Existential as' - Existential (Cons a as') This is a pretty easy way to deal with the fromList. You'll now also want (which I don't think you mentioned in your example code) a GADT version of null, and perhaps other length operators: data NullT t where IsNull :: NullT NilT NotNull :: NullT (ConsT t) nullL :: List a t - NullT t so you can now actually use your head function on a dynamically generated list, by running something like (e.g. in a monad) do cs - readFile foo Existential cs' - return $ fromList cs -- note: we'll pattern-match fail on non-empty list here, which -- may not gain much, we'd use case statements in reality, or we'd -- catch failure within the monad, which is also safe--provided you -- catch them, which the language doesn't force you to do! (Or if -- we're in a pure monad like Maybe.) NotNull - nullL cs' let c = headL cs' t = tailL cs' -- Now to illustrate the power of the GADT, a line that will fail -- at compile time: t' = tailL t return c -- David Roundy http://www.darcs.net ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Did quickchekc get dropped from ghc from 6.4 to 6.6?
According to http://www.cs.chalmers.se/~rjmh/QuickCheck/ Quickcheck is distributed with ghc. I seem to recall this came with ghc 6.4. After upgrading to ghc 6.6, however, I don't seem to have it anymore. Do I need to install it from cabal? If so, I assume this would start by wgetting http://hackage.haskell.org/packages/archive/QuickCheck/QuickCheck-1.0.tar.gz and building that. thomas. [EMAIL PROTECTED]:~/learning/haskell/lists$ ghci ___ ___ _ / _ \ /\ /\/ __(_) / /_\// /_/ / / | | GHC Interactive, version 6.6, for Haskell 98. / /_\\/ __ / /___| | http://www.haskell.org/ghc/ \/\/ /_/\/|_| Type :? for help. Loading package base ... linking ... done. Prelude :m Control.Monad Prelude Control.Monad :m Test.QuickCheck Could not find module `Test.QuickCheck': Use -v to see a list of the files searched for. Prelude Control.Monad :m Quickcheck Could not find module `Quickcheck': Use -v to see a list of the files searched for. Prelude Control.Monad ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe lists with GADT's
I am really curious about this style of programming, and find myself playing with it from time to time. The example so far is very nice, but the funniest part is missing. That is, defining appendL. appendL :: List a t1 - List a t2 - List a t3 This says that the append of a list of length t1 and a list of length t2 is a list of whatever length t3 we want. Obviously this is not true and will not typecheck. After some healthy days of reading papers and theses, I've found at least three ways of defining it. First, via existentials: appendL1 :: List a t1 - List a t2 - exists t3. List a t3 Second, attaching a proof. Question: what would be the advantage of the proof here? data Add a b c where Base :: Add NilT a a ; Step :: Add a b c - Add (ConsT a) b (ConsT c) appendL2 :: List a t1 - List a t2 - exists t3. (Add t1 t2 t3, List a t3) Third, via Type Classes. \begin{code} class AddList a b c | a b - c where append :: List x a - List x b - List x c instance AddList NilT b b where append Nil x = x instance AddList a b c = AddList (ConsT a) b (ConsT c) where append (Cons x l) l' = Cons x (append l l') \end{code} Given the three methods, I wouldn't know which one should be preferred, and why. In the first one you pay the burden of programming with existentials. The second one in addition to that is the least efficient, as building the proof surely has a cost. Since we are building it, isn't there a way to use it to remove the existential? Finally, with the third one your compiler will produce error messages that will make you swear, apart from possible efficiency losses too. Thanks for reading, any hints will be appreciated pepe On 26/02/2007, at 15:26, David Roundy wrote: On Sun, Feb 25, 2007 at 10:40:13PM +, Neil Mitchell wrote: data ConsT a data NilT data List a t where Cons :: a - List a b - List a (ConsT b) Nil :: List a NilT ... Defining safeMap was trivial, but one thing I couldn't figure out was how to write something like fromList: fromList [] = Nil fromList (a:as) = Cons a (fromList as) fromList could obviously be anything such as reading from a file etc, where the input is not known in advance. Are there any techniques for this? My favorite ways to wrap an existential is with another GADT: data Existential a where Existential :: a b - a (Yes, properly speaking this isn't a GADT, just an existential ADT, but it's easier for me to understand this way.) Then fromList [] = Existential Nil fromList (a:as) = case fromList as of Existential as' - Existential (Cons a as') This is a pretty easy way to deal with the fromList. You'll now also want (which I don't think you mentioned in your example code) a GADT version of null, and perhaps other length operators: data NullT t where IsNull :: NullT NilT NotNull :: NullT (ConsT t) nullL :: List a t - NullT t so you can now actually use your head function on a dynamically generated list, by running something like (e.g. in a monad) do cs - readFile foo Existential cs' - return $ fromList cs -- note: we'll pattern-match fail on non-empty list here, which -- may not gain much, we'd use case statements in reality, or we'd -- catch failure within the monad, which is also safe-- provided you -- catch them, which the language doesn't force you to do! (Or if -- we're in a pure monad like Maybe.) NotNull - nullL cs' let c = headL cs' t = tailL cs' -- Now to illustrate the power of the GADT, a line that will fail -- at compile time: t' = tailL t return c -- David Roundy http://www.darcs.net ___ 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: AT solution: rebinding = for restricted monads
David Roundy droundy at darcs.net writes: My latest attemp (which won't compile with the HEAD ghc that I just compiled, probably because I haven't figured out the synatax for guards with indexed types is: class WitnessMonad m where type W m :: * - * - * (=) :: (WitnessMonad m', WitnessMonad m'', w a b = W m', w b c = W m'', w a c = W m) = m' x - (x - m'' y) - m y () :: (WitnessMonad m', WitnessMonad m'', w a b = W m', w b c = W m'', w a c = W m) = m' x - m'' y - m y f g = f = const g return :: w a a = W m x = - m x fail :: String - m x data Witness a b instance Monad m = WitnessMonad m where W m = Witness () () (=) = Prelude.(=) () = Prelude.() return = Prelude.return fail = Prelude.fail which I think is quite pretty. It allows the Monadlike object to have kind * - *, while still allowing us to hide extra witness types inside and pull them out using the W function. Did anyone with knowledge of Associated Types pursue this solution? It doesn't work with GHC head, and I can't really do anything about that. Mostly curiosity. Thanks pepe Everything from here on is to convince GMane that, even if my message contains more quoted text than fresh text, it is a legitimate message and it should be ok to post it. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] R wrapper in haskell
On Sun, 25 Feb 2007, Peng Zhang wrote: Hi folks, My primary language is R, which is an imperative functional language. I start to learn haskell and try to use it instead when a project is time-consuming and it takes months in R. I like the language very much so far, but I do miss some important functions in R which can generate random numbers from all kinds of distributions. Maybe, also this one is of interest: http://haskell.org/haskellwiki/New_monads/MonadRandom ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Did quickchekc get dropped from ghc from 6.4 to 6.6?
On 26/02/07, Thomas Hartman [EMAIL PROTECTED] wrote: According to http://www.cs.chalmers.se/~rjmh/QuickCheck/ Quickcheck is distributed with ghc. I seem to recall this came with ghc 6.4. After upgrading to ghc 6.6, however, I don't seem to have it anymore. Hmm, which release do you have? I don't think that I had to do anything special to get QuickCheck. I just have the generic Linux binary distribution. If you have a distribution-specific package, check that there isn't another one for QuickCheck. Alternately, yeah, you can just get it from Hackage like you described. [EMAIL PROTECTED]:~$ ghci ___ ___ _ / _ \ /\ /\/ __(_) / /_\// /_/ / / | | GHC Interactive, version 6.6, for Haskell 98. / /_\\/ __ / /___| | http://www.haskell.org/ghc/ \/\/ /_/\/|_| Type :? for help. Loading package base ... linking ... done. Prelude :m + Test.QuickCheck Prelude Test.QuickCheck ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Did quickchekc get dropped from ghc from 6.4 to 6.6?
Thomas Hartman wrote: According to http://www.cs.chalmers.se/~rjmh/QuickCheck/ Quickcheck is distributed with ghc. I seem to recall this came with ghc 6.4. After upgrading to ghc 6.6, however, I don't seem to have it anymore. Do I need to install it from cabal? If so, I assume this would start by wgetting http://hackage.haskell.org/packages/archive/QuickCheck/QuickCheck-1.0.tar.gz and building that. thomas. Hi Thomas, between GHC 6.4 and 6.6 many libraries were moved into the ghc-extralibs source tarball. QuickCheck is among those. If you install GHC from the source tarball, you may also want to grab extralibs and install that, if you want an environment resembling the one you get with a normal GHC 6.4 installation. /Björn ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe lists with GADT's
On Mon, Feb 26, 2007 at 04:35:06PM +0100, Pepe Iborra wrote: First, via existentials: appendL1 :: List a t1 - List a t2 - exists t3. List a t3 It seems like this problem is begging for the new indexed types (for which I never remember the right syntax). type AddListTs :: * - * - * AddListTs NilT NilT = NilT AddListTs NilT t = t AddListTs (ConsT t) t' = AddListTs t (ConsT t') then appendLi :: List a t1 - List a t2 - List a (AddListTs t1 t2) I'd be interested if Manuel had an idea whether this would work right. I think it can be made equivalent to the FD approach, but doesn't require that you define a stupid class, and is far, far prettier. -- David Roundy Department of Physics Oregon State University ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Trouble with record syntax and classes
I'm brand new to haskell and I'm having trouble using classes. The basic idea is I want two classes, Sine and MetaSine, that are both instances of ISine. This way I can use the act method and recurse through the metasines and sines. Here's my code: module Main where class ISine a where period :: a - Integer offset :: a - Integer threshold :: a - Integer act :: (ISine b) = Integer - a - b on :: Integer - a - Bool --on needs offset, period, threshold on time self = (mod (time-(offset self)) (period self)) (threshold self) data Sine = Sine { period :: Integer, offset :: Integer, threshold :: Integer, letter :: String } instance Sine ISine where act time (Sine self) |on time self = [letter self] |otherwise = [] data MetaSine = MetaSine { period :: Integer, offset :: Integer, threshold :: Integer, sines :: (ISine a) = [a] } instance MetaSine ISine where act time (MetaSine self) |on time self = foldr (++) (map (act time) (sines self)) |otherwise = [] The errors I get involve multiple declarations of period, offset, and threshold. Any help would be greatly appreciated. -Thomas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Links in Haskell code in HaskellWiki
L.S., Links in the Haskell code in the wiki pages point to wrong labels; for example, if 'print' is used, it is linked to: http://haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#v:print the colon should be %3A: http://haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#v%3Aprint For '==', the link is: http://haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#v:== it should be: http://haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#v%3A%3D%3D (see for example http://haskell.org/haskellwiki/OOP_vs_type_classes ) Can someone correct this? -- Met vriendelijke groet, Henk-Jan van Tuyl -- http://Van.Tuyl.eu/ -- Using Opera's revolutionary e-mail client: https://secure.bmtmicro.com/opera/buy-opera.html?AID=789433 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] [Fwd: Re: Computer Language Shootout]
[redirecting to haskell-cafe, since this is getting to be a long discussion] On 2/26/07, Andrzej Jaworski [EMAIL PROTECTED] wrote: The examples I pointed to seem to share strong and relatively consistent logic of a program. In case of large GA (e.g. Royal Road Problem) and IFP (e.g. ADATE) SML was exhaustively proved to predict this logic much better. Can you clarify what you mean by this? How do you formally prove that a programming language (rather than a specific implementation of one) performs better for a given problem? Or do you mean that a specific implementation of this problem in SML performed better than a specific implementation of it in Haskell? In case of Algebraic Dynamic Programming C compiler seems to address specific properties of a program more adequately which leads to substantial improvements in optimization. It is important to stress that we deal in ADP with strong logic of the domain application. Handcrafting C code for regular applications does not show that kind of advantage, so it wouldn't leave Haskell in the dust. In general declarative nature has the edge over C craftsmanship (see: http://www.clip.dia.fi.upm.es/papers/carro06:stream-interpreter-TR.pdf). I've read a few of your posts and I still don't understand what you mean by a compiler address[ing] specific properties of a program. Can you give an example of the kinds of program properties you're talking about, and explain how C compilers exploit them in a way that Haskell compilers currently fail to do? Cheers, Kirsten -- Kirsten Chevalier* [EMAIL PROTECTED] *Often in error, never in doubt Religion is just a fancy word for the Stockholm Syndrome. -- lj user=pure_agnostic ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] FFI basics
... and now I have more questions. Maybe it would be better if I just asked them on the mailing list, and then incorporated the answers into the wiki myself. Question #1 is compiling FFI using modules. I'd like to use ghc --make for the speed and convenience, but obviously it doesn't know how to compile the C. So my hybrid approach has been to write a makefile for the C, and then make the haskell program depend on the .o files and invoke ghc --make on them, like so: _dummy_target: cfile.o ghc -Ic_includes -Lc_libs --make -main-is HsMain -o target HsMain.hs cfile.o -lclib Unfortunately, ghc doesn't seem relink the target if cfile.o changed, so as a hack I put 'rm target' before the ghc line to make it link every time. Does anyone have a better solution? #2 is structs. What's a good way to marshal structs? The straightforward way would be C stubs like T get_t(struct foo *x) for every field of the struct, but clearly at any kind of scale something like greencard will be necessary (as an aside, greencard's last update seems to have been support this newfangled FFI... is it still alive and just done or are people using something else nowadays?). Hopefully in can be made efficient though (I don't know if cross C-haskell inlining will happen, but maybe with -fvia-c?). The other issue is that the haskell type will not be Storable, so the Foreign.Array stuff won't work... I need a separate sizeof C stub and allocaBytes. It's much easier to declare e.g. type SomeCStruct = Word64 and then use Bits to pick out the fields in pure haskell, but I imagine this assumes way too much about how the struct is layed out in memory. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Trouble with record syntax and classes
All record fields are in the same namespace, and furthermore this is also the same namespace of functions and class methods. In other words you cannot have two record types containing the same field name, and you cannot have a record field and a function using the same name, and you cannot have a record field and a class method using the same name. You have to choose some other names for the fields of Sine, and yet some other names for the fields of MetaSine. In instance Sine ISine where ..., you must implement the methods period, offset, and threshold, not just act. Similarly for instance MetaSine ISine where The implementations of method act are syntactically wrong as well as semantically wrong. I do not know what is a right implementation. Actually given the overly general signature act :: (ISine b) = Integer - a - b I do not think there is any possible implementation at all. I submit that you have set a goal too ambitious and too magical. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Trouble with record syntax and classes
On 2/26/07, Thomas Nelson [EMAIL PROTECTED] wrote: I'm brand new to haskell and I'm having trouble using classes. The basic idea is I want two classes, Sine and MetaSine, that are both instances of ISine. 'class' in Haskell doesn't mean the same as 'class' in C++ or Java. I found it easier at first to thing of them as: A Haskell 'class' is more like a Java interface. Haskell types are more like what you might think of as 'class'es. Haskell 'instance' means Java 'implement' There is no word that means that same as 'instance' from Java/C++ terminology. I suppose we would call them 'values' or something. Somebody more knowledgeable can describe the etymology of the terms, but these 3 observations should help. data Sine = Sine { period :: Integer, offset :: Integer, threshold :: Integer, letter :: String} instance Sine ISine where act time (Sine self) |on time self = [letter self] |otherwise = [] To be honest, I'm not sure what you're trying to do here, so beware of my advice... You might want to do this instead: data Sine = Sine Integer Integer Integer String instance ISine Sine where -- note that ISine should come before Sine period (Sine p _ _ _ _) = p period (Sine _ o _ _ _) = o -- and so on ... There can only be a single function called period, which will take a thing of any type which is an instance of ISine and return an Integer. So every time you tell Haskell this type is to be an implementation of ISine you have to write the period function for it as I have done for Sine here. -Thomas Aaron ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Delaling with State StateT and IO in the same function
Hello, I know StateT is exactly aimed at dealing with a state and an inner monad but I have an example in which I have to mix State and IO and in which I didn't get to an elegant solution using StateT. I have a higher order function which gets some State processing functions as input, makes some internal operations with IO and has to return a State as output. My (ugly) function interface is netlist :: DT.Traversable f = (State s (S HDPrimSignal) - State s v ) - -- new (State s (Type,v) - S v - State s ()) - -- define State s (f HDPrimSignal) - -- the graph StateT s IO () The returned type is a StateT and the only way in which I succesfully managed to internally work with both State and StateT is converting from the former to the later one using this function (not elegant at all) state2StateT :: Monad m = State s a - StateT s m a state2StateT f = StateT (return.runState f) I tried avoiding to use state2StateT by changing the interface to netlist :: DT.Traversable f = (State s (S HDPrimSignal) - State s v ) - -- new (State s (Type,v) - S v - State s ()) - -- define State s (f HDPrimSignal) - -- the graph State s (IO ()) but the function ended up being even uglier and I had to be care full about all the internal IO actions being executed (it is aesy to formget about it), let me show a (quite stupid) example myState :: State () (IO ()) myState = (return $ putStrLn first line) (return $ putStrLn second line) eval myState () second line The first line is obviously lost Here is the full code of my function (many type definitions are missing but I hope it is understandable anyway) import qualified Data.Traversable as DT (Traversable(mapM)) import qualified Control.Monad.Trans import Language.Haskell.TH(Type) netlist :: DT.Traversable f = (State s (S HDPrimSignal) - State s v ) - -- new (State s (Type,v) - S v - State s ()) - -- define State s (f HDPrimSignal) - -- the graph StateT s IO () -- Generates a netlist given: -- new: generates the new (and normally unique) tag of every node given -- the iteration state which is updated as well. -- define: given the tag of a node, -- current iteration state, its type, and the tag of its children, -- generates the netlist of that node, updating the iteration state -- pSignals: the graph itself, a traversable collection of root --signals including the initial state of the iteration -- It returns the final iteration state and the tags of outputs -- (root primitivesignals) netlist new define pSignals = do f - state2StateT pSignals tab - lift table let -- gather :: State s HDPrimSignal - StateT s IO v gather sm = do HDPrimSignal t node - sm visited - lift (find tab node) case visited of Just v - return v Nothing - do let sP = deref node v' - state2StateT (new (return sP)) lift (extend tab node v') sV - DT.mapM (gather.return) sP state2StateT (define (return (t,v')) sV) return v' in DT.mapM (gather.return) f return() just in case it helps table :: IO (Table a b) find :: Table a b - Ref a - IO (Maybe b) extend :: Table a b - Ref a - b - IO () Maybe is asking too much but would anyone be able to provide a more elegant netlist function which ... option a) returns StateT but doesn't make use of state2StateT? or option b) returns State but doesnt end up being messy? Thanks in advance, Alfonso Acosta ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe lists with GADT's
On Mon, Feb 26, 2007 at 04:35:06PM +0100, Pepe Iborra wrote: I am really curious about this style of programming, and find myself playing with it from time to time. The example so far is very nice, but the funniest part is missing. That is, defining appendL. appendL :: List a t1 - List a t2 - List a t3 This says that the append of a list of length t1 and a list of length t2 is a list of whatever length t3 we want. Obviously this is not true and will not typecheck. After some healthy days of reading papers and theses, I've found at least three ways of defining it. First, via existentials: appendL1 :: List a t1 - List a t2 - exists t3. List a t3 Second, attaching a proof. Question: what would be the advantage of the proof here? data Add a b c where Base :: Add NilT a a ; Step :: Add a b c - Add (ConsT a) b (ConsT c) appendL2 :: List a t1 - List a t2 - exists t3. (Add t1 t2 t3, List a t3) Third, via Type Classes. \begin{code} class AddList a b c | a b - c where append :: List x a - List x b - List x c instance AddList NilT b b where append Nil x = x instance AddList a b c = AddList (ConsT a) b (ConsT c) where append (Cons x l) l' = Cons x (append l l') \end{code} Given the three methods, I wouldn't know which one should be preferred, and why. In the first one you pay the burden of programming with existentials. The second one in addition to that is the least efficient, as building the proof surely has a cost. Since we are building it, isn't there a way to use it to remove the existential? Finally, with the third one your compiler will produce error messages that will make you swear, apart from possible efficiency losses too. Personally I like the GADT approach best since it is very flexible and convienient. I have never used a purpose-build computer proof system, but (modulo _|_) it took me less than 10 minutes to answer LoganCapaldo (on #haskell)'s challenge to proof that + was commutative ( http://hpaste.org/522 ). Now, efficiency concerns. GHC haskell already uses higher-than-value-level proofs to implement newtypes/GADTs/ATs; efficiency concerns are addressed in a strikingly adhoc way, by promoting equality to the KIND level, allowing type erasure to remove the overhead of checking. Chakravarty, Peyton Jones, we'd really like a general kind-level proof system! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Delaling with State StateT and IO in the same function
On 2/26/07, Alfonso Acosta [EMAIL PROTECTED] wrote: The returned type is a StateT and the only way in which I succesfully managed to internally work with both State and StateT is converting from the former to the later one using this function (not elegant at all) I may be missing something, but why are you using both State and StateT? Maybe I don't understand your code, but it seems like you could be using StateT everywhere you're currently using State. Also, your type signatures would be easier to read if you defined a type synonym for your instantiation of StateT, e.g.: type AlfonsoM s = StateT s IO () and then everywhere you write (StateT s IO ()) now, you could write (AlfonsoM s) instead. Cheers, Kirsten -- Kirsten Chevalier* [EMAIL PROTECTED] *Often in error, never in doubt ...People who mind their own business die of boredom at thirty.--Robertson Davies ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Delaling with State StateT and IO in the same function
On 2/27/07, Kirsten Chevalier [EMAIL PROTECTED] wrote: I may be missing something, but why are you using both State and StateT? Maybe I don't understand your code, but it seems like you could be using StateT everywhere you're currently using State. Well, as far as I know using StateT s IO a for the input functions would force the state and value of their monad to stay within IO. That restriction dissapears by using barely State s a Also, your type signatures would be easier to read if you defined a type synonym for your instantiation of StateT, e.g.: type AlfonsoM s = StateT s IO () and then everywhere you write (StateT s IO ()) now, you could write (AlfonsoM s) instead. Thanks for the suggestion, I'll make use of it :) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] FFI basics
On Mon, Feb 26, 2007 at 01:02:57PM -0800, Evan Laforge wrote: Question #1 is compiling FFI using modules. I'd like to use ghc --make for the speed and convenience, but obviously it doesn't know how to compile the C. So my hybrid approach has been to write a makefile for the C, and then make the haskell program depend on the .o files and invoke ghc --make on them, like so: _dummy_target: cfile.o ghc -Ic_includes -Lc_libs --make -main-is HsMain -o target HsMain.hs cfile.o -lclib Unfortunately, ghc doesn't seem relink the target if cfile.o changed, so as a hack I put 'rm target' before the ghc line to make it link every time. Does anyone have a better solution? Yeah. GHC knows how to call GCC on .c files, so just do: ghc -Ic_includes -Lc_libs --make -main-is HsMain -o target HsMain.hs cfile.c -lclib Don't worry about recompilation checking, GCC is two orders of magnitude faster than GHC so the extra time will be neglible unless your program is 95% C. #2 is structs. What's a good way to marshal structs? The straightforward way would be C stubs like T get_t(struct foo *x) for every field of the struct, but clearly at any kind of scale something like greencard will be necessary (as an aside, greencard's last update seems to have been support this newfangled FFI... is it still alive and just done or are people using something else nowadays?). Hopefully in can be made efficient though (I don't know if cross C-haskell inlining will happen, but maybe with -fvia-c?). The other issue is that the haskell type will not be Storable, so the Foreign.Array stuff won't work... I need a separate sizeof C stub and allocaBytes. It's much easier to declare e.g. type SomeCStruct = Word64 and then use Bits to pick out the fields in pure haskell, but I imagine this assumes way too much about how the struct is layed out in memory. I don't know about GreenCard, but hsc2hs is still very much alive and also addresses that goal. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Delaling with State StateT and IO in the same function
On 2/26/07, Alfonso Acosta [EMAIL PROTECTED] wrote: On 2/27/07, Kirsten Chevalier [EMAIL PROTECTED] wrote: I may be missing something, but why are you using both State and StateT? Maybe I don't understand your code, but it seems like you could be using StateT everywhere you're currently using State. Well, as far as I know using StateT s IO a for the input functions would force the state and value of their monad to stay within IO. That restriction dissapears by using barely State s a Ah, ok. So what if you changed your netlist function so that the type sig would be: netlist :: DT.Traversable f = (State s (S HDPrimSignal) - State s v ) - -- new (State s (Type,v) - S v - State s ()) - -- define State s (f HDPrimSignal) - -- the graph IO (State s ()) I didn't follow your code well enough to be sure that this would help, but I think it might. Or why not: netlist :: DT.Traversable f = (State s (S HDPrimSignal) - State s v ) - -- new (State s (Type,v) - S v - State s ()) - -- define State s (f HDPrimSignal) - -- the graph IO s which seems to me like it would be even simpler, unless you're planning on composing calls to netlist together (and from the code you gave, I can't tell whether you are.) If your code is such that refactoring it to have either of those types wouldn't make sense, stating the reasons why should clarify things for the rest of us. Cheers, Kirsten -- Kirsten Chevalier* [EMAIL PROTECTED] *Often in error, never in doubt Aw, honey, you can keep what's in my pockets, but send me back my pants. --Greg Brown ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Delaling with State StateT and IO in the same function
On 2/27/07, Kirsten Chevalier [EMAIL PROTECTED] wrote: So what if you changed your netlist function so that the type sig would be: netlist :: DT.Traversable f = (State s (S HDPrimSignal) - State s v ) - -- new (State s (Type,v) - S v - State s ()) - -- define State s (f HDPrimSignal) - -- the graph IO (State s ()) Or why not: netlist :: DT.Traversable f = (State s (S HDPrimSignal) - State s v ) - -- new (State s (Type,v) - S v - State s ()) - -- define State s (f HDPrimSignal) - -- the graph IO s Uhm, this looks better, I'll try with this one and see what I get, I anyway suspect I'll have a hard time because of the nested monads ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: OO Design in Haskell Example (Draft)
interesting. it leads to something that feels much more like an object based, as opposed to a class based, system. as far as haskell is concerned, everything has the same type, even though different instances have very different behavior. instance variables are captured by the closures that define the object methods, through the instance construction functions. i get the feeling that a model like 'self''s , based on prototypes, would not be that hard to implement. i should have the equivalent example with this style done soon. the question is, which plays nicer with the rest of haskell? that is, if i'm not committing to a closed dsl, which style is more likely to be reusable against other libraries. my experience so far has been with parsers and type checkers that make extensive use of pattern matching, which is why I probably gravitated towards the type class with existentials solution. but my experience is limited. On 2/26/07, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: Tim Docker wrote: Steve Downey wrote: So, I've been working on a Composite example. I've used existential types to have a generic proxy to the base type, rather than a simple algebraic type, since adding new leaves to the algebraic type means modifying the whole type, a violation of the Open-Closed principle (open for extension, closed for modification) Rather than using existential types, a simple record of functions can be often be useful. ie: data Component = Component { draw :: String add :: Component - Component } It might be worth comparing this approach with the (more complex) one you have described. The point about existential types is that every class like IComponent that allow as useful existential like data Component = forall e.(IComponent e) = Component e can be put into the record form Tim mentions. See the old wiki pages at http://haskell.org/hawiki/ExistentialTypes This is because every such IComponent has to look like class IComponent e where foo1 :: e - ... - e ... bar1 :: e - ... ... where the dots in - ... must not contain the type variable e. Regards, apfelmus ___ 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] Hi can u explain me how drop works in Haskell
in addition, a good example of how to apply quickcheck would be really awesome. without using the standard drop g On 2/26/07, Thomas Hartman [EMAIL PROTECTED] wrote: Here's my, probably very obvious, contribution. What I'd like feedback on is 1) code seem ok? (hope so!) 2) What do you think of the tests I did to verify that this behaves the way I want? Is there a better / more idiomatic way to do this? ** [EMAIL PROTECTED]:~/learning/haskell/lists$ cat drop.hs mydrop :: Int - [Int] - [Int] mydrop 0 xs = xs mydrop n xs = mydrop (n-1) (tail xs) main = test test = do print test1 print test2 print test3 test1 = mydrop 3 [1,2,3] == [] test2 = mydrop 2 [1,2,3] == [3] test3 = mydrop 0 [1,2,3] == [1,2,3] [EMAIL PROTECTED]:~/learning/haskell/lists$ runghc drop.hs True True True 2007/2/26, iliali16 [EMAIL PROTECTED]: Hi I am trying to implement the function drop in haskell the thing is that I I have been trying for some time and I came up with this code where I am trying to do recursion: drop :: Integer - [Integer] - [Integer] drop 0 (x:xs) = (x:xs) drop n (x:xs) |n lList (x:xs) = dropN (n-1) xs : |otherwise = [] So I want to understand how would this work and what exacttly should I put as an answer on line 4 couse that is where I am lost. I know I might got the base case wrong as well but I don't know what to think for it. I have done the lList as a function before writing this one. Thanks to those who can help me understand this. Thanks alot in advance! Have a nice day! -- View this message in context: http://www.nabble.com/Hi-can-u-explain-me-how-drop-works-in-Haskell-tf3290490.html#a9152251 Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Hi can u explain me how drop works in Haskell
ok maybe i should have read ahead. but still, i can see how to apply hunit, but not quickcheck. but quickcheck seems more powerful. On 2/26/07, Steve Downey [EMAIL PROTECTED] wrote: in addition, a good example of how to apply quickcheck would be really awesome. without using the standard drop g On 2/26/07, Thomas Hartman [EMAIL PROTECTED] wrote: Here's my, probably very obvious, contribution. What I'd like feedback on is 1) code seem ok? (hope so!) 2) What do you think of the tests I did to verify that this behaves the way I want? Is there a better / more idiomatic way to do this? ** [EMAIL PROTECTED]:~/learning/haskell/lists$ cat drop.hs mydrop :: Int - [Int] - [Int] mydrop 0 xs = xs mydrop n xs = mydrop (n-1) (tail xs) main = test test = do print test1 print test2 print test3 test1 = mydrop 3 [1,2,3] == [] test2 = mydrop 2 [1,2,3] == [3] test3 = mydrop 0 [1,2,3] == [1,2,3] [EMAIL PROTECTED]:~/learning/haskell/lists$ runghc drop.hs True True True 2007/2/26, iliali16 [EMAIL PROTECTED]: Hi I am trying to implement the function drop in haskell the thing is that I I have been trying for some time and I came up with this code where I am trying to do recursion: drop :: Integer - [Integer] - [Integer] drop 0 (x:xs) = (x:xs) drop n (x:xs) |n lList (x:xs) = dropN (n-1) xs : |otherwise = [] So I want to understand how would this work and what exacttly should I put as an answer on line 4 couse that is where I am lost. I know I might got the base case wrong as well but I don't know what to think for it. I have done the lList as a function before writing this one. Thanks to those who can help me understand this. Thanks alot in advance! Have a nice day! -- View this message in context: http://www.nabble.com/Hi-can-u-explain-me-how-drop-works-in-Haskell-tf3290490.html#a9152251 Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] overlapping instances, selecting if type a does not belong to class?
I want to write a class introducing a function which should append a b resulting in a HList containing a and b (order doesn't matter) So I came up with: = code === class (HList c) = HListAppendArbitrary a b c | a b - c where hAppendArbitrary :: a - b - c -- instance HList + HList (1) instance (HList a, HList b, HAppend a b c, HList c) = HListAppendArbitrary a b c where hAppendArbitrary a b = hAppend a b -- overlapping instance HList + value (2) instance (HList a, HList c) = HListAppendArbitrary a b c where hAppendArbitrary a b = HCons b a = error == hps-lib/HPS/Utils.hs|130| 0: || Duplicate instance declarations: || instance [overlap ok] (HList a, HList b, HAppend a b c, HList c) = || HListAppendArbitrary a b c -- Defined at hps-lib/HPS/Utils.hs|130| 0 || instance [overlap ok] (HList a, HList c) = || HListAppendArbitrary a b c -- Defined at hps-lib/HPS/Utils.hs|134| 0 = === instance (2) should be used if b does not belong to class HList. Of course there is another opportunity by writing (HCons a x) instead of to force the first type beeing a HList... Which is the topic to read from the ghc/ haskell manual ? Marc Weber ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] overlapping instances, selecting if type a does not belong to class?
Marc Weber wrote: class (HList c) = HListAppendArbitrary a b c | a b - c where hAppendArbitrary :: a - b - c -- instance HList + HList (1) instance (HList a, HList b, HAppend a b c, HList c) = HListAppendArbitrary a b c where hAppendArbitrary a b = hAppend a b -- overlapping instance HList + value (2) instance (HList a, HList c) = HListAppendArbitrary a b c where hAppendArbitrary a b = HCons b a In Haskell, instances are selected based on the _type_ (rather than class) and only the instance head is considered in the process. The instance constraints are checked only _after_ the instance has been selected, but not during the process. In the above example, if we disregard the instance constraints, the instances become instance ListAppendArbitrary a b c instance ListAppendArbitrary a b c they are indeed the same: hence the typechecker complaint. That said, it is quite possible in Haskell to achieve genuine class-based dispatch, with backtracking if necessary: http://pobox.com/~oleg/ftp/Haskell/poly2.txt However, it seems that your particular problem can be solved with simpler means: instance (HList a) = HListAppendArbitrary a HNil a where hAppendArbitrary a _ = a instance (HList a, HList b, HList c) = HListAppendArbitrary a (HCons b d) c where hAppendArbitrary a b = hAppend a b -- or use HCons with recursion -- overlapping instance HList + value (2) instance (HList a, HList c) = HListAppendArbitrary a b c where hAppendArbitrary a b = HCons b a Besides, the constraint |HList a| is equivalent to |a| being either HNil or HCons x y. Using the structural induction is always preferable. Incidentally, the code in your previous messages contained -fallow-incoherent-instances. I'd like to caution against using this extension. It makes GHC commit to a general instance even if more specific exist (and could be selected if more type information becomes available). Therefore, enabling this extension may lead to surprises. Sometimes this extension is indeed necessary and essential, when we wish to compare type variables for identity. These cases are rare however. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] State of OOP in Haskell
Lennart wrote: OOHaskell is ingenious, but it's a terrible way to use Haskell. It's very unidiomatic Haskell, and it makes you do things in the same old OO way. It's probably obvious but let me say that ... OOHaskell is more of a proof of concept and a sandbox for OO language design. It is not a serious proposal for actual OO application development. Alexy wrote: And OOHaskell didn't compile for me on GHC 6.6... tells you about currency of use. I know a few people trying to use it. :-) Oleg and I were distracted but will update OOHaskell for 6.6 soon. Ralf ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Safe lists with GADT's
Stefan O'Rear wrote: Personally I like the GADT approach best since it is very flexible and convienient. I have never used a purpose-build computer proof system, but (modulo _|_) it took me less than 10 minutes to answer LoganCapaldo (on #haskell)'s challenge to proof that + was commutative ( http://hpaste.org/522 ) I'm afraid it may be premature to call this a proof. Here's your code data S x data Z data Add :: * - * - * - * where AddZZ :: Add Z Z Z AddS1 :: !(Add x y z) - Add (S x) y (S z) AddS2 :: !(Add x y z) - Add x (S y) (S z) add_is_commutatative :: Add a b c - Add b a c add_is_commutatative (AddZZ) = AddZZ add_is_commutatative (AddS1 a) = AddS2 (add_is_commutatative a) add_is_commutatative (AddS2 a) = AddS1 (add_is_commutatative a) First of all, where is the coverage proof? Given two numbers, S (S Z) and S Z, how to find their sum using the above code? Someone needs to construct the sequence of Adds, _at run-time_! But where is the proof that the sequence of Add applications expresses all possible ways of computing the sum, and each possible sum can be represented as a sequence of Adds? One may say -- this is so trivial; to which I reply that the original question was trivial as well. If we talk about the formal _proof_, then let's do it rigorously and formally all the way. Also, we can write main = let x = AddS1 (undefined::Add Z Z (S Z)) in print OK main2 = let x = add_is_commutatative (undefined::Add Z Z (S Z)) in print OK and the evaluation of 'main' and main2 prints OK. Thus we need to do forcing _all_ the way. But what if we forget some forcing? Incidentally, this is exactly what happened: add_is_commutatative should have been strict. But the code above misses the strictness annotation and still it compiles and seems to work -- and gives one a reason to call it a proof despite the deficiency. I'm afraid I have little trust in the system that permits such lapses. but (modulo _|_) That is quite an unsatisfactory disclaimer! From the CH point of view, Haskell is inconsistent as every type is populated. Showing that a function is total is precisely demonstrating that the function is the proof of its type. So, showing the absence of bottoms is precisely making the proof! The problem with GADTs and other run-time based evidence is just that: _run-time_ based evidence and pattern-matching. In a non-strict system, checking that the evidence is really present is the problem on and of itself. BTW, Omega, Dependent ML and a few other systems with GADTs are strict. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: overlapping instances, selecting if type a does not belong to class?
Wow. That said, it is quite possible in Haskell to achieve genuine class-based dispatch, with backtracking if necessary: http://pobox.com/~oleg/ftp/Haskell/poly2.txt Thanks for digging this up. I'll have to reread it tomorrow. I wasn't able to find the definition of AllOf(But): quote type Nums = Int :*: Integer :*: AllOf Fractionals :*: HNil type Ords = Bool :*: Char :*: AllOf Nums :*: HNil type Eqs = AllOf (TypeCl OpenEqs) :*: AllOfBut Ords Fractionals :*: HNil However, it seems that your particular problem can be solved with simpler means: instance (HList a) = HListAppendArbitrary a HNil a where hAppendArbitrary a _ = a instance (HList a, HList b, HList c) = HListAppendArbitrary a (HCons b d) c where hAppendArbitrary a b = hAppend a b -- or use HCons with recursion You are right. But it's more complicated in the sense that it needs two instance declarations compared to one (called much boilerplate in the article) ... Incidentally, the code in your previous messages contained -fallow-incoherent-instances. I'd like to caution against using this extension. I agree. It was a stupid perhaps this will make it compile try and error approach. Thanks oleg! Marc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] OO Design in Haskell Example (Draft)
Steve Downey wrote: In the last OO design in Haskell thread (and probably in every one preceeding it), it was suggested that having some examples might be a good idea. Since most people with existing designs will have some familiarity with Design Patterns, and those are typical building blocks for OO designs, it occured to me that implementing some of them might be a useful excersize. Have you looked at OOHaskell? http://homepages.cwi.nl/~ralf/OOHaskell/ http://darcs.haskell.org/OOHaskell/ With the exception of pure-functional objects and binary methods, I think we have considered almost every OO pattern/idiom we could find, including nominal/structural subtyping, co- and contra-variance, self-typing, etc. The DARCS repository contains the complete code for all of the examples and patterns. To clarify, the point of OOHaskell is to use Haskell as a tool, laboratory bench, for exploring various (thorny) OO issues. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Trouble with record syntax and classes
G'day all. Quoting Aaron McDaid [EMAIL PROTECTED]: 'class' in Haskell doesn't mean the same as 'class' in C++ or Java. I found it easier at first to thing of them as: A Haskell 'class' is more like a Java interface. Haskell types are more like what you might think of as 'class'es. Haskell 'instance' means Java 'implement' There is no word that means that same as 'instance' from Java/C++ terminology. I suppose we would call them 'values' or something. Somebody more knowledgeable can describe the etymology of the terms, but these 3 observations should help. When you type class Foo in Java or C++, it does three things: 1. It declares a new type called Foo. 2. It declares a _set_ of types (i.e. a class). 3. It declares that the type Foo (and all of its subtypes) is a member of the set of types Foo. In Haskell, these three operations are distinct. 1. You declare a new type using data or newtype. 2. You declare a new set of types using class. 3. You declare that a type is a member of a class using instance. Cheers, Andrew Bromage ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Splitting Hairs Over Terminology
Hi folks in C and C++ world the humble comma is an operator. Is this also the case in Haskell or, is it classed as a function? In the wikibook they talk about consing new elements onto a list. Does this cons stand for anything meaningful in the English language? For example, is it short for construction or something similar? I'm assuming that the : function takes two arguments and returns a newly constructed list which is assigned to the variable holding/pointing to the old list. Cheers Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Trouble with record syntax and classes
G'day all. Oh, one more thing. Quoting Aaron McDaid [EMAIL PROTECTED]: Somebody more knowledgeable can describe the etymology of the terms, [...] You can think of a type as a set of values. For example, Bool is the set { False, True }. A class, then, is a set of types. The distinction between set and class comes from the various set theories (Goedel-Bernays-von Neumann set theory being the most common) which try to avoid Russell's Paradox. For those who are don't know about Russell's Paradox, take a look at the Wikipedia entry before going on: http://en.wikipedia.org/wiki/Russell%27s_paradox The idea behind GBN set theory is to distinguish between sets, which are always well-behaved, and classes, which are not necessarily so well-behaved. Russell's Paradox is resolved by setting up your axioms such that the paradoxical set of all sets with property X is not, itself, a set, but a class. By analogy, we call a set of types, or a set of sets, a class. Cheers, Andrew Bromage ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: OO Design in Haskell Example (Draft)
I just started reading Haskell's overlooked object system. http://www.cwi.nl/%7Eralf/OOHaskell/ The survey of existing object encodings looks like a good place to start, although for several, where Either is used as a union type there are some rather obvious scaling problems. g If I've understood it, the OOHaskell library is meant to be a way of exploring OO in Haskell. Is it something that should be used by someone who wants to implement an OO design today? Or is it more for someone interested in research into the best way of doing OO in a functional context? I agree that there are a number of thorny OO issues, particularly that there really isn't a single OO model, rather a number of related models, practices and principles that are all lumped into the context of OO. Not to mention the tension between a model that revolves around mutable state against a system built on referential transparency. Mostly, I'd like to see better answers to questions like 'how do I do this' than here's something that will let you build something that lets you do that. I tend towards the engineering / reduction to practice side of things. Much as I like theory. And even if the answer is, there isn't really a best answer, but here are two or three reasonably good ways that won't cause too much trouble, and here's the kind of trouble they are likely to cause. On 2/26/07, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: Steve Downey wrote: In the last OO design in Haskell thread (and probably in every one preceeding it), it was suggested that having some examples might be a good idea. Since most people with existing designs will have some familiarity with Design Patterns, and those are typical building blocks for OO designs, it occured to me that implementing some of them might be a useful excersize. Have you looked at OOHaskell? http://homepages.cwi.nl/~ralf/OOHaskell/ http://darcs.haskell.org/OOHaskell/ With the exception of pure-functional objects and binary methods, I think we have considered almost every OO pattern/idiom we could find, including nominal/structural subtyping, co- and contra-variance, self-typing, etc. The DARCS repository contains the complete code for all of the examples and patterns. To clarify, the point of OOHaskell is to use Haskell as a tool, laboratory bench, for exploring various (thorny) OO issues. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe lists with GADT's
On Mon, 26 Feb 2007 17:28:59 -0800 (PST) [EMAIL PROTECTED] wrote: The problem with GADTs and other run-time based evidence is just that: _run-time_ based evidence and pattern-matching. In a non-strict system, checking that the evidence is really present is the problem on and of itself. That's a problem in any system that does not have both termination checking and exhaustive coverage checking. In this presence of both those checks, laziness is not a problem. BTW, Omega, Dependent ML and a few other systems with GADTs are strict. Omega does not yet have termination checking AFAIK, and Dependent ML has a more limited type language. Coq does have termination checking, and Neil Mitchell is working on a case-and-termination checker for Haskell. -- Robin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Splitting Hairs Over Terminology
P. R. Stanley wrote: You know, as soon as I posted the message I remembered the destructive assignment thingummy. the following is what I was talking about: Prelude 13:[1, 2] [13, 1, 2] which I don't believe has an address in the memory, correct? No. It does have a well-defined address in memory, which is there as long as you need it (and then garbage-collected away sometime thereafter). Back to the comma, surely, syntax sugar fulfills the role of an operator, a function, or a sequence of low-level procedures, either in part or comprehensively. The : is actually a constructor, which is a function that is fully evaluated at compile time and on which you can do pattern matching. The list syntax also forms such a pattern. In C, for example, iteration could be implemented using the if construct with the dreaded goto command. So, strictly speaking, the while loop could be classed as syntax sugar. Yet, the while loop is a well-recognized construct in its own right. I hope you can see what I'm driving at. Syntactic sugar is fully desugared at compile time. A while loop with constant limits *could* be considered syntactic sugar if the compiler can statically unroll the loop. Variable limits are definitely beyond this definition, since they can only be evaluated at runtime. Dan Weston ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Splitting Hairs Over Terminology
On 2/26/07, Dan Weston [EMAIL PROTECTED] wrote: P. R. Stanley wrote: In C, for example, iteration could be implemented using the if construct with the dreaded goto command. So, strictly speaking, the while loop could be classed as syntax sugar. Yet, the while loop is a well-recognized construct in its own right. I hope you can see what I'm driving at. Syntactic sugar is fully desugared at compile time. A while loop with constant limits *could* be considered syntactic sugar if the compiler can statically unroll the loop. Variable limits are definitely beyond this definition, since they can only be evaluated at runtime. I think what P.R. meant is that while loops in C can be desugared like this: while(condition) { stuff } more_stuff = loop: if(!condition) goto exit; stuff goto loop; exit: more_stuff No static unrolling of the loop happens. So in the sense of syntactic sugar that means a construct that can be defined in terms of other language constructs, while is syntactic sugar in C. Not sure what the original point was, though. Cheers, Kirsten -- Kirsten Chevalier* [EMAIL PROTECTED] *Often in error, never in doubt Are you aware that rushing toward a goal is a sublimated death wish? It's no coincidence we call them 'deadlines'. -- Tom Robbins ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Splitting Hairs Over Terminology
On Feb 26, 2007, at 22:17 , P. R. Stanley wrote: Prelude 13:[1, 2] [13, 1, 2] which I don't believe has an address in the memory, correct? If I understand what you're getting at: internally it just allocates a new cons cell, stuffs 13 in the left side and a pointer to the existing list [1, 2] in the right side, yes. Back to the comma, surely, syntax sugar fulfills the role of an operator, a function, or a sequence of low-level procedures, either in part or comprehensively. I suppose I'd have to go with the latter. In the formal constructor syntax (,,) it's just part of the operator name, but the tuple constructors are unique in that they don't need to be predeclared --- Haskell just looks for a parenthesized series of commas and counts the commas to find out the size of the tuple. (Note that the unit type () falls out of this as a degenerate case.) (1, 2, 3) is internally rewritten to (,,) 1 2 3, then parsed as the tuple constructor (,,) applied to the three arguments that constructor requires: Prelude :kind (,,) (,,) :: * - * - * - * Prelude :type (,,) (,,) :: a - b - c - (a, b, c) My point is that, syntactically, the comma can't really be considered a function or an operator per se; it's just special syntax. -- brandon s. allbery[linux,solaris,freebsd,perl] [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] Splitting Hairs Over Terminology
On 2/26/07, P. R. Stanley [EMAIL PROTECTED] wrote: Back to the comma, surely, syntax sugar fulfills the role of an operator, a function, or a sequence of low-level procedures, either in part or comprehensively. In C, for example, iteration could be implemented using the if construct with the dreaded goto command. So, strictly speaking, the while loop could be classed as syntax sugar. Yet, the while loop is a well-recognized construct in its own right. I hope you can see what I'm driving at. It's useful to see the square-bracket-and-comma list notation in Haskell as syntactic sugar because you don't need to worry about what it means; you just need to know how to mentally translate it into applications of cons and nil, and you already know what those means. Indeed, Haskell compilers are based on that same principle. Cheers, Kirsten -- Kirsten Chevalier* [EMAIL PROTECTED] *Often in error, never in doubt Apathy at the individual level translates into insanity at the mass level. -- Douglas Hofstadter ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Build failed - hidden package ?
Hi. I've got stuck with the following compilation error I probably can't fully understand: -- Building library... ... Using package config file: /usr/local/lib/ghc-6.6/package.conf wired-in package base mapped to base-2.0 wired-in package rts mapped to rts-1.0 wired-in package haskell98 mapped to haskell98-1.0 wired-in package template-haskell mapped to template-haskell-2.0 Hsc static flags: -static ... Graphics/UI/SDL/Rotozoomer.hs:15:7: Could not find module `Foreign.C': it is a member of package base, which is hidden -- What does such error mean ? Modules Foreign and Foreign.C are installed and available from the default path. Lines 12-15 of Rotozoomer.hs: -- module Graphics.UI.SDL.Rotozoomer where import Foreign import Foreign.C -- Any idea what's wrong, resp. some explanation why compilation fails ? Thanks in an advance. -- www.icqsms.cz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: OO Design in Haskell Example (Draft)
Steve Downey wrote: interesting. it leads to something that feels much more like an object based, as opposed to a class based, system. as far as haskell is concerned, everything has the same type, even though different instances have very different behavior. the question is, which plays nicer with the rest of haskell? that is, if i'm not committing to a closed dsl, which style is more likely to be reusable against other libraries. I suspect there's no right answer - it's a case of choosing the best approach for the problem. As an example, my charting library (http://dockerz.net/software/chart.html) uses the record of functions approach for composing drawings: data Renderable = Renderable { minsize :: (Render RectSize) render :: (Rect - Render ()) } Tim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Trouble with record syntax and classes
Thank you all for your advice so far. I went back and tried to simplify my code, but I'm still stuck. The basic idea I want is something like an arbitrary tree structure, where MetaSines are the branches containing Sines, and Sines are the leaves containing strings. I want to recurse through the tree and pick up all the leaf strings, but only if that branch/leaf is on for that time. Here's my second attempt at the code: data ISine = Sine Integer Integer Integer String | MetaSine Integer Integer Integer [ISine] letter (Sine _ _ _ l) = l sub_sines (MetaSine _ _ _ xs) = xs period p _ _ _ = p offset _ o _ _ = o threshold _ _ t _ = t on :: Integer-ISine-Bool on time (p o t x) = (mod (time-(offset p o t x)) (period p o t x)) (threshold p o t x) act time (MetaSine p o t s) |on time (p o t s) = foldr (++) (map (act time) (sub_sines p o t s)) |otherwise = [] act time (Sine p o t l) |on time p o t l = [letter p o t l] |otherwise = [] the on, period, offset, and threshold functions should work exactly the same for Sine and MetaSine, so I'd prefer to only write them once. But the act function needs to differentiate: for a Sine, it just returns a singleton list if on is true, or an empty list otherwise; but for a Metasine, it needs to get the list of all the strings in Sine objects in it's sub_sines field. It only does this if it's on. For example, let's say A / | \ B CD / | / | \ E FG H I If A, C, D, E, F and I are all on, only the strings of Sines C and I should be joined to make a to element list. If everything is on, C, E, F, G, H, I will all be joined. Anyway, the above code still doesn't work; there's a parse error for the definition of on. I don't think my arguments are right somehow. I appreciate your collective patience and expertise, and hope you can put me on the right track. Thomas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: AT solution: rebinding = for restricted monads
Pepe Iborra: David Roundy droundy at darcs.net writes: My latest attemp (which won't compile with the HEAD ghc that I just compiled, probably because I haven't figured out the synatax for guards with indexed types is: class WitnessMonad m where type W m :: * - * - * (=) :: (WitnessMonad m', WitnessMonad m'', w a b = W m', w b c = W m'', w a c = W m) = m' x - (x - m'' y) - m y () :: (WitnessMonad m', WitnessMonad m'', w a b = W m', w b c = W m'', w a c = W m) = m' x - m'' y - m y f g = f = const g return :: w a a = W m x = - m x fail :: String - m x data Witness a b instance Monad m = WitnessMonad m where W m = Witness () () (=) = Prelude.(=) () = Prelude.() return = Prelude.return fail = Prelude.fail which I think is quite pretty. It allows the Monadlike object to have kind * - *, while still allowing us to hide extra witness types inside and pull them out using the W function. Did anyone with knowledge of Associated Types pursue this solution? Where did you get this from. My haskell-cafe mail folder doesn't seem to have the thread you are replying to. It doesn't work with GHC head, and I can't really do anything about that. Mostly curiosity. The main reason this doesn't work with the head is because the implementation of associated type *synonyms* (as opposed to associated data types) is still incomplete. (See also http://haskell.org/haskellwiki/GHC/Indexed_types.) We are working at the implementation, but I just relocated from New York to Sydney, which is why not much happened in the last two months. But I also don't quite understand the intention of this code: * What exactly is the kind of the type function W supposed to be? Is it (* - *) - *? If so, then the declaration needs to be class WitnessMonad m where type W m :: * That is, assuming (m :: * - *), we have (W m :: *) with (W :: (* - *) - *). * In the signature (=) :: (WitnessMonad m', WitnessMonad m'', w a b = W m', w b c = W m'', w a c = W m) what is the purpose of w (and hence the purpose of the equality constraints)? What you really want is to impose a kind of state transition relationship on the monads involved in monad binds, right? * In the instance, using Prelude.= for the witness monad won't work. After all, Prelude.= can only combine two actions in the same monad, but the WitnessMonad signature promises to combine two different WitnessMonads (under certain constraints). * Another problem with the instance is that it requires undecidable instances. As I am not quite sure about the intention of the code it is hard to propose a fix. In particular, I have no idea how you want to combine two different witness monads in (=). Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Trouble with record syntax and classes
On Mon, 26 Feb 2007 23:41:14 -0600 (CST), you wrote: Here's my second attempt at the code: ... You've left out a bunch of constructors, and there are various other errors here and there. I think this will do what you want: data ISine = Sine Integer Integer Integer [Char] | MetaSine Integer Integer Integer [ISine] letter (Sine _ _ _ l) = l sub_sines (MetaSine _ _ _ xs) = xs period (Sine p _ _ _) = p period (MetaSine p _ _ _) = p offset (Sine _ o _ _) = o offset (MetaSine _ o _ _) = o threshold (Sine _ _ t _) = t threshold (MetaSine _ _ t _) = t on :: Integer - ISine - Bool on time iSine = (mod (time-(offset iSine)) (period iSine)) (threshold iSine) act :: Integer - ISine - [[Char]] act time (MetaSine p o t s) = if on time (MetaSine p o t s) then foldr1 (++) (map (act time) (sub_sines (MetaSine p o t s))) else [] act time (Sine p o t l) = if on time (Sine p o t l) then [letter (Sine p o t l)] else [] But note that you have to write the equations for period, offset and threshold twice. If you want to avoid that, you can move the Sine/MetaSine discrimination into the tail of the data structure, something like this: data ISineTail = SineTail [Char] | MetaTail [ISine] data ISine = ISine Integer Integer Integer ISineTail letter (ISine _ _ _ (SineTail l)) = l sub_sines (ISine _ _ _ (MetaTail xs)) = xs period (ISine p _ _ _) = p offset (ISine _ o _ _) = o threshold (ISine _ _ t _) = t on :: Integer - ISine - Bool on time iSine = (mod (time-(offset iSine)) (period iSine)) (threshold iSine) act :: Integer - ISine - [[Char]] act time (ISine p o t (MetaTail s)) = if on time (ISine p o t (MetaTail s)) then foldr1 (++) (map (act time) (sub_sines (ISine p o t (MetaTail s else [] act time (ISine p o t (SineTail l)) = if on time (ISine p o t (SineTail l)) then [letter (ISine p o t (SineTail l))] else [] Steve Schafer Fenestra Technologies Corp. http://www.fenestra.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe