RE: [Haskell-cafe] ANNOUNCE: pqueue-mtl, stateful-mtl
Henning Thielemann wrote: On Mon, 16 Feb 2009, Louis Wasserman wrote: Overnight I had the following thought, which I think could work rather well. The most basic implementation of the idea is as follows: class MonadST s m | m - s where liftST :: ST s a - m a instance MonadST s (ST s) where ... instance MonadST s m = MonadST ... Like MonadIO, isn't it? I think it should be, except that you need to track 's' somewhere. Ganesh == Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html == ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Hoogle and Network.Socket
On Thu, Feb 19, 2009 at 3:50 AM, Thomas DuBuisson thomas.dubuis...@gmail.com wrote: I recall that Niel made sure hoogle doesn't search through non-portable libraries (a shame), but I thought Network.Socket could be used on Windows and yet Hoogle does not give any results for 'socket' or any other functions within Network.Socket. First, am I mistaken and Network.Socket is POSIX only? I could swear it wasn't. Secondly - is there any chance of lifting the non-portable libraries ban, Niel? From the stand point of an application developer it might not sound good, but even in Haskell some software is system level and bound to be single platform (case and point: XCB, xmonad, hsXenCtrl). Judging by the amount of research in systems level functional programming I wouldn't be surprised to see this collection grow and making functions hard to find isn't productive. The Network.Socket module is for when you want full control over sockets. Essentially the entire C socket API is exposed through this module; in general the operations follow the behaviour of the C functions of the same name (consult your favourite Unix networking book). The C socket API in question is the POSIX one, I'm afraid. It has no exact equivalent on windows. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell.org GSoC
Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain: Haskell is a nice, mature and efficient programming language. By its very nature it could also become a nice executable formal specification language, provided there is tool support. Wouldn’t it be better to achieve the goals you describe with a dependently typed programming language? Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] package for algebraic structures
Am Donnerstag, 19. Februar 2009 00:17 schrieben Sie: On Tue, 17 Feb 2009, Wolfgang Jeltsch wrote: Now, a package only for one class with one method seems like overkill. However, it could serve as a start for a package of all kinds of algebraic structures. So I called the package “algebra” and put it on Hackage. So if someone wants to implement rings, ideals, fields or whatever, I’d be happy to receive patches. Do you mean this one: http://haskell.org/haskellwiki/Numeric_Prelude? There is currently no code for this, is there? In addition, I wouldn’t include algebraic structures in a *numerical* prelude since the cool thing about them is that they are so abstract that they are not only about numbers. However, then you might say that this package is overkill for Grapefruit since you only need the Semigroup class. What is the alternative to using a “numerical prelude” or the algebra package? Declaring the semigroup class inside Grapefruit? Then almost no library writer would define instances of this class. What’s the problem with Grapefruit having an additional dependency? If the package that is depended upon is open-source and automatically installable via cabal-install then the problems are little. On the other hand, you have the big advantage of modularization and thereby reuse of effort and consistency between different libraries (all use the same semigroup class). Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [darcs-users] darcs and Google Summer of Code
Am Donnerstag, 19. Februar 2009 05:10 schrieben Sie: Wolfgang Jeltsch wrote: I’ve put myself as a potential mentor on the old Haskell SoC ticket (http://hackage.haskell.org/trac/summer-of-code/ticket/17). However, one or two years ago I was told that mentoring is a very time-consuming thing (and to my knowledge, you don’t get any payments for that, at least for Haskell projects). So if some other person wants to mentor a Grapefruit-based GUI or patch viewer project, I’d be very happy and would support this person the best I can. Unless Google's changed things, the organization gets 500$ for each project. What the Darcs organization does with that, who knows. Yes, who knows. The “Haskell orgainization” didn’t give a cent to the mentors, as far as I know. Am I wrong here? It'd be a piddling amount as a stipend for the mentor, but... …it would be much better than nothing. :-) Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to create an online poll
Ketil == Ketil Malde ke...@malde.org writes: Ketil gregg reynolds d...@mobileink.com writes: I.e. war, plague.famine. etc. Ketil No, those are quite outdated by now. The new horsemen of Ketil the programming apocalypse are, of course, IO, Ketil MutableState, LazyMemoryLeak, and Bottom. And what are those four horsemen revealing? -- Colin Adams Preston Lancashire ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Hoogle and Network.Socket
The Network.Socket module works fine on Windows. The original Winsock implementation was based on the Berkeley sockets api. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell.org GSoC
2009/2/19 Wolfgang Jeltsch g9ks1...@acme.softbase.org Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain: Haskell is a nice, mature and efficient programming language. By its very nature it could also become a nice executable formal specification language, provided there is tool support. Wouldn't it be better to achieve the goals you describe with a dependently typed programming language? But I wonder how a dependent typed language can express certain properties, for example, the distributive property between the operation + and * in a ring or simply the fact that show(read x)==x. As far as I understand, a dependent type system can restrict the set of values for wich a function apply, but it can not express complex relationships between operations. My knowledge on dependent types is very limited. I would like to be wrong on this. The point is that permits the automatic checking of such properties at the class level (or module level) are critical, to make sure that derived instances agree with that. This would be very good to feel confident and program at higuer levels of abstraction. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A typeclass for Data.Map etc?
Greetings, Is there a typeclass for mappings with a Data.Map-like interface, with stuff like: empty, insert, insertWithKey, unionWith etc. ? And, probably, a similar typeclass for mutable mappings like Data.Hashtable. Looks like such a thing would be useful; as for now, I see at least two applications: Data.Map and Data.Trie (bytestring-trie) - it's a pity that they have rather similar interfaces, but the latter lacks many methods and some are named in a different way. Also, Data.Map has some inconsistensies, too: for instance, it has an insertWith' but lacks a unionWith'. One typeclass for all would eliminate these inconsistencies. I'm asking mainly because I've been wondering why noone has yet written a mutable hashtable package with a MArray-like interface, I wrote a small thing myself and I am unsure as to what interface it should have. -- Eugene Kirpichov ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: How to create an online poll
Ketil Malde wrote: Rick R writes: I'm sure Premier Election Solutions (formerly Diebold) can provide us with an online voting solution. You know, while the recent voting scandals have been milked for all they're worth by the open source community, FP has been very quiet about it. I think that's because FP is guilty of inventing the circular time traveling knots^1 used to correctly predict future election results in the first place. ^1 See also Russel O'Connor's article in http://www.haskell.org/sitewiki/images/1/14/TMR-Issue6.pdf Regards, apfelmus -- http://apfelmus.nfshost.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell.org GSoC
This could look like: module Integer where .. theorem read_parses_what_show_shows : (a :: Integer, Show a, Read a) = show . read a = id a proof axiom There are several problems with this approach. For example, I can show: const 0 (head []) = 0 But if I pretend that I don't know that Haskell is lazy: const 0 (head []) = const 0 (error ) = error ... Which would allow me to substitute each occurrence of 0 with error - which probably isn't a good idea. So to do proper equational reasoning in a lazy language you need to be extremely careful with evaluation order. Predicting the evaluation order of code generated by ghc -O2 Main.hs is non-trivial to say the least. To make matters worse, as you're working in a language with general recursion, you have to be fight quite hard to avoid introducing inconsistencies in your proof language. Alberto wrote: As far as I understand, a dependent type system can restrict the set of values for wich a function apply, but it can not express complex relationships between operations. My knowledge on dependent types is very limited. I would like to be wrong on this. I'm sorry, but you're wrong. Dependent types can encode the kind of equational proofs Sylvain mentioned perfectly adequately. Lennart Augustsson has a nice note explaining the principle in the context of Cayenne: http://www.cs.chalmers.se/~augustss/cayenne/eqproof.ps The good news is: in languages like Coq and Agda you can write total functional programs, like map or ++, verify such properties and extract Haskell code. Hope this helps, Wouter ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [darcs-users] darcs and Google Summer of Code
Unless Google's changed things, the organization gets 500$ for each project. What the Darcs organization does with that, who knows. Yes, who knows. The Haskell organization didn't give a cent to the mentors, as far as I know. Am I wrong here? That is correct. The haskell.org mentors decided to spend the money on hosting the haskell.org and community.haskell.org web sites and services, to benefit the whole community rather than just themselves. Regards, Malcolm ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Ready for testing: Unicode support for Handle I/O
Bulat Ziganshin wrote: Hello Khudyakov, Saturday, February 7, 2009, 4:01:57 PM, you wrote: How do you plan to handle filenames? Currently FilePath is simply a string. i think that this patch does nothing to unicode filenames support Correct - I'm aware that there's a problem with filenames, but it hasn't been tackled yet. There probably isn't anything sensible that we can do without changing FilePath into an ADT. Cheers, Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
Jonathan Cast-2 wrote: Summary: Existential types are not enough for ST. You need the rank 2 type, to guarantee that *each* application of runST may (potentially) work with a different class of references. (A different state thread). Interesting. What's going on in the example that you posted seems to be a stronger but still familiar version of there exists, namely there exists exactly one a.k.a. there uniquely exists, often represented with exists-bang: exists!. The problem is that given [1] exists! a. (U[a] -V) we can constructively derive [2] (forall a. U[a]) - V even though the program/proof of [2] derived from [1] is deficient as you've explained. In Haskell, the only existential quantification is exists-bang. The weaker form of existence is sufficient to regain thread safety for runST. Every application of a program of type (exists-w/o-bang a. U[a]) simply cannot assume that the (a) is always the same. What would be a suitable logic for framing these kinds of analyses I wonder? -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22099322.html 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] Re[2]: Ready for testing: Unicode support for Handle I/O
Hello Simon, Thursday, February 19, 2009, 3:21:03 PM, you wrote: Correct - I'm aware that there's a problem with filenames, but it hasn't been tackled yet. There probably isn't anything sensible that we can do without changing FilePath into an ADT. i think that FilePath=String is ok, we just need to use utf8 string encoding on unix/macs and utf-16 encoding with *W functions on Windows. i have implemented such support inside my own application, and would be happy to mentor appropriate gsoc project -- Best regards, Bulatmailto:bulat.zigans...@gmail.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
On Thursday 19 February 2009 7:22:48 am Kim-Ee Yeoh wrote: Jonathan Cast-2 wrote: Summary: Existential types are not enough for ST. You need the rank 2 type, to guarantee that *each* application of runST may (potentially) work with a different class of references. (A different state thread). Interesting. What's going on in the example that you posted seems to be a stronger but still familiar version of there exists, namely there exists exactly one a.k.a. there uniquely exists, often represented with exists-bang: exists!. The problem is that given [1] exists! a. (U[a] -V) we can constructively derive [2] (forall a. U[a]) - V even though the program/proof of [2] derived from [1] is deficient as you've explained. I don't think there's anything wrong with that. The forall version works for ST refs, and the exists version does not. This is generalized by the fact that one cannot write a function with type: ((forall a. U[a]) - V) - (exists a. U[a] - V) By contrast, the fact that you can write a function with type: (exists a. U[a] - V) - ((forall a. U[a]) - V) would indicate that anything that can be handled with the exists type could also be handled by the forall type. In Haskell, the only existential quantification is exists-bang. The weaker form of existence is sufficient to regain thread safety for runST. Every application of a program of type (exists-w/o-bang a. U[a]) simply cannot assume that the (a) is always the same. Correct me if I'm wrong, but isn't this 'merely' what the constructive existential is (which is what you get in the usual type theories, not the classical existential)? An existential: exists a:T. P(a) is a pair of some a with type T and a proof that a satisfies P (which has type P(a)). In Haskell, T is some kind, and P(a) is some type making use of a. That doesn't mean that there is only one a:T for which P is satisfied. But it *does* mean that for any particular proof of exists a:T. P(a), only one a:T is involved. So if you can open that proof, then you know that that is the particular a you're dealing with, which leads to the problems in the grandparent. Cheers, -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell.org GSoC
Am Donnerstag, 19. Februar 2009 11:35 schrieb Alberto G. Corona: 2009/2/19 Wolfgang Jeltsch g9ks1...@acme.softbase.org Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain: Haskell is a nice, mature and efficient programming language. By its very nature it could also become a nice executable formal specification language, provided there is tool support. Wouldn't it be better to achieve the goals you describe with a dependently typed programming language? But I wonder how a dependent typed language can express certain properties, for example, the distributive property between the operation + and * in a ring or simply the fact that show(read x)==x. As far as I understand, a dependent type system can restrict the set of values for wich a function apply, but it can not express complex relationships between operations. Each type system corresponds to some constructive logic and can enforce properties which are expressible in that logic. Dependent type systems correspond to higher order predicate logics or so and therefore can express almost everything you want. An Agda or Epigram type can cover a complete behavioral specification like “This function turns a list into its sorted equivalent.” Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A typeclass for Data.Map etc?
On Thu, Feb 19, 2009 at 9:51 PM, Eugene Kirpichov ekirpic...@gmail.com wrote: Greetings, Is there a typeclass for mappings with a Data.Map-like interface, with stuff like: empty, insert, insertWithKey, unionWith etc. ? And, probably, a similar typeclass for mutable mappings like Data.Hashtable. Looks like such a thing would be useful; as for now, I see at least two applications: Data.Map and Data.Trie (bytestring-trie) - it's a pity that they have rather similar interfaces, but the latter lacks many methods and some are named in a different way. Also, Data.Map has some inconsistensies, too: for instance, it has an insertWith' but lacks a unionWith'. One typeclass for all would eliminate these inconsistencies. I'm asking mainly because I've been wondering why noone has yet written a mutable hashtable package with a MArray-like interface, I wrote a small thing myself and I am unsure as to what interface it should have. Probably not adding anything terribly useful to this except to say that it'd be useful to me too - I've written a binding to a perfect hashing library (PerfectHash on hackage) which implements only 'fromList' and 'lookup', so a slightly more fine-grained type class hierarchy would be nice. (This particular implementation is useful when you have a lot of keys, but all known at run-time.) Mark -- A UNIX signature isn't a return address, it's the ASCII equivalent of a black velvet clown painting. It's a rectangle of carets surrounding a quote from a literary giant of weeniedom like Heinlein or Dr. Who. -- Chris Maeda ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell.org GSoC
Unfortunately the proofs in dependently typed languages are extremely long and tedious to write. Some kind of compiler proofing tool could ease the pain, but I do not think it has low enough complexity for a GSoC project. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Feb 19, 2009, at 1:37 AM, Wolfgang Jeltsch wrote: Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain: Haskell is a nice, mature and efficient programming language. By its very nature it could also become a nice executable formal specification language, provided there is tool support. Wouldn’t it be better to achieve the goals you describe with a dependently typed programming language? Best wishes, Wolfgang ___ 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] Haskell.org GSoC
Yes, this is indeed the point. Right now we express properties that a type class should obey, but there is no compiler assistance to prove or verify them. A compiler aware of properties can do additional symbolic manipulation to increase performance. Surely there has been some research in this area already. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Feb 19, 2009, at 3:35 AM, Alberto G. Corona wrote: 2009/2/19 Wolfgang Jeltsch g9ks1...@acme.softbase.org Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain: Haskell is a nice, mature and efficient programming language. By its very nature it could also become a nice executable formal specification language, provided there is tool support. Wouldn't it be better to achieve the goals you describe with a dependently typed programming language? But I wonder how a dependent typed language can express certain properties, for example, the distributive property between the operation + and * in a ring or simply the fact that show(read x)==x. As far as I understand, a dependent type system can restrict the set of values for wich a function apply, but it can not express complex relationships between operations. My knowledge on dependent types is very limited. I would like to be wrong on this. The point is that permits the automatic checking of such properties at the class level (or module level) are critical, to make sure that derived instances agree with that. This would be very good to feel confident and program at higuer levels of abstraction. ___ 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] forall ST monad
There's a lot to chew on (thank you!), but I'll just take something I can handle for now. Dan Doel wrote: An existential: exists a:T. P(a) is a pair of some a with type T and a proof that a satisfies P (which has type P(a)). In Haskell, T is some kind, and P(a) is some type making use of a. That doesn't mean that there is only one a:T for which P is satisfied. But it *does* mean that for any particular proof of exists a:T. P(a), only one a:T is involved. So if you can open that proof, then you know that that is the particular a you're dealing with, which leads to the problems in the grandparent. re: Constructivity and the opening of a proof A form of the theorem that the primes are infinite goes Given a finite set of primes, there's a prime bigger than any of them. The usual proof is constructive since factorization is algorithmic, but I don't see why a priori, applications of this theorem on a given input should always yield the same prime when more than one factor exists. Is non-deterministic choice forbidden in constructive math? A cursory google seems to suggest that if not, it's at least a bête noire to some. -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22100873.html 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
Re: [Haskell-cafe] A typeclass for Data.Map etc?
On Thu, Feb 19, 2009 at 2:46 PM, Mark Wotton mwot...@gmail.com wrote: On Thu, Feb 19, 2009 at 9:51 PM, Eugene Kirpichov ekirpic...@gmail.com wrote: Greetings, Is there a typeclass for mappings with a Data.Map-like interface, with stuff like: empty, insert, insertWithKey, unionWith etc. ? And, probably, a similar typeclass for mutable mappings like Data.Hashtable. There are some apparently useful classes for this sort of thing in the EdisonAPI package, with corresponding implementations in EdisonCore. Have a look. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Uses of `fix' combinator
Hello, While browsing documentation I've found following function -- | @'fix' f@ is the least fixed point of the function @f@, -- i.e. the least defined @x@ such that @f x = x...@. fix :: (a - a) - a fix f = let x = f x in x I have two questions. How could this function be used? I'm unable to imagine any. Naive approach lead to nothing (no surprise): Prelude Data.Function fix (^^2) interactive: out of memory (requested 2097152 bytes) Second question what does word `least' mean?`a' isn't an Ord instance. -- Khudyakov Alexey ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Uses of `fix' combinator
On Thu, 2009-02-19 at 17:00 +0300, Khudyakov Alexey wrote: Hello, While browsing documentation I've found following function -- | @'fix' f@ is the least fixed point of the function @f@, -- i.e. the least defined @x@ such that @f x = x...@. fix :: (a - a) - a fix f = let x = f x in x I have two questions. How could this function be used? I'm unable to imagine any. Naive approach lead to nothing (no surprise): Prelude Data.Function fix (^^2) interactive: out of memory (requested 2097152 bytes) Second question what does word `least' mean?`a' isn't an Ord instance. Least defined, i.e. least in the definability order where undefined = anything (hence also being called bottom) and, say, Just undefined = Just 3 and 1 /= 2 and 2 /= 1. Fix is the basic mechanism supporting recursion (theoretically). The idea is when you have a recursive definition, you can abstract out the recursive uses and apply fix to the resulting function, e.g. ones = 1:ones ones = fix (\ones - 1:ones) fact 0 = 1 fact n | n 1 = n * fact (n-1) fact = fix (\fact n - case n of 0 - 1; _ | n 1 - n * fact (n - 1)) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Overloading functions based on arguments?
On Feb 14, 2009, at 2:29 PM, Luke Palmer wrote: To me, typeclasses are at their best when you have a real abstraction to encode. I agree. If you are having trouble using a typeclass and need C++-style ad- hoc overloading, it's likely you are trying to encode a fake abstraction -- one that has only linguistic, rather than mathematical meaning. I don't think what you're calling a linguistic abstraction is fake. Words and operators have connotations in the minds of those reading them. There's a reason I choose the word, 'flatten' rather than 'sdj834' to name a function -- because the word 'flatten' suggests what I am trying to accomplish with the function. Let's try a little test: 1. If the parameter is a tree, what do you think flatten would do? 2. If the parameter is a list, what do you think flatten would do? 3. If the parameter is a Style (possible a composite Style consisting of other styles), what do you think flatten would do? 4. If the parameter is a Bezier curve, what do you think flatten would do? My guess is that we would come to the same conclusions for (1) - (4). The name flatten is a perfectly good name for all of these operations, because the domains are distinct, and because using that name suggests the correct meaning to you. (Note use of the word suggests -- like an analogy or parable, you're likely not going to know exactly what the function does just by reading its name, but you'll be in the ballpark and have an intuition about it, which is extremely valuable.) In the current world, flatten will be appended with (usually non- informative) suffixes, or alternate, less-descriptive names chosen. Informative coding is about drawing upon our common pool of experience to mold the form and function of programs to suggest our intentions to others. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [darcs-users] darcs and Google Summer of Code
Am Donnerstag, 19. Februar 2009 12:37 schrieb Malcolm Wallace: Unless Google's changed things, the organization gets 500$ for each project. What the Darcs organization does with that, who knows. Yes, who knows. The Haskell organization didn't give a cent to the mentors, as far as I know. Am I wrong here? That is correct. The haskell.org mentors decided to spend the money on hosting the haskell.org and community.haskell.org web sites and services, to benefit the whole community rather than just themselves. Hmm, mentoring a project also benefits the whole community and not just the mentors. So even if mentors take the money, the community wins. Resources are limited. The more limited a resource is, the more painful it is to abandon parts of it. This is also true for my time. If keeping valuable time is better for me than getting a software project done then I chose to keep the time. Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell.org GSoC
Am Donnerstag, 19. Februar 2009 14:50 schrieb John A. De Goes: Unfortunately the proofs in dependently typed languages are extremely long and tedious to write. Some kind of compiler proofing tool could ease the pain, but I do not think it has low enough complexity for a GSoC project. I was not saying that I want such a thing done as a GSoC project. I just wanted to say that if one wants a programming language with an integrated proof language, it might be better to put work into Agda or Epigram instead of extending Haskell. Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
On Thu, 2009-02-19 at 05:53 -0800, Kim-Ee Yeoh wrote: There's a lot to chew on (thank you!), but I'll just take something I can handle for now. Dan Doel wrote: An existential: exists a:T. P(a) is a pair of some a with type T and a proof that a satisfies P (which has type P(a)). In Haskell, T is some kind, and P(a) is some type making use of a. That doesn't mean that there is only one a:T for which P is satisfied. But it *does* mean that for any particular proof of exists a:T. P(a), only one a:T is involved. So if you can open that proof, then you know that that is the particular a you're dealing with, which leads to the problems in the grandparent. re: Constructivity and the opening of a proof A form of the theorem that the primes are infinite goes Given a finite set of primes, there's a prime bigger than any of them. The usual proof is constructive since factorization is algorithmic, but I don't see why a priori, applications of this theorem on a given input should always yield the same prime when more than one factor exists. They don't. Any particular constructive proof will yield a particular new bigger prime, but they don't have to yield the same one. Let's choose a simpler example: There exists an Integer. Any (constructive) proof of that proposition is just an Integer and thus certainly a particular Integer. However, there is nothing special about any particular Integer. Is non-deterministic choice forbidden in constructive math? A cursory google seems to suggest that if not, it's at least a bête noire to some. Not particularly, but if you ultimately want an executable algorithm, you are sooner or later going to have to spell out how such a non-deterministic choice is made. -Proof-search-, though, is usually quite non-deterministic. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re[2]: Ready for testing: Unicode support for Handle I/O
Hello Khudyakov, Thursday, February 19, 2009, 4:06:06 PM, you wrote: i think that FilePath=String is ok, we just need to use utf8 string encoding on unix/macs and utf-16 encoding with *W functions on Windows. i have implemented such support inside my own application, and would be happy to mentor appropriate gsoc project It won't _always_ work. current solution works never :) And there are still 8-bit locales lurking somewhere in bush. UTF8 isn't appropriate for them at all. i think that SetFilenameEncoding whould solve this, among with access to lower-level openFileUsingCStringPath -- Best regards, Bulatmailto:bulat.zigans...@gmail.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Uses of `fix' combinator
Hello Khudyakov, Thursday, February 19, 2009, 5:00:03 PM, you wrote: I have two questions. How could this function be used? I'm unable to imagine any. Naive approach lead to nothing (no surprise): fix (1:) -- Best regards, Bulatmailto:bulat.zigans...@gmail.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Overloading functions based on arguments?
On Feb 14, 2009, at 11:28 PM, wren ng thornton wrote: John A. De Goes wrote: On Feb 13, 2009, at 2:11 PM, Jonathan Cast wrote: The compiler should fail when you tell it two mutually contradictory things, and only when you tell it two mutually contradictory things. By definition, it's not a contradiction when the symbol is unambiguously typeable. Do you think math textbooks are filled with contradictions when they give '+' a different meaning for vectors than matrices or real numbers??? Yes. Yes, I do. If you really think you have discovered a contradiction in tens of thousands of mathematical textbooks, then you should write a paper and submit it to the AJM. Now me, I DON'T think you've discovered a contradiction. I don't even think YOU believe that. Rather, you're fixated on using a unique, precise meaning for each symbol. Somehow this is associated for you with some notion of purity. But I'm guessing, if I take a look at all the source code you have ever written in your entire life, you will not have as many unique symbols as you have functions and operators. You probably reuse names and operators just like the rest of us. It is precisely this abuse of notation which makes, for instance, statistics textbooks impossible to read (without already knowing the material). Hmmm, I don't find statistics books difficult to read. Scalars, vectors, and matrices are fundamentally different here and the operations on them should be unambiguous, regardless of context. It's customary to use a unique typeface and/or font for each domain. So you know the type of the variables by inspection, and the meaning of the operators flows from that. Matrices, for example, are generally denoted in all uppercase (smallcaps), with an italic font, and often with the letters 'M' or 'N' and subscripts. Vectors are usually all lower-case and italic, sometimes with tiny arrows above them, and usually they're represented with the letters u, v, and w (and subscripted versions thereof). With unique domains, reuse of the symbols such as '+' for vector and matrix addition is unambiguous and perfectly sensible because it suggests that at some level, the operation reduces to scalar addition (which is correct). Compare that to using unique symbols for every possible operator and function. That would be brain overload because you would have to memorize each symbol and function separately. For another example, consider matrices vs their transposes. Many folks can't be bothered to type a single character to clarify when things should be transposed before multiplying. Now that's just plain sloppiness, and is quite orthogonal to this discussion. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: pqueue-mtl, stateful-mtl
It does. In the most recent version, the full class declaration runs class MonadST m where type StateThread m liftST :: ST (StateThread m) a - m a and the StateThread propagates accordingly. Louis Wasserman wasserman.lo...@gmail.com On Thu, Feb 19, 2009 at 2:10 AM, Sittampalam, Ganesh ganesh.sittampa...@credit-suisse.com wrote: Henning Thielemann wrote: On Mon, 16 Feb 2009, Louis Wasserman wrote: Overnight I had the following thought, which I think could work rather well. The most basic implementation of the idea is as follows: class MonadST s m | m - s where liftST :: ST s a - m a instance MonadST s (ST s) where ... instance MonadST s m = MonadST ... Like MonadIO, isn't it? I think it should be, except that you need to track 's' somewhere. Ganesh == Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html == ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Uses of `fix' combinator
By the way, the fact that least is in the sense of least defined explains why fix (2^) gives an undefined: The least defined fixpoint of any strict function (f : f _|_ = _|_) is, by definition, undefined. And (2^) is strict. 2009/2/19 Derek Elkins derek.a.elk...@gmail.com: On Thu, 2009-02-19 at 17:00 +0300, Khudyakov Alexey wrote: Hello, While browsing documentation I've found following function -- | @'fix' f@ is the least fixed point of the function @f@, -- i.e. the least defined @x@ such that @f x = x...@. fix :: (a - a) - a fix f = let x = f x in x I have two questions. How could this function be used? I'm unable to imagine any. Naive approach lead to nothing (no surprise): Prelude Data.Function fix (^^2) interactive: out of memory (requested 2097152 bytes) Second question what does word `least' mean?`a' isn't an Ord instance. Least defined, i.e. least in the definability order where undefined = anything (hence also being called bottom) and, say, Just undefined = Just 3 and 1 /= 2 and 2 /= 1. Fix is the basic mechanism supporting recursion (theoretically). The idea is when you have a recursive definition, you can abstract out the recursive uses and apply fix to the resulting function, e.g. ones = 1:ones ones = fix (\ones - 1:ones) fact 0 = 1 fact n | n 1 = n * fact (n-1) fact = fix (\fact n - case n of 0 - 1; _ | n 1 - n * fact (n - 1)) ___ 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] Uses of `fix' combinator
Each data type in Haskell contains one element, which is usually invisible. It's called bottom and denoted by (_|_). Naturally (_|_) of type Int and (_|_) of type Char are different; however, they are denoted as if they are the same, 'cause there isn't much difference between them. Anyway, if you try to calculate something which happens to be (_|_) and your program would throw an error or loop forever. Now, since there is (_|_)::Int and (_|_)::Char, there are also ((_|_), (_|_)) :: (Int, Char) as well as (1, (_|_)) :: (Int, Char) and ((_|_), 'a') :: (Int, Char); all of them are different from (_|_) :: (Int, Char). If a value contains (_|_) somewhere inside it, we say that it is less defined than the value obtained from it by replacing (_|_)s with something else. For example, (_|_) is less defined than ((_|_),(_| _)), which is less defined than (1, (_|_)) or ((_|_), 'a'); and both of them are less defined than (1, 'a'). 'fix' is a function which maps a function 'f' to the LEAST defined x such that f x = x. Such 'x' always exists; it could be (_|_), but it could be something else. For example, (^^2) is a strict function, which means that (_|_)^^2 = (_|_); therefore fix (^^2) = (_|_) - which you've discovered yourself. A stupid example: fix (\a - (1, snd a)) = (1, (_|_)). (_|_) is not the right answer: (\a - (1, snd a)) (_|_) = (1, snd (_|_)) = (1, (_| _)) which isn't (_|_). Another, less stupid example: fix (\a - (1, fst a)) = (1, 1) - which doesn't contain (_|_) anywhere inside it. See, (_|_) is not the right answer here: (\a - (1, fst a)) (_|_) = (1, fst (_|_)) = (1, (_|_)), which isn't (_|_). But (1, (_|_)) is not the right answer either: (\a - (1, fst a)) (1, (_|_)) = (1, fst (1, (_|_))) = (1, 1). On 19 Feb 2009, at 17:00, Khudyakov Alexey wrote: Hello, While browsing documentation I've found following function -- | @'fix' f@ is the least fixed point of the function @f@, -- i.e. the least defined @x@ such that @f x = x...@. fix :: (a - a) - a fix f = let x = f x in x I have two questions. How could this function be used? I'm unable to imagine any. Naive approach lead to nothing (no surprise): Prelude Data.Function fix (^^2) interactive: out of memory (requested 2097152 bytes) Second question what does word `least' mean?`a' isn't an Ord instance. -- Khudyakov Alexey ___ 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] Re: Overloading functions based on arguments?
On Thu, Feb 19, 2009 at 7:09 AM, John A. De Goes j...@n-brain.net wrote: On Feb 14, 2009, at 2:29 PM, Luke Palmer wrote: To me, typeclasses are at their best when you have a real abstraction to encode. I agree. If you are having trouble using a typeclass and need C++-style ad-hoc overloading, it's likely you are trying to encode a fake abstraction -- one that has only linguistic, rather than mathematical meaning. I don't think what you're calling a linguistic abstraction is fake. Please ignore the word fake. I don't want to get into any subjective arguments based on the connotation of that word. What I mean to say is, the theory of typeclasses is good at encoding mathematical abstractions, and bad at encoding linguistic ones. Take that as you will, but I conjecture that trying to cram linguistic overloading into a typeclass is generally going to be painful. A good rule of thumb is: are there any algorithms which work for an arbitrary member of this class? I certainly cannot see any for your flatten example. I'm not saying that linguistic overloading is a bad thing. You make good arguments for it, and I find it cleans up code sometimes. Typeclasses just aren't the right tool for it, and Haskell has no good tool for it. In fact, I think it a very interesting research question to come up with a mechanism that supports linguistic overloading, and interacts with typeclasses and inference cleanly. The obvious solution (just look in your namespace for one that matches) has serious drawbacks, and nothing else is jumping to mind. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell.org GSoC
Unfortunately the proofs in dependently typed languages are extremely long and tedious to write. Some kind of compiler proofing tool could ease the pain, but I do not think it has low enough complexity for a GSoC project. I wouldn't say that. Here's the complete proof script in Coq proving the theorem that was originally proposed: length (map f (xs ++ ys)) = length xs + length ys. It weighs in at about 30 lines, although I could probably get it down to less than 10. The proofs maybe look a bit unfamiliar if you haven't seen Coq before, but they are hardly extremely long and tedious to write. I can understand that raw proof *terms* in type theory can be long and painful to write. But that's like saying Haskell is bad, because its hard to understand ghc-core. Wouter Require Import List. Variables a b : Set. Variable f : a - b. Lemma lengthMap : forall (xs : list a), length (map f xs) = length xs. Proof. intros. induction xs; trivial. simpl; rewrite IHxs. reflexivity. Qed. Lemma appendLength : forall (xs ys : list a), length (xs ++ ys) = length xs + length ys. Proof. intros. induction xs; trivial. simpl; rewrite IHxs. reflexivity. Qed. Lemma main : forall (xs ys : list a), length (map f (xs ++ ys)) = length xs + length ys. Proof. intros. rewrite lengthMap. rewrite appendLength. reflexivity. Qed. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Overloading functions based on arguments?
I agree that type classes should not be used for this purpose. That's part of the reason I support linguistic overloading -- to stop the type class abuse. Type classes should be used, as you say, when there are algorithms that work for arbitrary members -- i.e. the type class encodes structure and associated properties. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Feb 19, 2009, at 7:33 AM, Luke Palmer wrote: On Thu, Feb 19, 2009 at 7:09 AM, John A. De Goes j...@n-brain.net wrote: On Feb 14, 2009, at 2:29 PM, Luke Palmer wrote: To me, typeclasses are at their best when you have a real abstraction to encode. I agree. If you are having trouble using a typeclass and need C++-style ad- hoc overloading, it's likely you are trying to encode a fake abstraction -- one that has only linguistic, rather than mathematical meaning. I don't think what you're calling a linguistic abstraction is fake. Please ignore the word fake. I don't want to get into any subjective arguments based on the connotation of that word. What I mean to say is, the theory of typeclasses is good at encoding mathematical abstractions, and bad at encoding linguistic ones. Take that as you will, but I conjecture that trying to cram linguistic overloading into a typeclass is generally going to be painful. A good rule of thumb is: are there any algorithms which work for an arbitrary member of this class? I certainly cannot see any for your flatten example. I'm not saying that linguistic overloading is a bad thing. You make good arguments for it, and I find it cleans up code sometimes. Typeclasses just aren't the right tool for it, and Haskell has no good tool for it. In fact, I think it a very interesting research question to come up with a mechanism that supports linguistic overloading, and interacts with typeclasses and inference cleanly. The obvious solution (just look in your namespace for one that matches) has serious drawbacks, and nothing else is jumping to mind. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Uses of `fix' combinator
Thankyou everyone. This was most helpful. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A typeclass for Data.Map etc?
2009/2/19 Eugene Kirpichov ekirpic...@gmail.com: Is there a typeclass for mappings with a Data.Map-like interface, with stuff like: empty, insert, insertWithKey, unionWith etc. ? Maybe this is of interest: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/gmap Peter ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to create an online poll
I think the capabilities community including E and Coyotos/BitC have extensively addressed this topic. Coyotos is taking the correct approach for trusted voting platform. Since, even if your software is trustworthy, it can't be trusted if the OS on which it runs is suspect. However, we might have a few more rigged elections before we see any deliverables from Coyotos. On Thu, Feb 19, 2009 at 2:45 AM, Ketil Malde ke...@malde.org wrote: Rick R rick.richard...@gmail.com writes: I'm sure Premier Election Solutions (formerly Diebold) can provide us with an online voting solution. You know, while the recent voting scandals have been milked for all they're worth by the open source community, FP has been very quiet about it. Isn't this an application where correctness matters? How about a proof that the software never loses (or injects) votes, for instance? -k -- If I haven't seen further, it is by standing in the footprints of giants -- We can't solve problems by using the same kind of thinking we used when we created them. - A. Einstein ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] ANNOUNCE: Cabal-1.6.0.2 and cabal-install-0.6.2
I'm pleased to announce point-releases of the Cabal library and the cabal-install command line tool. If you are already using cabal-install then you can upgrade both using: $ cabal update $ cabal install Cabal cabal-install New users you can get it from: http://haskell.org/cabal/download.html For users on unix systems there is a source tarball with a bootstrap script. For users on Windows systems there is a pre-compiled cabal.exe. Release notes = Cabal-1.6.0.2 - This is a point-release in the stable 1.6.x series. It is expected that this release will be included with ghc-6.10.2. It has a number of fixes and minor improvements. The most noticeable change is that Cabal now checks at configure time that C libraries and header files are available. This is known to break a small number of packages. The maintainers of these packages have been notified. Changes since 1.6.0.1: * New configure-time check for C headers and libraries * Added language extensions present in ghc-6.10 * Added support for NamedFieldPuns extension in ghc-6.8 * Fix in configure step for ghc-6.6 on Windows * Fix warnings in Path_pkgname.hs module on Windows * Fix for exotic flags in ld-options field * Fix for using pkg-config in a package with a lib and an executable * Fix for building haddock docs for exes that use the Paths module * Fix for installing header files in subdirectories * Fix for the case of building profiling libs but not ordinary libs * Fix read-only attribute of installed files on Windows * Ignore ghc -threaded flag when profiling in ghc-6.8 and older cabal-install-0.6.2 --- This release contains a number of incremental improvements, including some new features. We expect to do another 0.6.x release in the not too distant future focusing on improvements in the way package dependencies are selected. Changes since 0.6.0: * The upgrade command has been disabled in this release * The configure and install commands now have consistent behaviour * Reduce the tendency to re-install already existing packages * The --constraint= flag now works for the install command * New --preference= flag for soft constraints / version preferences * Improved bootstrap.sh script, smarter and better error checking * New cabal info command to display detailed info on packages * New cabal unpack command to download and untar a package * HTTP-4000 package required, should fix bugs with http proxies * Now works with authenticated proxies. * On Windows can now override the proxy setting using an env var * Fix compatibility with config files generated by older versions * Warn if the hackage package list is very old * More helpful --help output, mention config file and examples * Better documentation in ~/.cabal/config file * Improved command line interface for logging and build reporting * Minor improvements to some messages Changes since 0.5.2: * Constraint solver can now cope with base 3 and base 4 * Allow use of package version preferences from hackage index * More detailed output from cabal install --dry-run -v * Improved bootstrap.sh Bugs and feature requests = This is an excellent opportunity to make sure your favourite bug or feature request is properly described in our bug tracker: http://hackage.haskell.org/trac/hackage/ To help us guide development priorities please add yourself to the ticket's cc list and describe why that bug or feature is important to you. Credits === On behalf of the Cabal hackers and the community generally I'd like to thank the people who have contributed patches for these releases: * Gleb Alexeyev * Samuel Bronson * Thomas Schilling * Ganesh Sittampalam * Andrea Vezzosi Get involved There's still a lot to do! We have big plans for Cabal-2.0, cabal-install and the Hackage website. So if you're interested in helping out with this core infrastructure project then: * subscribe to the cabal-devel mailing list: http://www.haskell.org/mailman/listinfo/cabal-devel * grab the source: http://haskell.org/cabal/code.html * read the guide to the source code: http://hackage.haskell.org/trac/hackage/wiki/SourceGuide * take a look at our list of bugs and feature requests: http://hackage.haskell.org/trac/hackage/report/12 especially the easy tickets: http://hackage.haskell.org/trac/hackage/report/13 Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to create an online poll
2009/2/19 Rick R rick.richard...@gmail.com I think the capabilities community including E and Coyotos/BitC have extensively addressed this topic. Coyotos is taking the correct approach for trusted voting platform. Since, even if your software is trustworthy, it can't be trusted if the OS on which it runs is suspect. Woah, that's a pretty interesting question! How do you write software which is protected against a malicious operating system (mind -- not erroneous, but rather somebody detecting the software you're running and changing your vote). Maybe some sort of randomized cryptographic technique, in which, with high probability, the OS either runs your program correctly or causes it to crash. Luke However, we might have a few more rigged elections before we see any deliverables from Coyotos. On Thu, Feb 19, 2009 at 2:45 AM, Ketil Malde ke...@malde.org wrote: Rick R rick.richard...@gmail.com writes: I'm sure Premier Election Solutions (formerly Diebold) can provide us with an online voting solution. You know, while the recent voting scandals have been milked for all they're worth by the open source community, FP has been very quiet about it. Isn't this an application where correctness matters? How about a proof that the software never loses (or injects) votes, for instance? -k -- If I haven't seen further, it is by standing in the footprints of giants -- We can't solve problems by using the same kind of thinking we used when we created them. - A. Einstein ___ 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] How to create an online poll
2009/2/19 Luke Palmer lrpal...@gmail.com: 2009/2/19 Rick R rick.richard...@gmail.com I think the capabilities community including E and Coyotos/BitC have extensively addressed this topic. Coyotos is taking the correct approach for trusted voting platform. Since, even if your software is trustworthy, it can't be trusted if the OS on which it runs is suspect. Woah, that's a pretty interesting question! How do you write software which is protected against a malicious operating system (mind -- not erroneous, but rather somebody detecting the software you're running and changing your vote). Maybe some sort of randomized cryptographic technique, in which, with high probability, the OS either runs your program correctly or causes it to crash. Luke Free associating: Static Typing for a Faulty Lambda Calculus http://lambda-the-ultimate.org/node/2108 A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. These faults do not cause permanent damage, but may result in incorrect program execution by altering signal transfers or stored valuesThis paper defines the first formal, type-theoretic framework for studying reliable computation in the presence of transient faults. More specifically, it defines lambda-zap, a lambda calculus that exhibits intermittent data faults. In order to detect and recover from these faults, lambda-zap programs replicate intermediate computations and use majority voting, thereby modeling software-based fault tolerance techniques studied extensively, but informally. To ensure that programs maintain the proper invariants and use lambda-zap primitives correctly, the paper defines a type system for the language. This type system guarantees that well-typed programs can tolerate any single data fault. To demonstrate that lambda-zap can serve as an idealized typed intermediate language, we define a type-preserving translation from a standard simply-typed lambda calculus into lambda-zap. -- gwern ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to create an online poll
2009/2/19 Luke Palmer lrpal...@gmail.com 2009/2/19 Rick R rick.richard...@gmail.com I think the capabilities community including E and Coyotos/BitC have extensively addressed this topic. Coyotos is taking the correct approach for trusted voting platform. Since, even if your software is trustworthy, it can't be trusted if the OS on which it runs is suspect. Woah, that's a pretty interesting question! How do you write software which is protected against a malicious operating system (mind -- not erroneous, but rather somebody detecting the software you're running and changing your vote). Maybe some sort of randomized cryptographic technique, in which, with high probability, the OS either runs your program correctly or causes it to crash. It gets worse. Even if you write your OS in Haskell, how do you know your compiler hasn't been compromised? Or the hardware? The solution necessarily involves a social component, e.g. Haskell, with the development practices of OpenBSD (continuous re-auditing of everything including tools, complete openness, etc.) IOW, it'll never happen, but it might end up better than paper ballots. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Hoogle and Network.Socket
Hi http://haskell.org/hoogle/?q=socket+%2Bnetwork By default it searches the libraries supplied with Windows apart from Network (for various technical reasons). If you add +network it will then search the network library. What libraries should Hoogle search by default? What flags should be available to control which ones are searched? I have no idea, if you do then say what you think and why! Thanks Neil On Thu, Feb 19, 2009 at 2:50 AM, Thomas DuBuisson thomas.dubuis...@gmail.com wrote: I recall that Niel made sure hoogle doesn't search through non-portable libraries (a shame), but I thought Network.Socket could be used on Windows and yet Hoogle does not give any results for 'socket' or any other functions within Network.Socket. First, am I mistaken and Network.Socket is POSIX only? I could swear it wasn't. Secondly - is there any chance of lifting the non-portable libraries ban, Niel? From the stand point of an application developer it might not sound good, but even in Haskell some software is system level and bound to be single platform (case and point: XCB, xmonad, hsXenCtrl). Judging by the amount of research in systems level functional programming I wouldn't be surprised to see this collection grow and making functions hard to find isn't productive. Thomas ___ 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] Hoogle and Network.Socket
Niel, Outside of flags to enable display of modules specific to each major platform (+windows, +posix, +osx) I see two options. This all depends on hoogle having some sort of list of modules for each platform, which I believe would be the main problem. 1) Show all the functions (when the number is low), but place platform specific functions under separate headers: Windows, Linux/BSD/POSIX, OS X, etc. This way the users can remain as ignorant as I was and still find their data. 2) Detect the OS (when possible - perhaps difficult for the web/JS interface) and display the functions specific to the platform requesting the search. This has a small issue if you are searching on one platform and programming on/for another platform. But the flags could still be used. Thomas On Thu, Feb 19, 2009 at 9:11 AM, Neil Mitchell ndmitch...@gmail.com wrote: Hi http://haskell.org/hoogle/?q=socket+%2Bnetwork By default it searches the libraries supplied with Windows apart from Network (for various technical reasons). If you add +network it will then search the network library. What libraries should Hoogle search by default? What flags should be available to control which ones are searched? I have no idea, if you do then say what you think and why! Thanks Neil On Thu, Feb 19, 2009 at 2:50 AM, Thomas DuBuisson thomas.dubuis...@gmail.com wrote: I recall that Niel made sure hoogle doesn't search through non-portable libraries (a shame), but I thought Network.Socket could be used on Windows and yet Hoogle does not give any results for 'socket' or any other functions within Network.Socket. First, am I mistaken and Network.Socket is POSIX only? I could swear it wasn't. Secondly - is there any chance of lifting the non-portable libraries ban, Niel? From the stand point of an application developer it might not sound good, but even in Haskell some software is system level and bound to be single platform (case and point: XCB, xmonad, hsXenCtrl). Judging by the amount of research in systems level functional programming I wouldn't be surprised to see this collection grow and making functions hard to find isn't productive. Thomas ___ 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] Hoogle and Network.Socket
On Wed, Feb 18, 2009 at 6:50 PM, Thomas DuBuisson thomas.dubuis...@gmail.com wrote: I recall that Niel made sure hoogle doesn't search through non-portable libraries (a shame), but I thought Network.Socket could be used on Windows and yet Hoogle does not give any results for 'socket' or any other functions within Network.Socket. I can't suggest why the network package isn't being indexed by Hoogle, but it does indeed work on Windows and is not, as erroneously stated by another respondent, POSIX-only. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A typeclass for Data.Map etc?
Maybe this is of interest: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/gmap The edison api is much more stable. The gmap api was already in place when I started working on it but I would prefer to at some point make it a superset of the edison api. No sense in having more than one map interface lying around. Jamie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Hoogle and Network.Socket
2009/2/19 Bryan O'Sullivan b...@serpentine.com: On Wed, Feb 18, 2009 at 6:50 PM, Thomas DuBuisson thomas.dubuis...@gmail.com wrote: I recall that Niel made sure hoogle doesn't search through non-portable libraries (a shame), but I thought Network.Socket could be used on Windows and yet Hoogle does not give any results for 'socket' or any other functions within Network.Socket. I can't suggest why the network package isn't being indexed by Hoogle, but it does indeed work on Windows and is not, as erroneously stated by another respondent, POSIX-only. If you say so, but.. Unix domain sockets? sendFd? I can't claim *none* of it works on windows, but those functions must at best be undefined on windows - right? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] forall ST monad
Jonathan Cast-2 wrote: Taking the `let open' syntax from `First-class Modules for Haskell' [1], we can say let open runST' = runST in let ref = runST' $ newSTRef 0 !() = runST' $ writeSTRef ref 1 !() = runST' $ writeSTRef ref 2 in runST' $ readSTRef ref This type-checks because the let open gives us the *same* skolemized constant for s everywhere in the sequel. One answer, of course, is to lift the skolem type-constant into a kind of IO-like type-monad. Sort of like getLine :: IO String, which is still constant in a way, since the program doesn't vary. You'd then want kind-level functions like returnK :: * - M * and the rest. It would be interesting to see this made explicit in System F. -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22106898.html 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
Re: [Haskell-cafe] Paper draft: Denotational design with type class morphisms
Hi, Thanks for this very interesting and inspiring paper. I'm certainly going to try some other data types, and see what kind of implementations you get when using the TCM property. I was wondering if any of this could be automated, given the semantic function? If not in Haskell, then could this be a nice basis for a new language? If something still needs to be cut, I'd consider much or even all of chapter 8. I found the tone and style unfitting for the rest of the paper, as it deals with the (imho) ugliness of bottom and strictness issues, instead of the beautiful relations found in the rest of the paper. greetings, Sjoerd Visscher On Feb 19, 2009, at 4:21 AM, Conal Elliott wrote: I have a draft paper some of you might enjoy, called Denotational design with type class morphisms. Abstract: Type classes provide a mechanism for varied implementations of standard interfaces. Many of these interfaces are founded in mathematical tradition and so have regularity not only of *types* but also of *properties* (laws) that must hold. Types and properties give strong guidance to the library implementor, while leaving freedom as well. Some of the remaining freedom is in *how* the implementation works, and some is in *what* it accomplishes. To give additional guidance to the *what*, without impinging on the *how*, this paper proposes a principle of *type class morphisms* (TCMs), which further refines the compositional style of denotational semantics. The TCM idea is simply that *the instance's meaning is the meaning's instance*. This principle determines the meaning of each type class instance, and hence defines correctness of implementation. In some cases, it also provides a systematic guide to implementation, and in some cases, valuable design feedback. The paper is illustrated with several examples of type, meanings, and morphisms. You'll find the paper at http://conal.net/papers/type-class- morphisms/ . I'd sure appreciate feedback on it, especially if in time for the *March 2* ICFP deadline. Pointers to related work would be particularly appreciated, as well as what's unclear and what could be cut. This draft is an entire page over the limit, so I'll have to do some trimming before submitting. Enjoy, and thanks! - Conal ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Sjoerd Visscher sjo...@w3future.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: pqueue-mtl, stateful-mtl
So, why not use this definition? Is there something special about ST
you are trying to preserve?
-- minimal complete definition:
-- Ref, newRef, and either modifyRef or both readRef and writeRef.
class Monad m = MonadRef m where
type Ref m :: * - *
newRef :: a - m (Ref m a)
readRef :: Ref m a - m a
writeRef :: Ref m a - a - m ()
modifyRef :: Ref m a - (a - a) - m a -- returns old value
readRef r = modifyRef r id
writeRef r a = modifyRef r (const a) return ()
modifyRef r f = do
a - readRef r
writeRef r (f a)
return a
instance MonadRef (ST s) where
type Ref (ST s) = STRef s
newRef = newSTRef
readRef = readSTRef
writeRef = writeSTRef
instance MonadRef IO where
type Ref IO = IORef
newRef = newIORef
readRef = readIORef
writeRef = writeIORef
instance MonadRef STM where
type Ref STM = TVar
newRef = newTVar
readRef = readTVar
writeRef = writeTVar
Then you get to lift all of the above into a monad transformer stack, MTL-style:
instance MonadRef m = MonadRef (StateT s m) where
type Ref (StateT s m) = Ref m
newRef = lift . newRef
readRef = lift . readRef
writeRef r = lift . writeRef r
and so on, and the mention of the state thread type in your code is
just gone, hidden inside Ref m. It's still there in the type of the
monad; you can't avoid that:
newtype MyMonad s a = MyMonad { runMyMonad :: StateT Int (ST s) a }
deriving (Monad, MonadState, MonadRef)
But code that relies on MonadRef runs just as happily in STM, or IO,
as it does in ST.
-- ryan
2009/2/19 Louis Wasserman wasserman.lo...@gmail.com:
It does. In the most recent version, the full class declaration runs
class MonadST m where
type StateThread m
liftST :: ST (StateThread m) a - m a
and the StateThread propagates accordingly.
Louis Wasserman
wasserman.lo...@gmail.com
On Thu, Feb 19, 2009 at 2:10 AM, Sittampalam, Ganesh
ganesh.sittampa...@credit-suisse.com wrote:
Henning Thielemann wrote:
On Mon, 16 Feb 2009, Louis Wasserman wrote:
Overnight I had the following thought, which I think could work
rather well. The most basic implementation of the idea is as
follows:
class MonadST s m | m - s where
liftST :: ST s a - m a
instance MonadST s (ST s) where ...
instance MonadST s m = MonadST ...
Like MonadIO, isn't it?
I think it should be, except that you need to track 's' somewhere.
Ganesh
==
Please access the attached hyperlink for an important electronic
communications disclaimer:
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==
___
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] ANNOUNCE: pqueue-mtl, stateful-mtl
Oh, sweet beans. I hadn't planned to incorporate mutable references -- my
code uses them highly infrequently -- but I suppose that since mutable
references are really equivalent to single-threadedness where referential
transparency is concerned, that could be pulled off -- I would still want a
StateThread associated type, but that'd just be RealWorld for IO and STM, I
guess.
Louis Wasserman
wasserman.lo...@gmail.com
On Thu, Feb 19, 2009 at 2:40 PM, Ryan Ingram ryani.s...@gmail.com wrote:
So, why not use this definition? Is there something special about ST
you are trying to preserve?
-- minimal complete definition:
-- Ref, newRef, and either modifyRef or both readRef and writeRef.
class Monad m = MonadRef m where
type Ref m :: * - *
newRef :: a - m (Ref m a)
readRef :: Ref m a - m a
writeRef :: Ref m a - a - m ()
modifyRef :: Ref m a - (a - a) - m a -- returns old value
readRef r = modifyRef r id
writeRef r a = modifyRef r (const a) return ()
modifyRef r f = do
a - readRef r
writeRef r (f a)
return a
instance MonadRef (ST s) where
type Ref (ST s) = STRef s
newRef = newSTRef
readRef = readSTRef
writeRef = writeSTRef
instance MonadRef IO where
type Ref IO = IORef
newRef = newIORef
readRef = readIORef
writeRef = writeIORef
instance MonadRef STM where
type Ref STM = TVar
newRef = newTVar
readRef = readTVar
writeRef = writeTVar
Then you get to lift all of the above into a monad transformer stack,
MTL-style:
instance MonadRef m = MonadRef (StateT s m) where
type Ref (StateT s m) = Ref m
newRef = lift . newRef
readRef = lift . readRef
writeRef r = lift . writeRef r
and so on, and the mention of the state thread type in your code is
just gone, hidden inside Ref m. It's still there in the type of the
monad; you can't avoid that:
newtype MyMonad s a = MyMonad { runMyMonad :: StateT Int (ST s) a }
deriving (Monad, MonadState, MonadRef)
But code that relies on MonadRef runs just as happily in STM, or IO,
as it does in ST.
-- ryan
2009/2/19 Louis Wasserman wasserman.lo...@gmail.com:
It does. In the most recent version, the full class declaration runs
class MonadST m where
type StateThread m
liftST :: ST (StateThread m) a - m a
and the StateThread propagates accordingly.
Louis Wasserman
wasserman.lo...@gmail.com
On Thu, Feb 19, 2009 at 2:10 AM, Sittampalam, Ganesh
ganesh.sittampa...@credit-suisse.com wrote:
Henning Thielemann wrote:
On Mon, 16 Feb 2009, Louis Wasserman wrote:
Overnight I had the following thought, which I think could work
rather well. The most basic implementation of the idea is as
follows:
class MonadST s m | m - s where
liftST :: ST s a - m a
instance MonadST s (ST s) where ...
instance MonadST s m = MonadST ...
Like MonadIO, isn't it?
I think it should be, except that you need to track 's' somewhere.
Ganesh
==
Please access the attached hyperlink for an important electronic
communications disclaimer:
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==
___
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] Haskell.org GSoC
Alberto G. Corona wrote:
Wouldn't it be better to achieve the goals you describe with a dependently
typed programming language?
But I wonder how a dependent typed language can express certain properties,
for example, the distributive property between the operation + and * in a
ring or simply the fact that show(read x)==x. As far as I understand, a
dependent type system can restrict the set of values for wich a function
apply, but it can not express complex relationships between operations.
In a dependently typed language, propositions can be encoded as types,
and a value of such a type is a proof that the theorem holds, so one
could imagine something like:
class ReadShow a where
show :: a - String
read :: String - Maybe a
law :: forall (x : String), read (show x) = x
instance ReadShow Int where
show x = construct string representation of x
read x = try to parse x
law = proof of property
Note that the forall quantifies over values in a type, so this is indeed
dependently typed.
With the new support for type classes in Coq 8.2, you can write stuff
like that.
Require Import List.
Class Monoid (A : Type) := {
empty : A;
concat : A - A - A;
left_ident : forall (a : A), a = concat empty a;
right_ident : forall (a : A), a = concat a empty;
assoc : forall (a b c : A), concat (concat a b) c = concat a (concat b c)
}.
Instance list_monoid : Monoid (list A) := {
empty := nil;
concat := fun x y = x ++ y;
left_ident := fun a = refl_equal (nil ++ a);
right_ident := @app_nil_end A;
assoc := @app_ass A
}.
The class declaration lists the laws, the instance declaration has to
give the proofs. Since these facts about lists are provided by the
standard library, this is easy in this example. Of course, one can use
the proof mode to prove the laws with a proof script. For example for
the Monoid instance for Maybe we have in Haskell.
Instance option_monoid_lifted (A : Type) (MA : Monoid A) : Monoid (option A) :=
{
empty := None;
append := fun x y = match (x, y) with
| (None, b) = b
| (a, None) = a
| (Some a, Some b) = Some (append a b)
end
}.
Proof.
auto.
destruct a; auto.
destruct a; destruct b; destruct c; auto. f_equal. apply assoc.
Defined.
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] equational reasoning
* Wouter Swierstra w...@cs.nott.ac.uk [2009-02-19 11:58:38+0100] There are several problems with this approach. For example, I can show: const 0 (head []) = 0 But if I pretend that I don't know that Haskell is lazy: const 0 (head []) = const 0 (error ) = error ... Where does the last equality come from? Which would allow me to substitute each occurrence of 0 with error - which probably isn't a good idea. So to do proper equational reasoning in a lazy language you need to be extremely careful with evaluation order. Evaluation order matters for operational semantics, not for axiomatic. And even in operational semantics Church–Rosser theorem should prevent getting different results (e.g. 0 and error) for different evaluation orders. Please correct me if I'm wrong. -- Roman I. Cheplyaka :: http://ro-che.info/ Don't let school get in the way of your education. - Mark Twain ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] equational reasoning
On Thu, 2009-02-19 at 23:06 +0200, Roman Cheplyaka wrote: * Wouter Swierstra w...@cs.nott.ac.uk [2009-02-19 11:58:38+0100] There are several problems with this approach. For example, I can show: const 0 (head []) = 0 But if I pretend that I don't know that Haskell is lazy: const 0 (head []) = const 0 (error ) = error ... Where does the last equality come from? Pretending Haskell is strict. It would be an axiom of Strict Haskell, were someone to write such a thing, that forall a b (x :: String) (f :: a - b). f (error x) = error x :: b With the side condition that f is a lambda. Then, we would know that, if f is a lambda of arity 1 (or a constant defined to be such a lambda), that (f a), where a is a value (such as 0), is equal to some lambda; so by congruence and the equation above, we get (f a (error x) = error x) for all values a. Which doesn't obviate the point that any proof-checker for *Haskell* worth its salt would reject any alleged proof of (const 0 (error x) = error x). jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] equational reasoning
Roman Cheplyaka schrieb: Evaluation order matters for operational semantics, not for axiomatic. And even in operational semantics Church–Rosser theorem should prevent getting different results (e.g. 0 and error) for different evaluation orders. Let's consider omega = omega const omega 42 which is evaluated to 42 in Haskell, but is nonterminating in an strict language. I would expect every kind of semantics to account for this difference. Regarding Church-Rosser. First, it says that if you can reduce term P into both P and Q, then there exists a term R so that both P and Q can be reduced to it. That doesn't mean that your particular evaluation order will ever do this reduction. Instead, it may keep doing other reductions forever. Second, who says Church-Rosser holds for Haskell? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Paper draft: Denotational design with type class morphisms
May be I am reading it wrong Shouldn't the second instance in The instance's meaning is the meaning's instance be plural as meaning's instances rather than meaning's instance? I am reading it similar to the you are who you know saying. It seems to say that the meaning of your data types (The instance's meaning) is defined by the instances of known classes (with predefined meaning, defined by it properties, as in functor, monoid..) that is defined for your type. Daryoush 2009/2/19 Sjoerd Visscher sjo...@w3future.com Hi, Thanks for this very interesting and inspiring paper. I'm certainly going to try some other data types, and see what kind of implementations you get when using the TCM property. I was wondering if any of this could be automated, given the semantic function? If not in Haskell, then could this be a nice basis for a new language? If something still needs to be cut, I'd consider much or even all of chapter 8. I found the tone and style unfitting for the rest of the paper, as it deals with the (imho) ugliness of bottom and strictness issues, instead of the beautiful relations found in the rest of the paper. greetings, Sjoerd Visscher On Feb 19, 2009, at 4:21 AM, Conal Elliott wrote: I have a draft paper some of you might enjoy, called Denotational design with type class morphisms. Abstract: Type classes provide a mechanism for varied implementations of standard interfaces. Many of these interfaces are founded in mathematical tradition and so have regularity not only of *types* but also of *properties* (laws) that must hold. Types and properties give strong guidance to the library implementor, while leaving freedom as well. Some of the remaining freedom is in *how* the implementation works, and some is in *what* it accomplishes. To give additional guidance to the *what*, without impinging on the *how*, this paper proposes a principle of *type class morphisms* (TCMs), which further refines the compositional style of denotational semantics. The TCM idea is simply that *the instance's meaning is the meaning's instance*. This principle determines the meaning of each type class instance, and hence defines correctness of implementation. In some cases, it also provides a systematic guide to implementation, and in some cases, valuable design feedback. The paper is illustrated with several examples of type, meanings, and morphisms. You'll find the paper at http://conal.net/papers/type-class-morphisms/ . I'd sure appreciate feedback on it, especially if in time for the *March 2* ICFP deadline. Pointers to related work would be particularly appreciated, as well as what's unclear and what could be cut. This draft is an entire page over the limit, so I'll have to do some trimming before submitting. Enjoy, and thanks! - Conal ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Sjoerd Visscher sjo...@w3future.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
Re: [Haskell-cafe] A typeclass for Data.Map etc?
On Thu, Feb 19, 2009 at 01:51:44PM +0300, Eugene Kirpichov wrote: Is there a typeclass for mappings with a Data.Map-like interface, with stuff like: empty, insert, insertWithKey, unionWith etc. ? And, probably, a similar typeclass for mutable mappings like Data.Hashtable. Here is one I wrote a while ago, feel free to use it any way you want, I bequeath the fille to the public domain. http://repetae.net/repos/jhc/Util/SetLike.hs John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: pqueue-mtl, stateful-mtl
Ryan, I didn't get your question after the first read, so here's an actual
answer to it --
What I want to preserve about ST is the existence of a guaranteed safe
runST, really. I tend to do algorithms and data structures development,
which almost never requires use of IO, or references of any kind -- usually
STArrays for intermediate computations are what I'm actually interested in,
and the actual outputs of my code are generally not monadic at all.
But I see how it would be useful in general. I'll add it in.
Louis Wasserman
wasserman.lo...@gmail.com
On Thu, Feb 19, 2009 at 2:51 PM, Louis Wasserman
wasserman.lo...@gmail.comwrote:
Oh, sweet beans. I hadn't planned to incorporate mutable references -- my
code uses them highly infrequently -- but I suppose that since mutable
references are really equivalent to single-threadedness where referential
transparency is concerned, that could be pulled off -- I would still want a
StateThread associated type, but that'd just be RealWorld for IO and STM, I
guess.
Louis Wasserman
wasserman.lo...@gmail.com
On Thu, Feb 19, 2009 at 2:40 PM, Ryan Ingram ryani.s...@gmail.com wrote:
So, why not use this definition? Is there something special about ST
you are trying to preserve?
-- minimal complete definition:
-- Ref, newRef, and either modifyRef or both readRef and writeRef.
class Monad m = MonadRef m where
type Ref m :: * - *
newRef :: a - m (Ref m a)
readRef :: Ref m a - m a
writeRef :: Ref m a - a - m ()
modifyRef :: Ref m a - (a - a) - m a -- returns old value
readRef r = modifyRef r id
writeRef r a = modifyRef r (const a) return ()
modifyRef r f = do
a - readRef r
writeRef r (f a)
return a
instance MonadRef (ST s) where
type Ref (ST s) = STRef s
newRef = newSTRef
readRef = readSTRef
writeRef = writeSTRef
instance MonadRef IO where
type Ref IO = IORef
newRef = newIORef
readRef = readIORef
writeRef = writeIORef
instance MonadRef STM where
type Ref STM = TVar
newRef = newTVar
readRef = readTVar
writeRef = writeTVar
Then you get to lift all of the above into a monad transformer stack,
MTL-style:
instance MonadRef m = MonadRef (StateT s m) where
type Ref (StateT s m) = Ref m
newRef = lift . newRef
readRef = lift . readRef
writeRef r = lift . writeRef r
and so on, and the mention of the state thread type in your code is
just gone, hidden inside Ref m. It's still there in the type of the
monad; you can't avoid that:
newtype MyMonad s a = MyMonad { runMyMonad :: StateT Int (ST s) a }
deriving (Monad, MonadState, MonadRef)
But code that relies on MonadRef runs just as happily in STM, or IO,
as it does in ST.
-- ryan
2009/2/19 Louis Wasserman wasserman.lo...@gmail.com:
It does. In the most recent version, the full class declaration runs
class MonadST m where
type StateThread m
liftST :: ST (StateThread m) a - m a
and the StateThread propagates accordingly.
Louis Wasserman
wasserman.lo...@gmail.com
On Thu, Feb 19, 2009 at 2:10 AM, Sittampalam, Ganesh
ganesh.sittampa...@credit-suisse.com wrote:
Henning Thielemann wrote:
On Mon, 16 Feb 2009, Louis Wasserman wrote:
Overnight I had the following thought, which I think could work
rather well. The most basic implementation of the idea is as
follows:
class MonadST s m | m - s where
liftST :: ST s a - m a
instance MonadST s (ST s) where ...
instance MonadST s m = MonadST ...
Like MonadIO, isn't it?
I think it should be, except that you need to track 's' somewhere.
Ganesh
==
Please access the attached hyperlink for an important electronic
communications disclaimer:
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==
___
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] Re: Overloading functions based on arguments?
On 20 Feb 2009, at 3:24 am, John A. De Goes wrote: It is precisely this abuse of notation which makes, for instance, statistics textbooks impossible to read (without already knowing the material). Hmmm, I don't find statistics books difficult to read. I'm interested in a technique called Correspondence Analysis. I recently bought a book about it. The author comes from the UK, but was trained in CA at its home in France. And the book is very nearly unreadable, thanks in part to some of the strangest overloading I've seen. I don't have it handy, but things like f(i) and f(j) having different types is just the start. (No, this is not dependent typing. Which type the result is depends on the *name* of the argument, not its value!) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] package for algebraic structures
Wolfgang Jeltsch schrieb: Am Donnerstag, 19. Februar 2009 00:17 schrieben Sie: Do you mean this one: http://haskell.org/haskellwiki/Numeric_Prelude? There is currently no code for this, is there? http://hackage.haskell.org/cgi-bin/hackage-scripts/package/numeric-prelude http://darcs.haskell.org/numericprelude/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] package for algebraic structures
On Thu, 19 Feb 2009, Wolfgang Jeltsch wrote: Am Donnerstag, 19. Februar 2009 00:17 schrieben Sie: Do you mean this one: http://haskell.org/haskellwiki/Numeric_Prelude? There is currently no code for this, is there? ??? http://hackage.haskell.org/cgi-bin/hackage-scripts/package/numeric-prelude http://darcs.haskell.org/numericprelude/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: garbage collector woes
waterson: On Feb 17, 2009, at 12:22 PM, Chris Waterson wrote: I'm at wits end with respect to GHC's garbage collector and would very much appreciate a code review of my MySQL driver for HDBC, which is here: http://www.maubi.net/~waterson/REPO/HDBC-mysql/Database/HDBC/MySQL/Connection.hsc In particular, the problem that I'm having is that my statements (really, just iterators over a SQL query result set) are getting garbage collected prematurely. So (*blush*), my woes turned out to be my misunderstanding of the MySQL C API, which I have now come to terms with. I apologize for the noise here. Is the solution written up somewhere so we can point to that next time? :) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: garbage collector woes
On Feb 19, 2009, at 3:41 PM, Don Stewart wrote: Is the solution written up somewhere so we can point to that next time? :) Well, the applicability to the community at large is probably minimal, but my misadventure follows... The MySQL C API has statements that are associated with a database connection. You connect to the database, and issue statements to query and manipulate it. The statement encapsulates, basically, the state of iteration through a result set. It turns out that a connection allows only one statement to be active at a time, and that closing any statement associated with a connection appears to close all other statements associated with that connection, too. I wrap the MySQL statement in a ForeignPtr whose finalizer closes the statement. Which, as it turns out, would close the *next* statement that I'd created on the connection as a side effect. I was incorrectly interpreting I tried to mitigate this surprising effect by 1) making sure that a statement gets finalized as soon as its result set is exhausted, and 2) adding some warnings to the driver docs about this wonderful feature. chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A typeclass for Data.Map etc?
On Thu, Feb 19, 2009 at 10:18 AM, Jamie Brandon jamii...@googlemail.com wrote: Maybe this is of interest: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/gmap The edison api is much more stable. The gmap api was already in place when I started working on it but I would prefer to at some point make it a superset of the edison api. No sense in having more than one map interface lying around. Jamie What would really be nice is a general interface to a lot of different types of containers that was both standardized by the community AND used as the basis for lots of different libraries. For instance, the new split package is a well-crafted library for dealing with splitting lists, but it only works on lists. The exact same logic that's already there could be used for splitting ByteStrings, Lazy ByteStrings, Data.Sequences, some of the sequence types in Edison, fixed-length vectors, etc., but currently, the way the package is made forces you to use only Haskell's lazy lists. Now if we look at the zlib package, this package decompresses data into the lazy ByteString format. So you can't directly split data that comes out of zlib - you have to convert it to String and then back again, which is annoying and also imposes a performance cost. If we could figure out a way to have a general interface to sequence-like or map-like or set-like objects, we could make our libraries a lot more general and also more useful in combination with each other. Alex ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell.org GSoC
On Feb 18, 2009, at 4:43 AM, Max Bolingbroke wrote: 2009/2/18 Sterling Clover s.clo...@gmail.com: The punchline: With GHC plugins, it should be possible, and reasonable, to add a proper unit system for Haskell. Alas, GHC plugins cannot change the type system - only meddle with the compilation strategy or analyse the code and suchlike. I'm working with Simon Peyton Jones to get plugins integrated fully into GHC (parts of it have been commited already) but we're both busy and so progress is slow. I don't think any GSoC projects should take a dependency on it being both integrated into GHC and stable in time for the summer. Thanks for the update on plugins! I look forward to trying them out from the GHC mainline at some point. I don't think that units as I envision them would need to mess with the type system directly, but could be implemented simply as a static analysis step, such as you describe. Units really do something quite different from standard types, and unit-correctness seems orthogonal to type correctness. A simple plugin would, e.g., allow unit annotations as distinct from type annotations (although, with an appropriate preprocessor step, they could, with cleverness, be written jointly), and simply track unit usage throughout the code to ensure correctness. It would, I assume, only need to operate on things which belonged to the Num typeclass to begin with, and assume that all unannotated numbers were scalars. Even lacking any sophisticated features, I would find this very useful, and certainly easier to envision than a more general extension to the type system that made unit tracking feasible, but yet, somehow, didn't veer fully into either simulated or actual dependent typing. So I guess I'll just keep this idea in mind and pitch it for next year's GSoC. :-) Cheers, Sterl. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A typeclass for Data.Map etc?
Eugene Kirpichov wrote: Looks like such a thing would be useful; as for now, I see at least two applications: Data.Map and Data.Trie (bytestring-trie) - it's a pity that they have rather similar interfaces, but the latter lacks many methods and some are named in a different way. Are there any particular functions you're missing? Most of the not-as-generic variants that Data.Map has are in Data.Trie.Convenience, so as to keep Data.Trie lean. There are a few notable exceptions which are on the todo list (the dual-use insertlookup and updatelookup in particular). In general I tried to keep all of the specific variants and any particularly helpful not-as-generic variants. Some of the not-as-generic variants didn't seem worth the time to wrapper given that we already have more generic variants (which Data.Map lacks) in Data.Trie and Data.Trie.Internal. Also, Data.Map has some inconsistensies, too: for instance, it has an insertWith' but lacks a unionWith'. One typeclass for all would eliminate these inconsistencies. Some of the name changes were to overcome these inconsistencies (e.g. `findWithDefault` - `lookupWithDefault`, since we have `lookup` and not `find`). As for the original question, the gmap stuff and the Edison libraries provide some classes for this sort of thing. Last I checked the community hadn't really settled on what all should be included in such an interface (e.g. do you only have insert, delete, etc; or do you also require the very generic *By functions like Data.Trie? The former may not be helpful enough, and the latter may be too much of a burden on the instances.) If (a) the community can agree on a typeclass for maps, which (b) allows instances to have a fixed type for keys (like Data.Trie and Data.IntMap have), (c) doesn't require ghc-only extensions like associated types, and (d) doesn't have onerous package dependencies, then I'd be more than happy to offer an instance. The #c requirement is basically a subset of #a I'd assume. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Overloading functions based on arguments?
On Feb 19, 2009, at 9:09 AM, John A. De Goes wrote: Let's try a little test: 1. If the parameter is a tree, what do you think flatten would do? I would imagine that it would be join on trees -- i.e. take a tree of trees and turn it into a tree. But perhaps it would be arbitrarily deep. Or perhaps it would turn a tree into a list, but I would of course prefer toList for that. 2. If the parameter is a list, what do you think flatten would do? Since a list is already flat, it couldn't possibly turn it into a list -- but again, it could perhaps be join or it could be deepJoin or maybe if it was a list of numbers that represented a signal, it would smooth out peaks beyond standard deviation, but maybe it would do that treating the numbers as a time series or perhaps it would do that treating the numbers as coefficient to a series of trigonometric functions. 3. If the parameter is a Style (possible a composite Style consisting of other styles), what do you think flatten would do? If the style included colors, perhaps it would mute them? Or, maybe, it would mean, as you intended, join. And if a style may consist of other styles, then isn't it, properly speaking, a variant of a tree to begin with? 4. If the parameter is a Bezier curve, what do you think flatten would do? One would imagine, produce a straight line. But would this line be between the original endpoints, or would it be a projection onto the horizontal axis? My guess is that we would come to the same conclusions for (1) - (4). The name flatten is a perfectly good name for all of these operations, because the domains are distinct, and because using that name suggests the correct meaning to you. (Note use of the word suggests -- like an analogy or parable, you're likely not going to know exactly what the function does just by reading its name, but you'll be in the ballpark and have an intuition about it, which is extremely valuable.) In three cases, depending on what you intended flatten to mean (I've been a bit provocative, but honestly I do have no idea), then the domains may not be distinct, because join is an operation that they do properly have in common. And no, the name doesn't suggest one clear meaning -- what does, generally, suggest a single clear meaning to me, is a good type signature, but since I could no longer query :t flatten in GHCI and get a single response, I would be, I'm afraid, somewhat at sea -- even more so if in some cases flatten was a typeclass operation, and in others not. Or, worse yet, if flatten was declared as a typeclass operation in one place, defined on lists in another, and in a third, lists were given an orphaned Flattenable instance. Cheers, Sterl. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Looking for pointfree version (Kim-Ee Yeoh) (02/12)
Kim-Ee Yeoh said: On the same note, does anyone have ideas for the following snippet? Tried the pointfree package but the output was useless. pointwise op (x0,y0) (x1,y1) = (x0 `op` x1, y0 `op` y1) First sorry for the delay in getting to this.. been behind on projects so had some days of mail piled up. Here is what I came up with, using one arrow operator, so you would have to import: Control.Arrow ((***)) at minimum to use this solution: pointfree :: forall t t1 c. (t - t1 - c) - (t, t1) - (t, t1) - (c, c) pointfree op = curry $ (\(a,b) - a `op` b) *** (\(a,b) - a `op` b) examples of use, that were executed using: ghci -fglasgow-exts -farrows Control.Arrow *pointfree (*) (3,5) (12,12) (15,144) * pointfree (++) (This ,That) (Old, Man) (This That,Old Man) Hope that helps. -- gene == website: http://haskblog.cloud.prohosting.com == If Helen Keller is alone in a forest and falls, does she make a sound? Receive Notifications of Incoming Messages Easily monitor multiple email accounts access them with a click. Visit http://www.inbox.com/notifier and check it out! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Hoogle and Network.Socket
On 2009 Feb 19, at 13:19, Svein Ove Aas wrote: If you say so, but.. Unix domain sockets? sendFd? I can't speak to sendFd, but BITD OS/2 had AF_LOCAL (the portable version of AF_UNIX; same API) sockets. There's no particular reason aside from unwillingness that Windows wouldn't support it. -- 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
Re: [Haskell-cafe] equational reasoning
* Tillmann Rendel ren...@cs.au.dk [2009-02-19 22:43:24+0100] Roman Cheplyaka schrieb: Evaluation order matters for operational semantics, not for axiomatic. And even in operational semantics Church–Rosser theorem should prevent getting different results (e.g. 0 and error) for different evaluation orders. Let's consider omega = omega const omega 42 I guess you meant const 42 omega. which is evaluated to 42 in Haskell, but is nonterminating in an strict language. I would expect every kind of semantics to account for this difference. It's slightly different. I understand that error .. and omega have the same denotation, but the difference is that omega does not have normal form and error .. is in normal form. So non-termination of const 42 omega in a strict language is not surprising (we know that strict evaluation does not always find normal form, even if it exists), but const 42 (error ...) = error ... means that different evaluation orders give us different normal forms, which is denied by Church-Rosser. Second, who says Church-Rosser holds for Haskell? Now I see that exceptions magic can break it. Is this what you mean? -- Roman I. Cheplyaka :: http://ro-che.info/ Don't let school get in the way of your education. - Mark Twain ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
