Re: [Haskell-cafe] Re: Chuch encoding of data structures in Haskell
Ivan Miljenovic wrote: On 28 May 2010 15:18, wren ng thornton wrote: Stefan Monnier wrote: churchedBool :: t -> t -> t Important detail: the precise type is "∀t. t → t → t". encodeBool x = \t e -> if x then t else e So the type of encodeBool should be: Bool → ∀t. t → t → t whereas Haskell will infer it to be ∀t. Bool → t → t → t Those are the same type. I can see a slight distinction between them, based upon when the quantification occurs (the former returns a function that work on all t, the latter will do that encoding for all t). The isomorphism in System F: in : (∀t. Bool → t → t → t) → (Bool → ∀t. t → t → t) in f = \b. /\t. f @t b out : (Bool → ∀t. t → t → t) → (∀t. Bool → t → t → t) out g = /\t. \b. g b @t If you're using the raw System F, then there's a slight difference ---as there always is between isomorphic things which are non-identical--- but that difference is not theoretically significant. If you're using a higher-level language like Haskell, then the conversions are done for you, so there's even less difference. The expression 1+1 is distinct from 2: it has a different representation in memory, it takes a different number of steps to normalize, etc. Sometimes these differences are important for engineering (e.g., dealing with space leaks), but they're rarely significant for theory. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
Lennart Augustsson wrote: So what would you consider a proof that there are no total Haskell functions of that type? Or, using Curry-Howard, a proof that the corresponding logical formula is unprovable in intuitionistic logic? It depends on what kind of proof I'm looking for. If I'm looking for an informal proof to convince myself, then I'd probably trust Djinn. If I'm trying to convince others, am deeply skeptical, or want to understand the reasoning behind the result, then I'd be looking for a more rigorous proof. In general, that rigorous proof would require metatheory (as you say)--- either my own, or understanding the metatheory behind some tool I'm using to develop the proof. For example, I'd only trust Djinn for a rigorous proof after fully understanding the algorithms it's using and the metatheory used to prove its correctness (and a code inspection, if I didn't trust the developers). If Djinn correctly implements the decision procedure that have been proven to be total (using meta theory), then I would regard Djinn saying no as a proof that there is no function of that type. So would I. However, that's adding prerequisites for trusting Djinn--- which was my original point: that Djinn says there isn't one is not sufficient justification for some folks, they'd also want justification for why we should believe Djinn actually does exhaust every possibility. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Wire GUI
I'm looking at a project which involves a GUI where you can insert components and wire up connections between them. Obviously the details of what the components are and what code gets executed for them is domain-specific, however the general idea of graphically wiring things together is quite generic. Has anybody already put together a Haskell library for doing this kind of thing? Blobs. (warning: some danger of bitrot) http://www.cs.york.ac.uk/fp/darcs/Blobs/ Regards, Malcolm ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
Dan Doel wrote: On Thursday 27 May 2010 1:49:36 pm wren ng thornton wrote: Sure, that's another option. But the failure of exhaustive search isn't a constructive/intuitionistic technique, so not everyone would accept the proof. Djinn is essentially an implementation of reasoning by parametricity, IIRC, so it comes down to the same first principles. How, exactly, is it non-constructive to encode the propositional calculus and its proofs as, say, types in intuitionistic type theory, write the algorithm djinn uses in the same (it was specially crafted to be provably terminating, after all), and prove the algorithm complete (again, hopefully in the type theory)? I realize this has not all been done, strictly speaking, but I see nowhere that it is necessarily non-constructive. All I'm saying is that a proof of (\forall x. ~ P x) does not constitute a proof of (~ \exist x. P x) for some intuitionists. The issue is one of the range of quantification and whether \forall truly exhausts every possibility. The BHK interpretation says the two propositions are the same, but others say the latter is a stronger claim. If you believe that Djinn truly does exhaust the search space, then it's fine to convert Djinn's proof of (\forall x. ~ P x) into a proof of (~ \exist x. P x). However, that just pushes the question back to why you feel justified in believing that Djinn truly exhausts the search space. I'm not saying you shouldn't believe in Djinn, I'm saying that belief in Djinn is not justification for a theorem unless you have justification for believing in Djinn. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma
On 05/27/10 17:42, Carlos Camarao wrote:
On Thu, May 27, 2010 at 5:43 PM, David Menendez wrote:
On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao
wrote:
Isaac Dupree:
Your proposal appears to allow /incoherent/ instance selection.
This means that an expression can be well-typed in one module, and
well-typed in another module, but have different semantics in the
two modules. For example (drawing from above discussion) :
module C where
class F a b where f :: a -> b
class O a where o :: a
module P where
import C
instance F Bool Bool where f = not
instance O Bool where o = True
k :: Bool
k = f o
module Q where
import C
instance F Int Bool where f = even
instance O Int where o = 0
k :: Bool
k = f o
module Main where
import P
import Q
-- (here, all four instances are in scope)
main = do { print P.k ; print Q.k }
-- should result, according to your proposal, in
-- False
-- True
-- , am I correct?
If qualified importation of k from both P and from Q was specified, we
would have two *distinct* terms, P.k and Q.k.
I think Isaac's point is that P.k and Q.k have the same definition (f
o). If they don't produce the same value, then referential
transparency is lost.
--
Dave Menendez
Re[3]: [Haskell-cafe] Re: Unicode vs. System.Directory
Hello Bulat, Friday, May 28, 2010, 9:24:02 AM, you wrote: >> I have finish all necessary GIO APIs at >> http://patch-tag.com/r/AndyStewart/gio-branch/home > but what is the license? heh, i've found COPYING file. but what you mean? if it's just about "one should share all improvements to the library he was made", it's fine for me. but strictly speaking, LGPL also means "you should allow user to replace himself GIO library with newer versions", it may be both hard for me and useless for users -- 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: Chuch encoding of data structures in Haskell
On 28 May 2010 15:18, wren ng thornton wrote: > Stefan Monnier wrote: >>> >>> churchedBool :: t -> t -> t >> >> Important detail: the precise type is "∀t. t → t → t". >> >>> encodeBool x = \t e -> if x then t else e >> >> So the type of encodeBool should be: >> >> Bool → ∀t. t → t → t >> >> whereas Haskell will infer it to be >> >> ∀t. Bool → t → t → t > > > Those are the same type. I can see a slight distinction between them, based upon when the quantification occurs (the former returns a function that work on all t, the latter will do that encoding for all t). For most purposes there is no difference, but IIUC the former will let you do hlist style stuff post-encoding whilst the latter doesn't. -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Re: Unicode vs. System.Directory
Hello Andy, Friday, May 28, 2010, 1:05:59 AM, you wrote: > Looks my file-manager: > http://farm5.static.flickr.com/4027/4584389024_782b1e09ee_o.png can you please share windows and linux executables and source code? > I have finish all necessary GIO APIs at > http://patch-tag.com/r/AndyStewart/gio-branch/home > I will try to merge those APIs to next release version of gtk2hs when i > have spare time. it seems that i can just merge these sources into my program for a while. but what is the license? believe it or not, but i have commercial project on the march -- 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: Math questions
On Thursday 27 May 2010 9:05:40 pm Ivan Miljenovic wrote: > On 28 May 2010 09:37, Richard O'Keefe wrote: > > On May 27, 2010, at 11:50 PM, Yitzchak Gale wrote: > >> agree100 = (==) `on` for [1..100] > > > > Search for "on" and "for" in the Haskell 98 Report and you > > will not find them. If you want to tell someone to use them, > > you ought to tell them where to find them. > > You mean like this? > > http://haskell.org/hoogle/?hoogle=on > http://haskell.org/hoogle/?hoogle=for for from Data.Traversable cannot be what was intended, because it would require the functions to have type: a -> F b for some Applicative F (which, moreover, should be providing the Eq instance you want to check with). This works for the identity functor (assuming the instance is declared), but the code is still not right, since the definition given doesn't lift the functions. Rather: for = flip map presumably. But this definition isn't in any of the standard libraries (at least visibly) to my knowledge. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Chuch encoding of data structures in Haskell
Stefan Monnier wrote: churchedBool :: t -> t -> t Important detail: the precise type is "∀t. t → t → t". encodeBool x = \t e -> if x then t else e So the type of encodeBool should be: Bool → ∀t. t → t → t whereas Haskell will infer it to be ∀t. Bool → t → t → t Those are the same type. which means that a given object can only be eliminated to one type. No, the t is universally quantified just fine. Perhaps you're thinking of the need for rank-2 polymorphism in functions which take Church-encoded arguments? -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Math questions
This is an effect with any language that offers a very high degree of abstraction. > >I think this is an example of the "Haskell effect" (more typically >seen on #haskell), which can be categorised as follows: > >1) Someone asks a (usually rather simple) question. > >2) People discuss this and provide several straightforward and relevant >answers. > >3) Out of curiosity (and probably a fair dose of masochism) others >then start to golf the solution into the most interesting approach >possible. > >4) The person that asked the question initially gets lost (but is >quite often awed at all the amazing stuff that's going on around them >zooming past at light speed). > >5) People suddenly remember that there was an initial question and >make an attempt to explain the more advanced solutions to the person >that asked the question in the first place. > >6) They smile and nod and pretend they understand whilst putting a >note onto their copious TODO list to someday sit down and try to work >out wtf was going on. > >7) ??? > >8) Profit!!! -- Regards, Casey ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Math questions
On 28 May 2010 14:52, Richard O'Keefe wrote:> Yes, that kind of thing. > Remember, this was a BEGINNER-type question. > If one is giving a *serious* answer, it has to be an answer a > beginner (who has almost certainly never heard of Traversable) > can make sense of, and if it uses functions that are pretty > much certain not to be in said beginner's text book, said > beginner has to be told quite clearly where to find them. I think this is an example of the "Haskell effect" (more typically seen on #haskell), which can be categorised as follows: 1) Someone asks a (usually rather simple) question. 2) People discuss this and provide several straightforward and relevant answers. 3) Out of curiosity (and probably a fair dose of masochism) others then start to golf the solution into the most interesting approach possible. 4) The person that asked the question initially gets lost (but is quite often awed at all the amazing stuff that's going on around them zooming past at light speed). 5) People suddenly remember that there was an initial question and make an attempt to explain the more advanced solutions to the person that asked the question in the first place. 6) They smile and nod and pretend they understand whilst putting a note onto their copious TODO list to someday sit down and try to work out wtf was going on. 7) ??? 8) Profit!!! -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Math questions
On May 28, 2010, at 1:05 PM, Ivan Miljenovic wrote: On 28 May 2010 09:37, Richard O'Keefe wrote: On May 27, 2010, at 11:50 PM, Yitzchak Gale wrote: agree100 = (==) `on` for [1..100] Search for "on" and "for" in the Haskell 98 Report and you will not find them. If you want to tell someone to use them, you ought to tell them where to find them. You mean like this? http://haskell.org/hoogle/?hoogle=on http://haskell.org/hoogle/?hoogle=for Yes, that kind of thing. Remember, this was a BEGINNER-type question. If one is giving a *serious* answer, it has to be an answer a beginner (who has almost certainly never heard of Traversable) can make sense of, and if it uses functions that are pretty much certain not to be in said beginner's text book, said beginner has to be told quite clearly where to find them. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Chuch encoding of data structures in Haskell
2010/5/27 Günther Schmidt > Hello C, > > thank you for explaining. > > The funny thing is that I have never seen anybody take this even a single > step further than you have in your email. > > In particular I have not found anything where someone might use church > encoding to solve a quite practical problem, namely for implementing > extensible records. > I think this article uses Church encoded lists, I could be wrong: http://okmij.org/ftp/Algorithms.html#zip-folds Jason ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Steven S. Skiena of "The Algorithm Design Manual", Second Edition, 2008 has sent me a message that if there is a Haskell page of algorithms he will link to it.
Hi: Steven S. Skiena of "The Algorithm Design Manual", Second Edition, 2008 has sent me a message that if there is a Haskell page of algorithms he will link to it. So, is there such a page and/or is there some collection(s) of algorithms and data structures some where that I can massage into the shape of his book? :) -- Regards, Casey ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] gemcutter src?
On 16 May 2010 05:13, Henning Thielemann wrote: > http://resources.businessobjects.com/labs/cal/gemcutter-techpaper.pdf Does anyone have the url to the source code? (I guess businessobjects was acquired by SAP.) Jens ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Chuch encoding of data structures in Haskell
On Thu, May 27, 2010 at 9:11 PM, Stefan Monnier wrote: > I.e. to make such an encoding really usable, you need "deep > polymorphism" (which GHC supports just fine, but which is not part of > the Haskell standard). Ah, yes, and thank you for pointing that out. My message involved a great deal of hand-waving that I neglected to clearly identify as such. The same caveat of course applies to most Church encodings. For instance, the proper type of a (recursive) encoded list would be: type ChurchList a = ∀t. t -> (a -> t -> t) -> t ...where "a" is fixed as the type of the list elements. Thus, "cons" ought to look something like this charming type: cons :: ∀a. a -> (∀t. t -> (a -> t -> t) -> t) -> (∀t. t -> (a -> t -> t) -> t) For extra fun, try writing an instance such as: instance (Show a) => Show (ChurchList a) where [...etc.] ...at which point, perhaps, we remind ourselves that the language is named "Haskell", not "Alonzo", and drop the whole matter. - C. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] llvm on windows
on the topic of llvm, is anybody using llvm binding on windows ? The official llvm windows distro does not have a precompiled library which is required for the llvm bindings ? jvl ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell] Re: [Haskell-cafe] Work on Video Games in Haskell
On Thu, May 27, 2010 at 08:41:02PM -0400, Pierre-Etienne Meunier wrote: > > If this ever gets to court, we may have a criterion imposed on us, > > possibly one as silly as the distinction between programs and > > algorithms said to be made in patent-land. > > I really do agree with your post, but what I dont get is why Apple does not > intent anything against George Hotz, who publicly acknowledged having > disassembled his iphone for performing FPGA black magic on it, and would sue > someone for refusing objects and mallocs in programming. > > This makes me wonder if they really have the legal means of doing anything. Sure, they have the legal means to simply deny your program access to the App store. They don't need to sue you, you did nothing wrong by writing a haskell->c compiler and writing a game in it. They just won't distribute it. They are already under no obligation to distribute your work or make it available. John -- John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Chuch encoding of data structures in Haskell
> churchedBool :: t -> t -> t Important detail: the precise type is "∀t. t → t → t". > encodeBool x = \t e -> if x then t else e So the type of encodeBool should be: Bool → ∀t. t → t → t whereas Haskell will infer it to be ∀t. Bool → t → t → t which means that a given object can only be eliminated to one type. I.e. to make such an encoding really usable, you need "deep polymorphism" (which GHC supports just fine, but which is not part of the Haskell standard). Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Math questions
On 28 May 2010 09:37, Richard O'Keefe wrote: > > On May 27, 2010, at 11:50 PM, Yitzchak Gale wrote: >> >> agree100 = (==) `on` for [1..100] > > Search for "on" and "for" in the Haskell 98 Report and you > will not find them. If you want to tell someone to use them, > you ought to tell them where to find them. You mean like this? http://haskell.org/hoogle/?hoogle=on http://haskell.org/hoogle/?hoogle=for -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell] Re: [Haskell-cafe] Work on Video Games in Haskell
> If this ever gets to court, we may have a criterion imposed on us, > possibly one as silly as the distinction between programs and > algorithms said to be made in patent-land. I really do agree with your post, but what I dont get is why Apple does not intent anything against George Hotz, who publicly acknowledged having disassembled his iphone for performing FPGA black magic on it, and would sue someone for refusing objects and mallocs in programming. This makes me wonder if they really have the legal means of doing anything. Cheers, PE___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Chuch encoding of data structures in Haskell
On Thursday 27 May 2010 7:15:15 pm Brandon S. Allbery KF8NH wrote: > On May 27, 2010, at 19:07 , Brandon S. Allbery KF8NH wrote: > > reordered_cons :: (t -> (t1 -> t2)) -> t -> (t1 -> t2) > > churchedNumeral :: (t -> t ) -> t -> t > > > > t unifies with (t1 -> t2), giving us a Church numeral made up of > > (t1,t2). (I think.) > > Which also explains why that record representation isn't used: it's > as inefficient as Peano numbers are. Church encoding has additional efficiency problems, too. If we look at Peano numerals for instance, the Church encoding is: forall r. r -> (r -> r) -> r This means that our only method of computation with them is the structurally recursive fold. So, suppose we want to implement a predecessor operation. With Haskell-like data, we do: pred :: Nat -> Nat pred Zero= Zero pred (Suc n) = n This operation is expected to be O(1). What if we want to write this using only fold? Well, we have to do tricks (this same trick works to define tail with foldr): pred n = snd $ fold (Zero, Zero) (\ ~(m, _) -> (Suc m, m)) So, we've done it, but if you look closely, you'll see that we've actually rebuilt the entire 'tail' of the number. So this definition is O(n) (at least, if it all gets evaluated). So, Church encodings are less efficient than a direct implementation is capable of being. There is a dual problem with codata. You can encode the extended natural numbers as: exists s. (s, s -> Either () s) but this only gives you the anamorphism. So, if you want to write the successor operation, it's: succ n = (Nothing, step) where step Nothing = Right (Just n) step (Just m) = case observe m of Left () -> Left () Right m' -> Right (Just m') so we end up re-unfolding the entire number. Taking the paramorphism/apomorphism as a primitive operation fixes this, I believe, but you cannot, to my knowledge, encode types that way in, say, System F, because it would involve: Nat = forall r. r -> (Nat -> r -> r) -> r which is still a recursive equation. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
So what would you consider a proof that there are no total Haskell functions of that type? Or, using Curry-Howard, a proof that the corresponding logical formula is unprovable in intuitionistic logic? As I understand, in general this can only be proven using meta theory rather than the logic itself (it could happen that the given formula implies absurdity, and then we'd know it can't be proven, given that the logic is consistent). If Djinn correctly implements the decision procedure that have been proven to be total (using meta theory), then I would regard Djinn saying no as a proof that there is no function of that type. -- Lennart On Thu, May 27, 2010 at 7:49 PM, wren ng thornton wrote: > Dan Doel wrote: >> >> On Thursday 27 May 2010 3:27:58 am wren ng thornton wrote: >>> >>> By parametricty, presumably. >> >> Actually, I imagine the way he proved it was to use djinn, which uses a >> complete decision procedure for intuitionistic propositional logic. The >> proofs of theorems for that logic correspond to total functions for the >> analogous type. Since djinn is complete, it will either find a total >> function with the right type, or not, in which case there is no such >> function. >> >> At that point, all you have left to do is show that djinn is in fact >> complete. For that, you can probably look to the paper it's based on: >> Contraction-Free Sequent Calculi for Intuitionistic Logic* (if I'm not >> mistaken) by Roy Dyckhoff. > > Sure, that's another option. But the failure of exhaustive search isn't a > constructive/intuitionistic technique, so not everyone would accept the > proof. Djinn is essentially an implementation of reasoning by parametricity, > IIRC, so it comes down to the same first principles. > > > (Sorry, just finished writing a philosophy paper on intuitionism :) > > -- > Live well, > ~wren > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Optimizations and constant unboxed values
Hi Cafe,
Profiling a function that I thought ultra simple revealed that it consumed more
than half the execution time of my code. After noticing that GHC did not unbox
all I thought it did, I rewrote it with primitive types, and it did a little
better, but not much. Then, examining the core (with of course -O3 on) revealed
things like :
(GHC.Prim.*##
(GHC.Prim.-## 1.0 (GHC.Prim.**## 2.0 -53.0))
(GHC.Prim.**## 2.0 1024.0))
or
case GHC.Prim.<## x_aB9 (GHC.Prim.**## 2.0 -1021.0) of _ {...
Then I wondered if this was really the last stage of GHC's optimizations, as
constants are not yet propagated. Or maybe GHC does not propagate constants, in
which case I'd really like to write my 1-2^53 and 2^-1021 once and for all in
my program. But since unsafeCoerce# does not work between doubles and words (
there is a trac ticket about it :
http://hackage.haskell.org/trac/ghc/ticket/4092 ), I do not even think this is
possible (and of course, specifying a double in decimal notation with ## is not
precise enough for this program).
Any clue about how to do it ?
Thanks,
PE
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Math questions
On May 27, 2010, at 11:50 PM, Yitzchak Gale wrote: Mujtaba Boori wrote: I think this answer agree100 f g = map f xs == map g xs where xs = [1..100] from Richard O'Keefe is do the job. agree100 = (==) `on` for [1..100] Search for "on" and "for" in the Haskell 98 Report and you will not find them. If you want to tell someone to use them, you ought to tell them where to find them. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma
On Thu, May 27, 2010 at 5:43 PM, David Menendez wrote:
> On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao
> wrote:
> > Isaac Dupree:
> >> Your proposal appears to allow /incoherent/ instance selection.
> >> This means that an expression can be well-typed in one module, and
> >> well-typed in another module, but have different semantics in the
> >> two modules. For example (drawing from above discussion) :
> >>
> >> module C where
> >>
> >> class F a b where f :: a -> b
> >> class O a where o :: a
> >>
> >> module P where
> >> import C
> >>
> >> instance F Bool Bool where f = not
> >> instance O Bool where o = True
> >> k :: Bool
> >> k = f o
> >>
> >> module Q where
> >> import C
> >> instance F Int Bool where f = even
> >> instance O Int where o = 0
> >> k :: Bool
> >> k = f o
> >>
> >> module Main where
> >> import P
> >> import Q
> >> -- (here, all four instances are in scope)
> >> main = do { print P.k ; print Q.k }
> >> -- should result, according to your proposal, in
> >> -- False
> >> -- True
> >> -- , am I correct?
> >
> > If qualified importation of k from both P and from Q was specified, we
> > would have two *distinct* terms, P.k and Q.k.
>
> I think Isaac's point is that P.k and Q.k have the same definition (f
> o). If they don't produce the same value, then referential
> transparency is lost.
>
> --
> Dave Menendez
>
[Haskell-cafe] Multidimensional generalization of the vector package
Hey everyone, I have been thinking about how to generalize the vector package to multiple dimensions, and I'd like to share my ideas with you all in the hope of having people smarter than me share their thoughts on how it could be improved --- *especially* regarding how to make it efficient! The standard way to represent a memory layout is to use a stride vector --- i.e., a vector which lets you get the (flat) index in memory of a given element by dotting the stride vector with the multidimensional index vector. This has the advantage that one can efficiently manipulate it to represent views with arbitrary slices, subranges, subranges plus striping (i.e., take every k-th element), and transpositions. Basically the only thing it can't do is represent a weird view where we, say, take every index along a particular dimension that is a prime number. Having said this, it might be useful to abstract the memory layout in order to preserve generality. Thus, I was thinking that the layout of the multidimensional vector could be represented as a type class with an associated type family: class MemoryLayout layout where type LayoutIndex layout :: * indexOf :: layout -> (LayoutIndex layout) -> Int firstIndex :: layout -> (LayoutIndex layout) -> Int lastIndex :: layout -> (LayoutIndex layout) -> Int withinBounds :: layout -> (LayoutIndex layout) -> Bool ... etc. It is important that we be able to iterate through the array efficiently. One way that this could be done is through the use of cursors. class MemoryLayout layout where ... type LayoutCursor layout :: * ... getCursorAt :: layout -> (LayoutIndex layout) -> (LayoutCursor cursor) getFirstCursor :: layout -> (LayoutCursor cursor) getLastCursor :: layout -> (LayoutCursor cursor) indexOfCursor :: layout -> (LayoutCursor cursor) -> Int advanceCursor :: layout -> (LayoutCursor cursor) -> (LayoutCursor cursor) In general these unfortunately cannot be integers because integers don't contain enough information to tell us about where we need to go next inside a non-contiguous array. The alternative is to use a data structure, but then we may potentially have lots of potentially wasteful allocations, deallocations, and copying going on unless we can somehow cause the cursor to be updated destructively. Fortunately, much of the time our array will be contiguous, so we can have a special case fast-path for this case: class MemoryLayout layout where ... layoutIsContiguous :: layout -> Bool layoutIsContiguousWhenTraversedInRowMajorOrder :: layout -> Bool layoutIsContiguousWhenTraversedInColumnMajorOrder :: layout -> Bool Then we know that we can just iterate through the array in the order of the indices. It turns out that it is not hard to compute whether a layout is contiguous efficiently. For example, in the code that implements cuts and slicing we can actually check to see if the new view is still contiguous and simply cache this in the layout. For restricted cases of layouts (when there aren't transpositions) it isn't too hard to just scan through the layout and see if it is contiguous. Another way to iterate through the array is to provide this capability by constructing functions that traverse through the array for us and call some user-supplied function on each element. This actually can be a lot more efficient (since by using recursive algorithms it can store the information that it needs on the stack rather than using heap allocations) but it is much more restrictive, and it requires special cases for traversing multiple arrays in parallel. Probably the most general way to sum/fold/etc. over particular dimensions (i.e., given a 4D vector, sum over the first and third dimensions leaving the second and fourth dimensions) is simply to generalize the notion of cursors, so that rather than iterating over elements we are iterating over views of the array. class (MemoryLayout layout1, MemoryLayout layout2) => MemoryLayoutSubviewable layout1 layout2 where type MemoryLayoutViewSetSlicer layout1 layout2 :: * type MemoryLayoutViewSet layout1 layout2 :: * getViewSet :: (MemoryLayoutViewSetSlicer layout1 layout2) -> layout1 -> (MemoryLayoutViewSet layout1 layout2) advanceViewSet :: (MemoryLayoutViewSet layout1 layout2) -> (MemoryLayoutViewSet layout1 layout2) currentView :: MemoryLayoutViewSet layout1 layout2 -> layout2 This way we can hand getViewSet some "slicer" that selects some dimensions to be reduced but not others and get back a set of views that we can iterate over, providing a generalization of the sum and fold functionality provided by repa. Although these framework allows us to stay general, in practice working with shapes that are fixed-length vectors (I personally would prefer the Vec package over the hand-rolled one
Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure
> Monstro I'm going to call it that from now on. Stay out of the IO Monstro. -deech On 5/27/10, Mike Dillon wrote: > begin C. McCann quotation: >> Personally, I advocate instead using "Sinister" and "Dexter". Nice and >> catchy, don't you think? > > Has anyone done a "translation" of the Prelude into Latin? > >> modulus PraeLudus ubi >> >> data Uter a b = Sinister a >> | Dexter b >> derivare (Aequo, Ordinaro, Lego, Monstro) > > Ha. > > -md > ___ > 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] Why Either = Left | Right instead of something like Result = Success | Failure
* Ionut G. Stan wrote: > I was just wondering if there's any particular reason for which the two > constructors of the Either data type are named Left and Right. Yes. The basic function on this type is "either". either a b (Left x) = Left (a x) either a b (Right x) = Right (b x) So the names of the constuctors are "natural". ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell] Re: [Haskell-cafe] Work on Video Games in Haskell
I think some of us may be missing the point about language identification. It's not a _technical_ question, it's a _legal_ one. Apple's lawyers have available to them exactly the kind of instrument they expect (as lawyers) to have: legal testimony. If you sign up to the new rules, you are entering into a contract, and whether Apple _engineers_ can tell what you originally wrong in or not, if Apple's _lawyers_ are called in, you will find yourself answering: Q: Well, Mr/Ms/Dr/ Developer, did you personally write any of the code in this program? A: Yes. Q: And did you write it directly in one of the programming languages allowed in the contract, or did you use some other programming language? A: The code that was checked into the repository was in C and had never been in any other known programming language, but it was actually generated from a table of player descriptions using a little AWK script. Q: So what you are saying is that you knowingly violated the terms of the contract? Given the code generation and refactoring capabilities of things like NetBeans and Eclipse, notions of "written" and "originally" are getting even fuzzier than they always were, which is saying something. If this ever gets to court, we may have a criterion imposed on us, possibly one as silly as the distinction between programs and algorithms said to be made in patent-land. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Chuch encoding of data structures in Haskell
Of interest, (.+.) is the T combinator - called (##) in Peter Thiemann's Wash and the queer bird in Raymond Smullyan's To Mock a Mockingbird. Your technique might well relate to the 'element transforming style' of Wash, see the Modelling HTML in Haskell paper. Best wishes Stephen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Chuch encoding of data structures in Haskell
On May 27, 2010, at 13:44 , Günther Schmidt wrote: The approach is so simple and trivial that it must have occurred to people a hundred times over. Yet I do not find any other examples of this. Whenever I google for church encoding the examples don't go beyond church numerals. Hm. If I reorder your (.+.) slightly and reparenthesize: reordered_cons :: (t -> (t1 -> t2)) -> t -> (t1 -> t2) churchedNumeral :: (t -> t ) -> t -> t t unifies with (t1 -> t2), giving us a Church numeral made up of (t1,t2). (I think.) -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon universityKF8NH PGP.sig Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma
On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao
wrote:
> Isaac Dupree:
>> Your proposal appears to allow /incoherent/ instance selection.
>> This means that an expression can be well-typed in one module, and
>> well-typed in another module, but have different semantics in the
>> two modules. For example (drawing from above discussion) :
>>
>> module C where
>>
>> class F a b where f :: a -> b
>> class O a where o :: a
>>
>> module P where
>> import C
>>
>> instance F Bool Bool where f = not
>> instance O Bool where o = True
>> k :: Bool
>> k = f o
>>
>> module Q where
>> import C
>> instance F Int Bool where f = even
>> instance O Int where o = 0
>> k :: Bool
>> k = f o
>>
>> module Main where
>> import P
>> import Q
>> -- (here, all four instances are in scope)
>> main = do { print P.k ; print Q.k }
>> -- should result, according to your proposal, in
>> -- False
>> -- True
>> -- , am I correct?
>
> If qualified importation of k from both P and from Q was specified, we
> would have two *distinct* terms, P.k and Q.k.
I think Isaac's point is that P.k and Q.k have the same definition (f
o). If they don't produce the same value, then referential
transparency is lost.
--
Dave Menendez
Re: [Haskell-cafe] Re: Unicode vs. System.Directory
Hello Andy, Thursday, May 27, 2010, 5:45:27 PM, you wrote: does it work both on linux and windows? i'm very interested to run executables of both kinds and look what features are really supported (i write file/archive manager and it seems that you have solved many problems that drive me crazy, such as displaying icons/filetypes, launching documents...) > Hi Arie, > If you don't mind binding code. > You can try to use GIO APIs from my repository: > http://patch-tag.com/r/AndyStewart/gio-branch/home > GIO APIs handle unicode filename every well, and cross-platform. > Cheers, > -- Andy > Arie Peterson writes: >> After upgrading to haskell-platform-2010.1.0.0, with the improved unicode >> support for IO in ghc-6.12, I hoped to be able to deal with filenames >> containing non-ascii characters. This still seems problematic, though: >> >> $ ls >> m?n?? >> $ ghci >> GHCi, version 6.12.1: http://www.haskell.org/ghc/ :? for help >> Prelude> :m +System.Directory >> Prelude System.Directory> getDirectoryContents "." >>= mapM_ putStrLn >> .. >> mAna?I± >> . >> >> I hope this passes through the various email systems unharmed; on my >> terminal, the output of 'ls' contains shiny unicode characters, while >> 'ghci' garbles up the filename. (My locale is en_GB.utf8.) >> >> Similar problems arise with functions such as 'copyFile', which refuses to >> handle filenames with non-ascii characters (unless wrapping it with >> encoding functions). >> >> >> Is this a known problem? I searched ghc's trac, but there are no relevant >> bugs for the component 'libraries/directory'. >> >> >> I have parts of a unicode-aware layer on top of System.Directory laying >> around somewhere. I was rather hoping to ditch it, but I can polish it and >> put it on hackage, if people are interested. >> >> >> Kind regards, >> >> Arie > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe -- 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] Why Either = Left | Right instead of something like Result = Success | Failure
On May 27, 2010, at 10:53 , Vo Minh Thu wrote: 2010/5/27 Ionut G. Stan : I was just wondering if there's any particular reason for which the two constructors of the Either data type are named Left and Right. I'm thinking that something like Success | Failure or Right | Wrong would have been a little better. I've recently seen that Scala uses a similar convention for some error notifications so I'm starting to believe there's more background behind it than just an unfortunate naming. Either *can* be used to represent success and failures, but not necessarily. It is a convention, when using Either to model success/failure, to use Right for success and Left for failure. Even if Left as a word does not match with the meaning of failure, it is easy to get it Right :) Historically it *has* been related to negativity in many cultures. (Consider "sinister", cognate of Italian "sinistro/a", and the prevalence of and preference for right-handed-ness.) -- 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] Chuch encoding of data structures in Haskell
Günther Schmidt writes: > Hi all, > > I'm exploring the use of church encodings of algebraic data types in > Haskell. > Since it's hard to imagine being the first to do so I wonder if folks > here could point me to some references on the subject. > > I'm looking for examples of church encodings in Haskell a little bit > beyond Church Booleans and Church Numerals. It's not quite practical, but have a look at Paul Bailes' Totally Functional Programming papers: http://www.itee.uq.edu.au/~paul/tfp-papers/ Also, Types and Programming Languages by Benjamin Pierce (who keeps reminding me of M*A*S*H, even though his middle name starts with a C...) has a decent section on church encodings. -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
On Thursday 27 May 2010 1:49:36 pm wren ng thornton wrote: > Sure, that's another option. But the failure of exhaustive search isn't > a constructive/intuitionistic technique, so not everyone would accept > the proof. Djinn is essentially an implementation of reasoning by > parametricity, IIRC, so it comes down to the same first principles. How, exactly, is it non-constructive to encode the propositional calculus and its proofs as, say, types in intuitionistic type theory, write the algorithm djinn uses in the same (it was specially crafted to be provably terminating, after all), and prove the algorithm complete (again, hopefully in the type theory)? I realize this has not all been done, strictly speaking, but I see nowhere that it is necessarily non-constructive. If you point is that the result you get is: ¬ ⊢ (...) instead of ⊢ ¬ (...) then this is true, but the former is what was originally claimed (there are no total functions of that type ==> that proposition is not a theorem). In fact, if one can prove the second, then we're in trouble, because the proposition is a classical theorem, and djinn provides a result for ⊢ ¬ ¬ (...) which contradicts the second statement above. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Chuch encoding of data structures in Haskell
The approach is so simple and trivial that it must have occurred to people a hundred times over. Yet I do not find any other examples of this. Whenever I google for church encoding the examples don't go beyond church numerals. Am I googling for the wrong keywords? You might find "Typing Record Concatenation for Free" interesting: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.401 Claus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Wire GUI
I'm looking at a project which involves a GUI where you can insert components and wire up connections between them. Obviously the details of what the components are and what code gets executed for them is domain-specific, however the general idea of graphically wiring things together is quite generic. Has anybody already put together a Haskell library for doing this kind of thing? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Chuch encoding of data structures in Haskell
On May 27, 2010, at 19:07 , Brandon S. Allbery KF8NH wrote: reordered_cons :: (t -> (t1 -> t2)) -> t -> (t1 -> t2) churchedNumeral :: (t -> t ) -> t -> t t unifies with (t1 -> t2), giving us a Church numeral made up of (t1,t2). (I think.) Which also explains why that record representation isn't used: it's as inefficient as Peano numbers are. -- 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] Why Either = Left | Right instead of something like Result = Success | Failure
begin C. McCann quotation: > Personally, I advocate instead using "Sinister" and "Dexter". Nice and > catchy, don't you think? Has anyone done a "translation" of the Prelude into Latin? > modulus PraeLudus ubi > > data Uter a b = Sinister a > | Dexter b > derivare (Aequo, Ordinaro, Lego, Monstro) Ha. -md ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] double2Float is faster than (fromRational . toRational)
Hello Daniel, Friday, May 21, 2010, 11:55:35 PM, you wrote: > xf = (fromRational $ toRational xd) :: Float > xf = double2Float xd > am still surprised how often such kinds of unobvious problems occur > while programming in Haskell does it mean that all other languages you are used doesn't have such problem or that you are an inexperienced programmer? :) -- Best regards, Bulatmailto:bulat.zigans...@gmail.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Gtk2hs-users] Problem when installing gtk2hs.
On May 27, 2010, at 02:46 , Magicloud Magiclouds wrote: I only have one alex installed under ~/.cabal/bin. It seems working with shell environment, but not cabal. But you're doing the Cabal install as root, so it's likely using / root/.cabal/bin instead of your home directory. Or possibly doing a global install which would ignore ~/.cabal. Better would be a global install of tools like Alex. -- 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] currying combinators
Dan Doel wrote: On Thursday 27 May 2010 3:27:58 am wren ng thornton wrote: By parametricty, presumably. Actually, I imagine the way he proved it was to use djinn, which uses a complete decision procedure for intuitionistic propositional logic. The proofs of theorems for that logic correspond to total functions for the analogous type. Since djinn is complete, it will either find a total function with the right type, or not, in which case there is no such function. At that point, all you have left to do is show that djinn is in fact complete. For that, you can probably look to the paper it's based on: Contraction-Free Sequent Calculi for Intuitionistic Logic* (if I'm not mistaken) by Roy Dyckhoff. Sure, that's another option. But the failure of exhaustive search isn't a constructive/intuitionistic technique, so not everyone would accept the proof. Djinn is essentially an implementation of reasoning by parametricity, IIRC, so it comes down to the same first principles. (Sorry, just finished writing a philosophy paper on intuitionism :) -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Chuch encoding of data structures in Haskell
Hello C,
thank you for explaining.
The funny thing is that I have never seen anybody take this even a
single step further than you have in your email.
In particular I have not found anything where someone might use church
encoding to solve a quite practical problem, namely for implementing
extensible records.
For instance suppose we'd have
data Person = Person { firstName :: String, lastName :: String }
person1 :: Person
person1 = Person "John" "Doe"
alternatively, and I'm not 100% if this what is commonly understood as
"church encoding" I'm just guessing, we could write this:
person1' :: (String -> String -> x) -> x
person1' = \fn -> fn "John" "Doe"
Now from a practical standpoint, up to here anyway, the first encoding
is far more useful.
But there is a problem when we want to extend the Person type by a new
field, age for instance. Person as such is *not* extensible, modifying
it would require us to rewrite existing code.
But person1' is easily extended:
person1'' :: (String -> String -> Int -> x) -> x
person1'' = \fn -> person1' fn 36
or more generally:
(.+.) :: (t1 -> t -> t2) -> t -> t1 -> t2
rec .+. v = \fn -> rec fn v
person1''' :: (String -> String -> Int -> x) -> x
person1''' = person1'' .+. 36
There is also a way to shrink the "record" from the left:
drp :: ((t1 -> t) -> b) -> t -> b
drp rec = \fn -> rec $ \_ -> fn
I can think of a number of applications for this and especially I
believe it should be possible to create more "combinators".
The approach is so simple and trivial that it must have occurred to
people a hundred times over. Yet I do not find any other examples of
this. Whenever I google for church encoding the examples don't go beyond
church numerals.
Am I googling for the wrong keywords?
Best regards
Günther
Am 27.05.10 19:10, schrieb C. McCann:
2010/5/27 Günther Schmidt:
I'm exploring the use of church encodings of algebraic data types in
Haskell.
Since it's hard to imagine being the first to do so I wonder if folks here
could point me to some references on the subject.
I'm looking for examples of church encodings in Haskell a little bit beyond
Church Booleans and Church Numerals.
The fully general description of Church encoding is rather simple, but
I've rarely seen it described explicitly. Consider the type of Church
encodings for Bool, Either, and the 2-tuple (written here as "Pair"
for clarity):
churchedBool :: t -> t -> t
churchedEither :: (a -> t) -> (b -> t) -> t
churchedPair :: (a -> b -> t) -> t
And compare the signatures for the constructors of the non-Church encoded types:
True :: Bool
False :: Bool
Left :: a -> Either a b
Right :: b -> Either a b
Pair :: a -> b -> Pair a b
We can observe two patterns: 1) The Church encodings take as many
arguments as the type has constructors 2) The type of each argument is
the same as the signature of a constructor, except returning an
arbitrary type. As this suggests, "Church decoding" is as simple as
applying the Church encoded type to each of the constructors.
From the above, a general description of Church encoding can be
deduced: The encoding of a value is a function that replaces each data
constructor with an arbitrary function. The Church encoding
represents, in a way, the most generalized means of using values of
that type--which is why Haskell already includes variations of "Church
encode" functions for a few standard types, like so:
encodeEither x = \f g -> either f g x
encodeMaybe x = \z f -> maybe z f x
encodeTuple x = \f -> uncurry f x
encodeBool x = \t e -> if x then t else e
But what of Church numerals? First, we must consider the
Church-encoding of recursive data types. Given arbitrary nested data
types, there's nothing else that can be done--the outer types know
nothing of the types they contain. But if an inner type is known to be
the same as the outer type, there are two options for the encoding:
Work only with the outermost value, as with non-recursive types, or
work with the recursive value as a whole, by having the outermost
value pass its arguments inward.
Now, consider the signature of a Church numeral:
churchedNumeral :: (t -> t) -> t -> t
Given the above, what can we say about the equivalent "decoded" data
type? It takes two arguments, so we have two constructors. The second
argument is a single value, so the associated constructor is nullary.
The first argument must be associated with a unary constructor, but
look at the parameter it takes: the same type as the result! This is
how we can tell that Church numerals are the encoding of a recursive
type. Since the only way a recursive constructor can do anything with
the values it contains is to pass its arguments inward, the value it
has to work with is the result of doing so. Thus, the other
constructor must take a single argument of its own type. What does
this look like as a standard data type?
data Nat = S Nat | Z
Good old inefficient Peano numbers, of course!
Keeping all that in
Re: [Haskell-cafe] currying combinators
wren ng thornton wrote: David Sankel wrote: keep :: ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b Lennart Augustsson wrote: There are no interesting (i.e. total) functions of that type. I wonder how one would prove that to be the case. I tried and didn't come up with anything. By parametricty, presumably. We must ultimately construct some value of type b, where b is universally quantified. Therefore, the only 'constructors' available for b are the ((t -> b) -> u -> b) and ((t1 -> t) -> b) arguments. However, since b is universally quantified, these arguments have no way of actually constructing some b, other than by returning bottom. Er, that's not quite right. That's only true if those arguments are rank-2 quantified. I'd had a longer (correct) explanation and tried shortening it. So here's the better proof: In order to produce a value of type b, keep must either use one of those two arguments or return bottom. If it uses the ((t -> b) -> u -> b) argument, then keep can only return non-bottom if that function [1] ignores its arguments and returns an arbitrary b, or [2] uses the (t -> b) argument to construct the b. If we assume #1 then keep is not total, because we have no way of proving that the assumption is valid. So we must expect #2; so in order for keep to be total it must be able to construct a total function (t -> b). In order to construct such a function it must use one of the original two arguments, so this is only possible if we can construct a b via ((t1 -> t) -> b). If it uses the ((t1 -> t) -> b) argument, then keep can only return non-bottom if that function [1] ignores its arguments, or [2] uses the (t1 -> t) argument. We can't assume #1 and be total, so we must expect #2. In order to construct (t1 -> t) we must construct a t. But, since t is universally quantified, keep knows of no total functions which return t. Thus, keep can only construct a function which returns bottom. Thus, keep can only return non-bottom under the assumption that the ((t -> b) -> u -> b) and ((t1 -> t) -> b) arguments ignore their arguments to return a constant b. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure
Left-Right also good for representing binary trees. 2010/5/27 C. McCann > On Thu, May 27, 2010 at 10:25 AM, Ionut G. Stan > wrote: > > I was just wondering if there's any particular reason for which the two > > constructors of the Either data type are named Left and Right. I'm > thinking > > that something like Success | Failure or Right | Wrong would have been a > > little better. > > Because that would confuse matters when using the type for something > other than representing success or failure. > > Either is a generic sum type. That is, "Either A B" only means "either > you have an A, or you have a B". Use of Left to represent failure is > merely a matter of convention. Similarly, the generic product type in > Haskell is the 2-tuple--"(A, B)" only means "you have both an A and a > B". > > Left and Right work well because they don't carry much extra semantic > baggage, and they make it easy to remember which type parameter goes > with which constructor. Other than the mnemonic value, something even > more bland like This and That would work as well. > > Personally, I advocate instead using "Sinister" and "Dexter". Nice and > catchy, don't you think? > > - C. > ___ > 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] Chuch encoding of data structures in Haskell
2010/5/27 Günther Schmidt : > I'm exploring the use of church encodings of algebraic data types in > Haskell. > Since it's hard to imagine being the first to do so I wonder if folks here > could point me to some references on the subject. > > I'm looking for examples of church encodings in Haskell a little bit beyond > Church Booleans and Church Numerals. The fully general description of Church encoding is rather simple, but I've rarely seen it described explicitly. Consider the type of Church encodings for Bool, Either, and the 2-tuple (written here as "Pair" for clarity): churchedBool :: t -> t -> t churchedEither :: (a -> t) -> (b -> t) -> t churchedPair :: (a -> b -> t) -> t And compare the signatures for the constructors of the non-Church encoded types: True :: Bool False :: Bool Left :: a -> Either a b Right :: b -> Either a b Pair :: a -> b -> Pair a b We can observe two patterns: 1) The Church encodings take as many arguments as the type has constructors 2) The type of each argument is the same as the signature of a constructor, except returning an arbitrary type. As this suggests, "Church decoding" is as simple as applying the Church encoded type to each of the constructors. >From the above, a general description of Church encoding can be deduced: The encoding of a value is a function that replaces each data constructor with an arbitrary function. The Church encoding represents, in a way, the most generalized means of using values of that type--which is why Haskell already includes variations of "Church encode" functions for a few standard types, like so: encodeEither x = \f g -> either f g x encodeMaybe x = \z f -> maybe z f x encodeTuple x = \f -> uncurry f x encodeBool x = \t e -> if x then t else e But what of Church numerals? First, we must consider the Church-encoding of recursive data types. Given arbitrary nested data types, there's nothing else that can be done--the outer types know nothing of the types they contain. But if an inner type is known to be the same as the outer type, there are two options for the encoding: Work only with the outermost value, as with non-recursive types, or work with the recursive value as a whole, by having the outermost value pass its arguments inward. Now, consider the signature of a Church numeral: churchedNumeral :: (t -> t) -> t -> t Given the above, what can we say about the equivalent "decoded" data type? It takes two arguments, so we have two constructors. The second argument is a single value, so the associated constructor is nullary. The first argument must be associated with a unary constructor, but look at the parameter it takes: the same type as the result! This is how we can tell that Church numerals are the encoding of a recursive type. Since the only way a recursive constructor can do anything with the values it contains is to pass its arguments inward, the value it has to work with is the result of doing so. Thus, the other constructor must take a single argument of its own type. What does this look like as a standard data type? data Nat = S Nat | Z Good old inefficient Peano numbers, of course! Keeping all that in mind, consider a List type, and both ways of encoding it: data List a = Nil | Cons a (List a) churchedListOuter :: t -> (a -> ___ -> t) -> t churchedListRecursive :: t -> (a -> t -> t) -> t For the "outermost" method, what type belongs in place of the ___? The second argument of Cons is itself a List, so naively we would like to simply put the type of "churchedListOuter" itself in place of ___, but that won't work. In fact, nothing will work here, because recursion on an "outermost encoded" list is impossible in a typed λ-calculus without some means of using general recursion provided as a primitive operation. Nested tuples can be used, but the length of the list will be reflected in the type, preventing polymorphism over arbitrary lists. This is also why Church encoding is most often seen in the setting of the untyped λ-calculus. The implicitly recursive encoding, however, presents no such problems. So, perhaps a function to Church encode lists would be useful? Indeed it would, and as before, it already exists: encodeList x = \z f -> foldr f z x Recall the earlier observation that "decoding" involves applying the encoded type to its equivalent constructors; the same holds true for recursive types, as demonstrated by right-folding a list with (:) and [], or applying a Church numeral to 0 and (+ 1). Regarding recursive data types as the least fixed point of a non-recursive data type is thus tied to replacing the "outermost" encoding with the "recursive" encoding, and the "Church encode" function for a recursive type is simply a generalized right fold, partially applied. Now, the descriptions above are rather informal, and ignore the possibility of infinite lazy recursive data structures, among other gaps; but perhaps will help to get you started regardless. - C. ___
Re: [Haskell-cafe] currying combinators
On Thursday 27 May 2010 3:27:58 am wren ng thornton wrote: > By parametricty, presumably. Actually, I imagine the way he proved it was to use djinn, which uses a complete decision procedure for intuitionistic propositional logic. The proofs of theorems for that logic correspond to total functions for the analogous type. Since djinn is complete, it will either find a total function with the right type, or not, in which case there is no such function. At that point, all you have left to do is show that djinn is in fact complete. For that, you can probably look to the paper it's based on: Contraction-Free Sequent Calculi for Intuitionistic Logic* (if I'm not mistaken) by Roy Dyckhoff. -- Dan [*] http://www.cs.st-andrews.ac.uk/~rd/publications/jsl57.pdf ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure
On Thu, May 27, 2010 at 10:25 AM, Ionut G. Stan wrote: > I was just wondering if there's any particular reason for which the two > constructors of the Either data type are named Left and Right. I'm thinking > that something like Success | Failure or Right | Wrong would have been a > little better. Because that would confuse matters when using the type for something other than representing success or failure. Either is a generic sum type. That is, "Either A B" only means "either you have an A, or you have a B". Use of Left to represent failure is merely a matter of convention. Similarly, the generic product type in Haskell is the 2-tuple--"(A, B)" only means "you have both an A and a B". Left and Right work well because they don't carry much extra semantic baggage, and they make it easy to remember which type parameter goes with which constructor. Other than the mnemonic value, something even more bland like This and That would work as well. Personally, I advocate instead using "Sinister" and "Dexter". Nice and catchy, don't you think? - C. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure
It's indeed arbitrary. Other common names are Inl and Inr (presumably standing for "inject left/right"). Some Haskell project do indeed use a more specific name. The advantage of using the generic Left/Right is reusability of library code. The particular name of the datatype and its constructors are competely arbitrary. The use of "Right" for "Success" is a handy pun -- the program returned "the right answer". HTH, / Thomas On 27 May 2010 15:25, Ionut G. Stan wrote: > Hi, > > I was just wondering if there's any particular reason for which the two > constructors of the Either data type are named Left and Right. I'm thinking > that something like Success | Failure or Right | Wrong would have been a > little better. > > I've recently seen that Scala uses a similar convention for some error > notifications so I'm starting to believe there's more background behind it > than just an unfortunate naming. > > Thanks, > -- > Ionuț G. Stan | http://igstan.ro > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Push the envelope. Watch it bend. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure
On 27 May 2010, at 15:25, Ionut G. Stan wrote: > Hi, > > I was just wondering if there's any particular reason for which the two > constructors of the Either data type are named Left and Right. I'm thinking > that something like Success | Failure or Right | Wrong would have been a > little better. The reason I guess is that Success/Failure and Right/Wrong are a lot less general than Left/Right. One can use Either for types with two possible valid types contained within, it doesn't only have to be used for types where one is for "correct" results and the other for "erroneous". Of course, there's nothing stopping you implementing your own type :) Bob___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure
2010/5/27 Ionut G. Stan : > Hi, > > I was just wondering if there's any particular reason for which the two > constructors of the Either data type are named Left and Right. I'm thinking > that something like Success | Failure or Right | Wrong would have been a > little better. > > I've recently seen that Scala uses a similar convention for some error > notifications so I'm starting to believe there's more background behind it > than just an unfortunate naming. Hi, Either *can* be used to represent success and failures, but not necessarily. It is a convention, when using Either to model success/failure, to use Right for success and Left for failure. Even if Left as a word does not match with the meaning of failure, it is easy to get it Right :) Cheers, Thu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma
On 05/26/10 15:42, Carlos Camarao wrote:
> I think you are proposing using the current set of instances in
> scope in order to remove ambiguity. Am I right?
I think that an important point is that it is not exactly "to remove
ambiguity", because the proposal tries to solve the problem exactly
when there is really no ambiguity. There would be ambiguity if there
were two or more conflicting definitions, and the proposal is to use,
upon occurrence of an unreachable type variable in a constraint, an
instance in the current context that is the single instance that could
be used to instantiate that type variable.
This was perhaps made unclear when I incorrectly wrote in haskell-cafe
that the proposal eliminates the need for defaulting. I should have
said that defaulting is not necessary to force instantiation (of
unreachable variables) when there are no conflicting definitions in
the current context. That is, defaulting should be used exactly to
remove ambiguity, i.e. when there exist conflicting definitions and
when unreachable type variables appear that can be instantiated to
such conflicting definitions.
> Your proposal appears to allow /incoherent/ instance selection.
> This means that an expression can be well-typed in one module, and
> well-typed in another module, but have different semantics in the
> two modules. For example (drawing from above discussion) :
>
> module C where
>
> class F a b where f :: a -> b
> class O a where o :: a
>
> module P where
> import C
>
> instance F Bool Bool where f = not
> instance O Bool where o = True
> k :: Bool
> k = f o
>
> module Q where
> import C
> instance F Int Bool where f = even
> instance O Int where o = 0
> k :: Bool
> k = f o
>
> module Main where
> import P
> import Q
> -- (here, all four instances are in scope)
> main = do { print P.k ; print Q.k }
> -- should result, according to your proposal, in
> -- False
> -- True
> -- , am I correct?
If qualified importation of k from both P and from Q was specified, we
would have two *distinct* terms, P.k and Q.k.
Unqualified importation must cause an error (two distinct definitions
for the same non-overloaded name).
For overloaded names with distinct instances, *ambiguity* would be reported,
as e.g. in:
module C where class O a where o::a
module P where instance O Bool where o = True
module Q where instance O Bool where o = False
moduke Main where
import P
import Q
main = do { print o::Bool }
> Also, in your paper, example 2 includes
>m = (m1 * m2) * m3
> and you state
>> In Example 2, there is no means of specializing type variable c0
>> occurring in the type of m to Matrix.
> In Example 2, there is no means of specializing type variable c0
> occurring in the type of m to Matrix.
> I suggest that there is an appropriate such means, namely, to write
> m = (m1 * m2 :: Matrix) * m3
Yes, that solution is fine. Sorry, I should have written "There is no means
of specializing type variable c0 occurring in the type of m to Matrix,
without an explicit type annotation in the expression defining m."
> (Could the paper address how that solution falls short?
> Are there other cases in which there is more than just a little
> syntactical convenience at stake?
> , or is even that much added code too much for some use-case?)
The point should have been that you cannot make a class with
FDs eliminate the need for having to make explicit type annotations,
in cases such as these. The example should also be such that it
would need more type annotations, instead of just one...
Cheers,
Carlos
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Chuch encoding of data structures in Haskell
Hi all, I'm exploring the use of church encodings of algebraic data types in Haskell. Since it's hard to imagine being the first to do so I wonder if folks here could point me to some references on the subject. I'm looking for examples of church encodings in Haskell a little bit beyond Church Booleans and Church Numerals. Günther ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure
Hi, I was just wondering if there's any particular reason for which the two constructors of the Either data type are named Left and Right. I'm thinking that something like Success | Failure or Right | Wrong would have been a little better. I've recently seen that Scala uses a similar convention for some error notifications so I'm starting to believe there's more background behind it than just an unfortunate naming. Thanks, -- Ionuț G. Stan | http://igstan.ro ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Unicode vs. System.Directory
Hi Arie, If you don't mind binding code. You can try to use GIO APIs from my repository: http://patch-tag.com/r/AndyStewart/gio-branch/home GIO APIs handle unicode filename every well, and cross-platform. Cheers, -- Andy Arie Peterson writes: > After upgrading to haskell-platform-2010.1.0.0, with the improved unicode > support for IO in ghc-6.12, I hoped to be able to deal with filenames > containing non-ascii characters. This still seems problematic, though: > > $ ls > m×n♯α > $ ghci > GHCi, version 6.12.1: http://www.haskell.org/ghc/ :? for help > Prelude> :m +System.Directory > Prelude System.Directory> getDirectoryContents "." >>= mapM_ putStrLn > .. > mÃnâ¯Î± > . > > I hope this passes through the various email systems unharmed; on my > terminal, the output of 'ls' contains shiny unicode characters, while > 'ghci' garbles up the filename. (My locale is en_GB.utf8.) > > Similar problems arise with functions such as 'copyFile', which refuses to > handle filenames with non-ascii characters (unless wrapping it with > encoding functions). > > > Is this a known problem? I searched ghc's trac, but there are no relevant > bugs for the component 'libraries/directory'. > > > I have parts of a unicode-aware layer on top of System.Directory laying > around somewhere. I was rather hoping to ditch it, but I can polish it and > put it on hackage, if people are interested. > > > Kind regards, > > Arie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
** Advertisement ** Have you tried the library I have written, Data.Rope ? ** End of advertisement ** The algorithmic complexity of most operations on ropes is way better than on bytestrings : log n for all operations, except traversals, of course. Cheers, PE El 27/05/2010, a las 06:01, Michael Snoyman escribió: > > > On Thu, May 27, 2010 at 12:57 PM, Johan Tibell wrote: > On Thu, May 27, 2010 at 10:23 AM, Michael Snoyman wrote: > On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic > wrote: > Wow, I find it rather surprising that String out-performs Text; any > idea why that is? I wonder if you're just using it wrong... > > Could be, I'd be very happy if that were the case. All of the benchmarks are > available on Github, and the bytestring[1], text[2] and string[3] versions > are all rather short. > > Do you include the cost of encoding the result as e.g. UTF-8? The hope would > be that the more compact Text would be faster to traverse, and thus encode, > than the list based String. > > No, but this is done on purpose. One of my goals in this benchmark was to > determine whether I should consider switching Hamlet to ByteStrings. If I > were to do so, then the UTF-8 encoding would be done at compile-time instead > of run-time. > > You're correct that a fair comparison would be to UTF-8 encode the Strings as > well. However, that's not what most users are going to do most of the time: > when dealing with ASCII data, a straight Char8.pack encoding will do the same > as UTF-8. I'm simply pointing out that I think Blaze should support this > style. > > Michael > ___ > 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] Re: [Haskell-cafe] Work on Video Games in Haskell
There is a enormous bunch of C code out there on the internet. It is not that hard to simply take arbitrary commentaries and variable names from it, then using it to replace GHC's "jjaksh34$"-like variables in the core. Doing objective-c is a bit harder, as you have to use the objects, or else the choice of objective-c instead of c would look suspicious. This requires to find the rules that make an object programmer happy. El 27/05/2010, a las 02:40, Ketil Malde escribió: > writes: > >> Or maybe this would be a nice research topic: how to generate C code >> that looks like it’s human written… > > Nah, that's too easy: just add a sprinkling of buffer overflows, > undefined behavior, and off-by one index errors. > > -k > -- > If I haven't seen further, it is by standing in the footprints of giants > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Math questions
Mujtaba Boori wrote: > I think this answer agree100 f g = map f xs == map g xs where > xs = [1..100] from Richard O'Keefe > is do the job. agree100 = (==) `on` for [1..100] Regards, Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Gtk2hs-users] Problem when installing gtk2hs.
On Thursday 27 May 2010 08:46:04, Magicloud Magiclouds wrote: > I only have one alex installed under ~/.cabal/bin. > It seems working with shell environment, but not cabal. > My guess: You added ~/.cabal/bin to the path, but have quoted the path, like export PATH="~/.cabal/bin:$PATH" in your .bashrc That does not work. Tilde expansion is *not* done for quoted strings, so cabal looks (among other places) for "~/.cabal/bin/alex". Now, there is no directory "~" in your file system, so alex is not found. Check: $ printenv PATH If the output contains ~, it won't work. If it doesn't, well then something else must be broken. Fixes 1) don't quote the path, export PATH=~/.cabal/bin:$PATH works. 2) (better) Use $HOME instead of ~ (works quoted or unquoted) 3) write out your home directory completely ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
As a user, I have too many HTML generators, a few of them with Ajax and none with server-side event handling (like ASPX or JSPX). Ajax is complicated but server side event handling is what I really miss because it is simple from the user point of view, my ervents could be handled in haskell code rather than in javaScript and I implicitly could use the advantages of dinamic HTML and Ajax without the need to know them at all. Imagine a dynamic Web application with 100% haskell code made with dynamic widgets created by third party developers. So, anyone want to create a HTML templating system with server side event handling? It is not terribly hard to do. (I refer to ASP.NET documentation or the JavaServer Faces framework). By the way, I vote for XML templating or else, combinator templating that produce XHML templating because it can be handled by a future graphical IDE. 2010/5/27 Jasper Van der Jeugt > Hey Bas, > > > How about also providing an enumerator back-end? > > > http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM > > > > Then your library can integrate more easily with the snap framework: > > http://snapframework.com > > Sure, I can do that. But I already tested integration with the snap > framework, the best path here seems to call the `writeLBS` function > from the snap framework on the `L.ByteString` that BlazeHtml produces > (`writeLBS` internally uses an enumerator). > > Kind regards, > Jasper Van der Jeugt > > On Thu, May 27, 2010 at 10:38 AM, Bas van Dijk > wrote: > > Q14: Do you see any problems with respect to integrating BlazeHtml in > > your favourite web-framework/server? > > > > How about also providing an enumerator back-end? > > > http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM > > > > Then your library can integrate more easily with the snap framework: > > http://snapframework.com > > > > Regards, > > > > Bas > > > ___ > 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] Google Summer of Code: BlazeHTML RFC
On Thu, May 27, 2010 at 10:53 AM, Michael Snoyman wrote:
> In other words, here's what I think the three different benchmarks are
> really doing:
>
> * String: generates a list of Strings, passes each String to a relatively
> inefficient IO routine.
> * ByteString: encodes Strings one by one into ByteStrings, generates a list
> of these ByteStrings, and passes each ByteString to a very efficient IO
> routine.
> : Text: encodes Strings one by one into Texts, generates a list of these
> Texts, calls a UTF-8 decoding function to decode each Text into a
> ByteString, and passes each resulting ByteString to a very efficient IO
> routine.
>
If Text used UTF-8 internally rather than UTF-16 we could create Texts from
string literals much more efficiently, in the same manner as done in
Char8.pack for bytestrings:
{-# RULES
"FPS pack/packAddress" forall s .
pack (unpackCString# s) = inlinePerformIO (B.unsafePackAddress s)
#-}
This rule skips the creation of an intermediate String when packing a string
literal by having the created ByteString point directly to the memory GHC
allocates (outside the heap) for the string literal. This rule could be
added directly to a builder monoid for lazy Texts so that no copying is done
at all. In addition, if Text was internally represented using UTF-8
encodeUtf8 would be free.
Johan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
On Thu, May 27, 2010 at 12:57 PM, Johan Tibell wrote: > On Thu, May 27, 2010 at 10:23 AM, Michael Snoyman wrote: > >> On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic < >> ivan.miljeno...@gmail.com> wrote: >> >>> Wow, I find it rather surprising that String out-performs Text; any >>> idea why that is? I wonder if you're just using it wrong... >>> >>> Could be, I'd be very happy if that were the case. All of the benchmarks >> are available on Github, and the bytestring[1], text[2] and string[3] >> versions are all rather short. >> > > Do you include the cost of encoding the result as e.g. UTF-8? The hope > would be that the more compact Text would be faster to traverse, and thus > encode, than the list based String. > > No, but this is done on purpose. One of my goals in this benchmark was to determine whether I should consider switching Hamlet to ByteStrings. If I were to do so, then the UTF-8 encoding would be done at compile-time instead of run-time. You're correct that a fair comparison would be to UTF-8 encode the Strings as well. However, that's not what most users are going to do most of the time: when dealing with ASCII data, a straight Char8.pack encoding will do the same as UTF-8. I'm simply pointing out that I think Blaze should support this style. Michael ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
On Thu, May 27, 2010 at 10:23 AM, Michael Snoyman wrote: > On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic < > ivan.miljeno...@gmail.com> wrote: > >> Wow, I find it rather surprising that String out-performs Text; any >> idea why that is? I wonder if you're just using it wrong... >> >> Could be, I'd be very happy if that were the case. All of the benchmarks > are available on Github, and the bytestring[1], text[2] and string[3] > versions are all rather short. > Do you include the cost of encoding the result as e.g. UTF-8? The hope would be that the more compact Text would be faster to traverse, and thus encode, than the list based String. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
On Thu, May 27, 2010 at 10:48 AM, Jasper Van der Jeugt wrote: >> How about also providing an enumerator back-end? >> http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM >> >> Then your library can integrate more easily with the snap framework: >> http://snapframework.com > > Sure, I can do that. But I already tested integration with the snap > framework, the best path here seems to call the `writeLBS` function > from the snap framework on the `L.ByteString` that BlazeHtml produces > (`writeLBS` internally uses an enumerator). I think it's worth analyzing if using enumerators directly gives a significant performance improvement over converting from lazy ByteStrings. Looking a the conversion functions in the snap framework it looks like we can avoid some intermediate lists for one: writeLBS :: L.ByteString -> Snap () writeLBS s = addToOutput $ enumLBS s addToOutput :: (forall a . Enumerator a) -> Snap () addToOutput enum = modifyResponse $ modifyResponseBody (>. enum) enumLBS :: (Monad m) => L.ByteString -> Enumerator m a enumLBS lbs iter = foldM k iter enums where enums = map (enumPure1Chunk . WrapBS) $ L.toChunks lbs k i e = e i -- from iteratee: enumPure1Chunk :: (SC.StreamChunk s el, Monad m) => s el -> EnumeratorGM s el m a enumPure1Chunk str iter = runIter iter (Chunk str) >>= checkIfDone return Regards, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Announce : New haskell-llvm mailing list.
Hi all, I have set up a mailing list for discussion of haskell and LLVM related topics. All discussion on using Haskell with LLVM is relevant. That includes the haskell-llvm bindings on Hackage, custom LLVM bindings and directly generating LLVM IR code from haskell and passing that through the LLVM tools. In particular, this list is a place to share code, information, techniques and user experiences. The subscription page is here: http://projects.haskell.org/cgi-bin/mailman/listinfo/haskell-llvm Cheers, Erik -- -- Erik de Castro Lopo http://www.mega-nerd.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
Michael Snoyman writes: > * If you're standardizing on UTF-8, why not support bytestrings? +1 > I'm aware that a user could shoot him/herself in the foot by passing > in non-UTF8 data, but I would imagine the performance gains would outweigh > this. Wrap them in a (new)type? -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
Hey Bas, > How about also providing an enumerator back-end? > http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM > > Then your library can integrate more easily with the snap framework: > http://snapframework.com Sure, I can do that. But I already tested integration with the snap framework, the best path here seems to call the `writeLBS` function from the snap framework on the `L.ByteString` that BlazeHtml produces (`writeLBS` internally uses an enumerator). Kind regards, Jasper Van der Jeugt On Thu, May 27, 2010 at 10:38 AM, Bas van Dijk wrote: > Q14: Do you see any problems with respect to integrating BlazeHtml in > your favourite web-framework/server? > > How about also providing an enumerator back-end? > http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM > > Then your library can integrate more easily with the snap framework: > http://snapframework.com > > Regards, > > Bas > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
On Thu, May 27, 2010 at 11:40 AM, Ivan Miljenovic wrote: > On 27 May 2010 18:33, Michael Snoyman wrote: > > I don't do any string concatenation (look closely), I was very careful to > > avoid it. I tried with lazy text as well: it was slower. This isn't > > surprising, since lazy text- under the surface- is just a list of strict > > text. And the benchmark itself already has a lazy list of strict text. > Using > > lazy text would just be adding a layer of wrapping. > > I don't know what you mean by "explicitly using Text values"; you mean > > calling pack manually? That's really all that OverloadedStrings does. > > You can try out lots of different variants on that benchmark. I did that > > already, and found this to be the fastest version. > > Fair enough. Now that I think about it, I recall once trying to have > pretty generate Text values rather than String for graphviz (by using > fullRender, so it was still using String under the hood until it came > time to render) and it too was much slower than String (unfortunately, > I didn't record a patch with these changes so I can't just go back and > play with it anymore as I reverted them all :s). > > Maybe Bryan can chime in with some best-practices for using Text? > > Here's my guess at an explanation for what's happening in my benchmark: text will clearly beat String in memory usage, that's what it's designed for. However, the compiler is still generating String values which are being encoded to Text as runtime. Now, this is the same process for bytestrings. However, bytestrings never have to be decoded: the IO routines simply read the character buffer. In the case of text, however, the encoded data must be decoded again to a bytestring. In other words, here's what I think the three different benchmarks are really doing: * String: generates a list of Strings, passes each String to a relatively inefficient IO routine. * ByteString: encodes Strings one by one into ByteStrings, generates a list of these ByteStrings, and passes each ByteString to a very efficient IO routine. : Text: encodes Strings one by one into Texts, generates a list of these Texts, calls a UTF-8 decoding function to decode each Text into a ByteString, and passes each resulting ByteString to a very efficient IO routine. In the case of ASCII data to be output as UTF-8, uses the Data.ByteString.Char8.pack function will most likely always be the most efficient choice, and thus it seems like something BlazeHtml should support. I'm considering releasing a Hamlet 0.3 based entirely on UTF-8 encoded ByteStrings, but I'd also like to hear from Bryan about this. Michael ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
On 27 May 2010 18:33, Michael Snoyman wrote: > I don't do any string concatenation (look closely), I was very careful to > avoid it. I tried with lazy text as well: it was slower. This isn't > surprising, since lazy text- under the surface- is just a list of strict > text. And the benchmark itself already has a lazy list of strict text. Using > lazy text would just be adding a layer of wrapping. > I don't know what you mean by "explicitly using Text values"; you mean > calling pack manually? That's really all that OverloadedStrings does. > You can try out lots of different variants on that benchmark. I did that > already, and found this to be the fastest version. Fair enough. Now that I think about it, I recall once trying to have pretty generate Text values rather than String for graphviz (by using fullRender, so it was still using String under the hood until it came time to render) and it too was much slower than String (unfortunately, I didn't record a patch with these changes so I can't just go back and play with it anymore as I reverted them all :s). Maybe Bryan can chime in with some best-practices for using Text? -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
Q14: Do you see any problems with respect to integrating BlazeHtml in your favourite web-framework/server? How about also providing an enumerator back-end? http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM Then your library can integrate more easily with the snap framework: http://snapframework.com Regards, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
On Thu, May 27, 2010 at 11:28 AM, Ivan Miljenovic wrote: > On 27 May 2010 18:23, Michael Snoyman wrote: > > > > > > On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic > > wrote: > >> > >> On 27 May 2010 17:55, Michael Snoyman wrote: > >> > Two comments: > >> > * The exclamation point seems good enough for attributes. I copied > that > >> > for > >> > Hamlet as well. > >> > * If you're standardizing on UTF-8, why not support bytestrings? I'm > >> > aware > >> > that a user could shoot him/herself in the foot by passing in non-UTF8 > >> > data, > >> > but I would imagine the performance gains would outweigh this. My > recent > >> > benchmarks on the BigTable benchmark[1] imply a huge performance gap > >> > between > >> > ByteStrings and other contenders. > >> > >> Wow, I find it rather surprising that String out-performs Text; any > >> idea why that is? I wonder if you're just using it wrong... > >> > > Could be, I'd be very happy if that were the case. All of the benchmarks > are > > available on Github, and the bytestring[1], text[2] and string[3] > versions > > are all rather short. > > Does using lazy Text values improve this? I find it a little strange > that you concatenate so many individual Strings that much. Also, how > about explicitly using Text values rather than OverloadedStrings? > > I don't do any string concatenation (look closely), I was very careful to avoid it. I tried with lazy text as well: it was slower. This isn't surprising, since lazy text- under the surface- is just a list of strict text. And the benchmark itself already has a lazy list of strict text. Using lazy text would just be adding a layer of wrapping. I don't know what you mean by "explicitly using Text values"; you mean calling pack manually? That's really all that OverloadedStrings does. You can try out lots of different variants on that benchmark. I did that already, and found this to be the fastest version. Michael ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
On 27 May 2010 18:23, Michael Snoyman wrote: > > > On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic > wrote: >> >> On 27 May 2010 17:55, Michael Snoyman wrote: >> > Two comments: >> > * The exclamation point seems good enough for attributes. I copied that >> > for >> > Hamlet as well. >> > * If you're standardizing on UTF-8, why not support bytestrings? I'm >> > aware >> > that a user could shoot him/herself in the foot by passing in non-UTF8 >> > data, >> > but I would imagine the performance gains would outweigh this. My recent >> > benchmarks on the BigTable benchmark[1] imply a huge performance gap >> > between >> > ByteStrings and other contenders. >> >> Wow, I find it rather surprising that String out-performs Text; any >> idea why that is? I wonder if you're just using it wrong... >> > Could be, I'd be very happy if that were the case. All of the benchmarks are > available on Github, and the bytestring[1], text[2] and string[3] versions > are all rather short. Does using lazy Text values improve this? I find it a little strange that you concatenate so many individual Strings that much. Also, how about explicitly using Text values rather than OverloadedStrings? -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic wrote: > On 27 May 2010 17:55, Michael Snoyman wrote: > > Two comments: > > * The exclamation point seems good enough for attributes. I copied that > for > > Hamlet as well. > > * If you're standardizing on UTF-8, why not support bytestrings? I'm > aware > > that a user could shoot him/herself in the foot by passing in non-UTF8 > data, > > but I would imagine the performance gains would outweigh this. My recent > > benchmarks on the BigTable benchmark[1] imply a huge performance gap > between > > ByteStrings and other contenders. > > Wow, I find it rather surprising that String out-performs Text; any > idea why that is? I wonder if you're just using it wrong... > > Could be, I'd be very happy if that were the case. All of the benchmarks are available on Github, and the bytestring[1], text[2] and string[3] versions are all rather short. Michael [1] http://github.com/snoyberg/benchmarks/blob/master/bigtable/cgi/bytestring.hs [2] http://github.com/snoyberg/benchmarks/blob/master/bigtable/cgi/text.hs [3] http://github.com/snoyberg/benchmarks/blob/master/bigtable/cgi/string.hs ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Math questions
*Pete Chown and Dan Doel. Thank you for your solution. I actually It was not homework . It was just a a past exam question trying to answer . * **but your solution is very long , so I don't think he wants answer this long in the exams. I think this answer agree100 f g = map f xs == map g xs where xs = [1..100] from Richard O'Keefe is do the job. **Anyway , your solution help understand more about Haskell not only this question . Many thanks to you guys. On 27 May 2010 02:04, Dan Doel wrote: > On Wednesday 26 May 2010 5:38:57 pm Pete Chown wrote: > > test :: (Eq a) => (Int -> a) -> (Int -> a) -> Bool > > test f1 f2 = unsafePerformIO $ do > > goodSoFar <- newIORef True > > forLoop 1 100 $ \i -> > >when (f1 i /= f2 i) $ writeIORef goodSoFar False > > readIORef goodSoFar > > The problem with this algorithm is that it needlessly tests f1 against f2 > for > all i, even when a non-matching value has has already been found. Using the > power of call-with-current-continuation, I have constructed an algorithm > that > lacks this deficiency: > >import Control.Monad.Cont > >test f g = flip runCont id . callCC $ \escape -> > do forM_ [1..100] $ \n -> > when (f n /= g n) $ > escape False > return True > > This should perform almost 75% less work in the testFunc1 case! It > certainly > feels much snappier. > > -- Dan > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Mujtaba Ali Alboori ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
On 27 May 2010 17:55, Michael Snoyman wrote: > Two comments: > * The exclamation point seems good enough for attributes. I copied that for > Hamlet as well. > * If you're standardizing on UTF-8, why not support bytestrings? I'm aware > that a user could shoot him/herself in the foot by passing in non-UTF8 data, > but I would imagine the performance gains would outweigh this. My recent > benchmarks on the BigTable benchmark[1] imply a huge performance gap between > ByteStrings and other contenders. Wow, I find it rather surprising that String out-performs Text; any idea why that is? I wonder if you're just using it wrong... -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Gtk2hs-users] Problem when installing gtk2hs.
That might be it. However, I linked ~/.cabal/bin/* to /usr/local/bin And it worked. On Thu, May 27, 2010 at 3:24 PM, Ivan Miljenovic wrote: > On 27 May 2010 16:46, Magicloud Magiclouds > wrote: >> I only have one alex installed under ~/.cabal/bin. >> It seems working with shell environment, but not cabal. > > This sounds like a similar problem to one that occurred a couple of months > ago. > > If you use "~/.cabal/bin/" for your PATH variable, try replacing that > with "$HOME/.cabal/bin/". > >> >> On Thu, May 27, 2010 at 1:40 PM, Axel Simon wrote: >>> Hi Magicloud, >>> >>> On May 27, 2010, at 4:11, Magicloud Magiclouds wrote: >>> Hi, I have met similar problem before, and I do not know what to do. # cabal install --reinstall gtk2hs-buildtools Resolving dependencies... Configuring gtk2hs-buildtools-0.9... cabal: alex is required but it could not be found. cabal: Error: some packages failed to install: gtk2hs-buildtools-0.9 failed during the configure step. The exception was: ExitFailure 1 # alex -v Alex version 2.3.3, (c) 2003 Chris Dornan and Simon Marlow >>> >>> I don't think this is due to us. Are there perhaps other alex installations >>> on your path? Or in ~/.cabal/bin? >>> >>> Axel >>> >>> -- 竹密岂妨流水过 山高哪阻野云飞 -- ___ Gtk2hs-users mailing list gtk2hs-us...@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/gtk2hs-users >>> >>> >> >> >> >> -- >> 竹密岂妨流水过 >> 山高哪阻野云飞 >> ___ >> Haskell-Cafe mailing list >> Haskell-Cafe@haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> > > > > -- > Ivan Lazar Miljenovic > ivan.miljeno...@gmail.com > IvanMiljenovic.wordpress.com > -- 竹密岂妨流水过 山高哪阻野云飞 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC
Two comments: * The exclamation point seems good enough for attributes. I copied that for Hamlet as well. * If you're standardizing on UTF-8, why not support bytestrings? I'm aware that a user could shoot him/herself in the foot by passing in non-UTF8 data, but I would imagine the performance gains would outweigh this. My recent benchmarks on the BigTable benchmark[1] imply a huge performance gap between ByteStrings and other contenders. As we've discussed before, I think combining BlazeHtml and Hamlet would be very nice, though I'm dubious that a BlazeHtml backend for Hamlet would be faster than a raw backend. Looking forward to hearing more progress, good luck! Michael [1] http://www.snoyman.com/blog/entry/bigtable-benchmarks/ On Thu, May 27, 2010 at 10:16 AM, Jasper Van der Jeugt wrote: > Dear all, > > BlazeHtml started out on ZuriHac 2010. Now, Jasper Van der Jeugt is > working on it as a student to Google Summer of Code for haskell.org. > His mentors are Simon Meier and Johan Tibell. The goal is to create a > high-performance HTML generation library. > > In the past few weeks, we have been exploring the performance and > design of different drafts of this library. Now, the time has come to > ask some questions to the Haskell community — more specifically the > future users of BlazeHtml as well as current users of other HTML > generation libraries. > > We have written an RFC to gather feedback from the community: > > HTML version: http://jaspervdj.be/posts/2010-05-27-blazehtml-rfc.html > Plain version: > http://github.com/jaspervdj/BlazeHtml/raw/develop/doc/RFC.lhs > > The easiest way of sending us feedback, comments or criticism is > replying to the haskell-cafe thread here. Alternatively, drop a > comment at the bottom of the HTML version or at reddit. > > Looking forward to your feedback, > Kind regards, > Simon Meier > Jasper Van der Jeugt > ___ > 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] currying combinators
David Sankel wrote: keep :: ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b On Wed, May 26, 2010 at 12:49 PM, Lennart Augustsson wrote: There are no interesting (i.e. total) functions of that type. I wonder how one would prove that to be the case. I tried and didn't come up with anything. By parametricty, presumably. We must ultimately construct some value of type b, where b is universally quantified. Therefore, the only 'constructors' available for b are the ((t -> b) -> u -> b) and ((t1 -> t) -> b) arguments. However, since b is universally quantified, these arguments have no way of actually constructing some b, other than by returning bottom. Remember, if a language lacks typecase, (forall a. X -> a) is just another way of saying (X -> Void). -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Gtk2hs-users] Problem when installing gtk2hs.
On 27 May 2010 16:46, Magicloud Magiclouds wrote: > I only have one alex installed under ~/.cabal/bin. > It seems working with shell environment, but not cabal. This sounds like a similar problem to one that occurred a couple of months ago. If you use "~/.cabal/bin/" for your PATH variable, try replacing that with "$HOME/.cabal/bin/". > > On Thu, May 27, 2010 at 1:40 PM, Axel Simon wrote: >> Hi Magicloud, >> >> On May 27, 2010, at 4:11, Magicloud Magiclouds wrote: >> >>> Hi, I have met similar problem before, and I do not know what to do. >>> >>> # cabal install --reinstall gtk2hs-buildtools >>> Resolving dependencies... >>> Configuring gtk2hs-buildtools-0.9... >>> cabal: alex is required but it could not be found. >>> cabal: Error: some packages failed to install: >>> gtk2hs-buildtools-0.9 failed during the configure step. The exception was: >>> ExitFailure 1 >>> # alex -v >>> Alex version 2.3.3, (c) 2003 Chris Dornan and Simon Marlow >> >> I don't think this is due to us. Are there perhaps other alex installations >> on your path? Or in ~/.cabal/bin? >> >> Axel >> >> >>> -- >>> 竹密岂妨流水过 >>> 山高哪阻野云飞 >>> >>> >>> -- >>> >>> ___ >>> Gtk2hs-users mailing list >>> gtk2hs-us...@lists.sourceforge.net >>> https://lists.sourceforge.net/lists/listinfo/gtk2hs-users >> >> > > > > -- > 竹密岂妨流水过 > 山高哪阻野云飞 > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Google Summer of Code: BlazeHTML RFC
Dear all, BlazeHtml started out on ZuriHac 2010. Now, Jasper Van der Jeugt is working on it as a student to Google Summer of Code for haskell.org. His mentors are Simon Meier and Johan Tibell. The goal is to create a high-performance HTML generation library. In the past few weeks, we have been exploring the performance and design of different drafts of this library. Now, the time has come to ask some questions to the Haskell community — more specifically the future users of BlazeHtml as well as current users of other HTML generation libraries. We have written an RFC to gather feedback from the community: HTML version: http://jaspervdj.be/posts/2010-05-27-blazehtml-rfc.html Plain version: http://github.com/jaspervdj/BlazeHtml/raw/develop/doc/RFC.lhs The easiest way of sending us feedback, comments or criticism is replying to the haskell-cafe thread here. Alternatively, drop a comment at the bottom of the HTML version or at reddit. Looking forward to your feedback, Kind regards, Simon Meier Jasper Van der Jeugt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Gtk2hs-users] Problem when installing gtk2hs.
I only have one alex installed under ~/.cabal/bin. It seems working with shell environment, but not cabal. On Thu, May 27, 2010 at 1:40 PM, Axel Simon wrote: > Hi Magicloud, > > On May 27, 2010, at 4:11, Magicloud Magiclouds wrote: > >> Hi, I have met similar problem before, and I do not know what to do. >> >> # cabal install --reinstall gtk2hs-buildtools >> Resolving dependencies... >> Configuring gtk2hs-buildtools-0.9... >> cabal: alex is required but it could not be found. >> cabal: Error: some packages failed to install: >> gtk2hs-buildtools-0.9 failed during the configure step. The exception was: >> ExitFailure 1 >> # alex -v >> Alex version 2.3.3, (c) 2003 Chris Dornan and Simon Marlow > > I don't think this is due to us. Are there perhaps other alex installations > on your path? Or in ~/.cabal/bin? > > Axel > > >> -- >> 竹密岂妨流水过 >> 山高哪阻野云飞 >> >> >> -- >> >> ___ >> Gtk2hs-users mailing list >> gtk2hs-us...@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/gtk2hs-users > > -- 竹密岂妨流水过 山高哪阻野云飞 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell] Re: [Haskell-cafe] Work on Video Games in Haskell
writes: > Or maybe this would be a nice research topic: how to generate C code > that looks like it’s human written… Nah, that's too easy: just add a sprinkling of buffer overflows, undefined behavior, and off-by one index errors. -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
