Re[4]: [Haskell-cafe] idea for avoiding temporaries
Hello Claus, Monday, March 12, 2007, 3:35:43 AM, you wrote: the problems was mainly due to 2 factors: 1) readArray m (i,j) yes, indeed. since we are dealing in bulk operations, we might as well take advantage of that, so dropping the repeated bounds-checks inside the loops makes a lot of sense. no, i say here only about memory leaks. of course, unsafeRead omits bounds checking but more important in this case is that readArray created a temporary memory cells - index calculation of matrix turns out to be not strict. it was biggest surprise for me - i thrown a lot of time, adding 'seq' here and there before i even tried to replace this call with unsafeRead moral/note to self: bulk array operations are your friend (i knew that!-), but you need to use that when defining them (unsafeRead et al are only for library writers, but library writers ought to use them; and i was writing a small inlined library) switching array operations to unsafe ones raised performance, but, aside of this matrix indexing, don't changed memory usage 2) 'op' in 'l' which was passed as real closure and was not inlined due to weakness of ghc optimizer it irked me having to write the same loop twice, but i didn't consider the consequences. an INLINE pragma on l almost seems sufficient to regain the loss, so i prefer that; but writing out the loop twice is still a tiny tick faster.. afaik, ghc can't inline recursive functions. it will be great if ghc can automatically make specialized version of function it can't inline. so i'm wonder whether INLINE really helps anything? ... well, after conducting tests i see that INLINE works but manual inlining works even better :)) we should help strictness analyzer by marking all the variables used in tight loops as strict. ah, there were a few surprises in that one. i thought i had considered possible strictness problems, but obviously, i missed a few relevant possibilities. annotating everything is the the problem is that arrays also need to be annotated as strict. ghc is not as smart as you think so it really needs that everything will be annotated as strict in order to make strict calls (or may be you just don't take into account that haskell is lazy language and everything by default is lazy, that definitely don't help program to run faster :) safe option, and clearly documents the intentions, but i cannot help thinking about which annotations could be omitted: - modArray: a and i are both used anyway sure? they are just passed into the unsafeRead routine. whether they are *definitely* used or not depends on strictness of unsafeRead in these arguments - i index in loop is definitely checked (but j isn't, and some others weren't, either; so better safe than sorry) again, checking in the form of unless strictifies your operation only if we know that 'unless' is strict in its first argument. using guard makes i definitely strict (and in fact was used before 6.6 to declare parameters as strict): l i | in = f k | k `seq` True = ... - some of the parameters need not be annotated in this example, but should be if one wanted to reuse the code elsewhere - the one i really don't get yet is the one on the accumulators (!s in l, in dotA/matA); i thought i had covered that by using $! in applying the loop, but annotating the formal loop parameter, apart from being nicer, also seems faster.. it is a very different things! when you use $! in call, you ensure that parameter will be calculated *before* making actual call - otherwise, 'l' will be called with a closure that calculates actual value on demand. so this omits creating a closure and therefore conserves memory. it is all we need to make memory usage as small as possible but unfortunately, this don't changes a 'l' itself. it remains lazy in is argument, so our strict call will just add box around computed value before passing it to 'l' otoh, when ghc knows that 'l' is strict in its parameter (due to strictness analysis or with help of our annotation), it creates l', a strict version of l whose actual parameter has Int# type. all calls to 'l' just deboxify their parameter and call l'. of course, this means that your entire computation of new index/accumulator will be done using Int# values and result will be passed to l' without additional boxing and unboxing. you see a difference :))) moral/note to self: don't try to be clever, try to be clear..; strictness in formal parameters is better than strictness in actual parameters; bang-patterns are good;-) when i saw your code, i've thought that we should add more strictness to fix memory leaks and unsafe* to become a bit faster. memory leak on matrix read was surprise for me too after that is done, we got 1000 times less temporary data allocated and 5x faster execution. now it's a bit faster than strict lists is this now anywhere near what the number-crunchers use, when they use Haskell?-) it will be
[Haskell-cafe] Maybe and partial functions
The Maybe construction is very useful for explicitly handling circumstances where the function cannot produce a sensible answer. But how far should this notion be taken? When you're writing a function which you realise may not produce what you want, in what circumstances would you use a Maybe, and when would you just throw an error? I'm wondering both in terms of good engineering practise and also for correctness. Should elementary partial functions like 5 `div` 0 or head [] return Nothing? I guess it's a bit of a silly suggestion, but it helps to highlight why we use Maybe in the first place. So --- where's the cutoff point in your code? Cheers, D. -- Dougal Stanton ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A valuable new combinator for Parsec?
Hello all, While using the very nice option combinator of Parsec recently, it seemed to me that it would be useful to have a more specific kind of combinator for optional tokens that wraps the token into a Maybe type. So, that gives: pmaybe :: GenParser tok st a - GenParser tok st (Maybe a) pmaybe p = option Nothing (p = return . Just) I've been using it happily with some code of mine. Do people think that it would be generally useful to have in Parsec? Cheers, Maxime ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Performance Help
Hi I notice that there's not much user-accessible documentation of what you can expect GHC (or some other Haskell implementation) to do and not do with a given piece of code. Yhc/nhc/Hugs - nothing GHC - inlining, simplification, fusion if you use the build in functions in a specified way, strictness analysis, maybe some unboxing, let movement, some other tricks JHC - everything The problem is that things like strictness are a static analysis which is undecidable in general. Static analysis is probably too complex for the user to figure out what is going on, its much better to look at the Core generated and see what actually happened. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A valuable new combinator for Parsec?
On Mon, Mar 12, 2007 at 11:24:48AM +0100, Maxime Henrion wrote: While using the very nice option combinator of Parsec recently, it seemed to me that it would be useful to have a more specific kind of combinator for optional tokens that wraps the token into a Maybe type. So, that gives: pmaybe :: GenParser tok st a - GenParser tok st (Maybe a) pmaybe p = option Nothing (p = return . Just) I've been using it happily with some code of mine. Do people think that it would be generally useful to have in Parsec? Yes, it would certainly be useful. I think optional should work this way, but unfortunately it returns (). Pozdrawiam Tomek ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Maybe and partial functions
Hi head [] return Nothing? I guess it's a bit of a silly suggestion, but it helps to highlight why we use Maybe in the first place. So --- where's the cutoff point in your code? If that is what you want, then see my Safe library: http://www-users.cs.york.ac.uk/~ndm/projects/libraries.php#safe headMay :: [a] - Maybe a (note this function already exists and is called listToMaybe) However, I think that partial functions are just great, although a lot of people disagree with me. There are some tools being developed to check things like head []: Catch: http://www-users.cs.york.ac.uk/~ndm/projects/catch.php ESC/Haskell: http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps Catch also checks division by zero, explicit patterns etc. To see the world of pain you would be in if you go down the make everything total route, I suggest you try rewriting this program to be complete: http://darcs.haskell.org/nofib/imaginary/digits-of-e2/Main.lhs (if you do, please post the result to the list) If you ignore getArgs and read (which are incomplete in the above example), then Catch is able to prove all the remaining things complete, without annotations or code modifications. You might also want to try redoing that example in the type style, discussed here: http://www.haskell.org/haskellwiki/Non-empty_list Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re[4]: [Haskell-cafe] idea for avoiding temporaries
1) readArray m (i,j) yes, indeed. since we are dealing in bulk operations, we might as well take advantage of that, so dropping the repeated bounds-checks inside the loops makes a lot of sense. no, i say here only about memory leaks. of course, unsafeRead omits bounds checking but more important in this case is that readArray created a temporary memory cells - index calculation of matrix turns out to be not strict. it was biggest surprise for me - i thrown a lot of time, adding 'seq' here and there before i even tried to replace this call with unsafeRead i'm not so sure about that conclusion;) i admit that i more often optimise for time than for space, so unless there's a real space leak to get rid of, i tend to measure space performance indirectly, by its impact on time, which is perhaps not a good habit. but i did a step-by-step rerun of the modifications, to see their effect on (time) performance: time ./CG array 10: 33s time ./CG_Bulat array 10: 8s 33s: baseline, my original code 30 - strict formal pars in l, in dotA/matA 22 - inline l, for +*=/-*= 14 - replace readArray m (i,j) by unsafeRead m (index .. (i,j)), replace index by unsafeIndex, eliminating bounds-check 12 - same for readArray/writeArray v 12 - eliminating the tuple in readMatrix makes no difference 8 - seq-ing all parameters in l,*+=,dotA,matA to handle the 2d indexing, i replaced readArray m (i,j) by readMatrix m (i,j): {-# INLINE readMatrix #-} readMatrix m ij = unsafeRead m (unsafeIndex matrixBounds ij) matrixBounds :: ((Int,Int),(Int,Int)) matrixBounds = ((1,1),(n,n)) so we're still dealing with pairs, just got rid of the bounds-checks in readArray/index, and that alone brings us from 22s to 14s (12s if we do the same for vectors), a substantial improvement. eliminating the tuples, passing i and j directly into the computation, doesn't seem to make any further difference (shifting the indices to avoid the decrements might, but not by much, certainly not enough to justify extending the arrays;-), so just getting rid of the bounds-check had sufficiently exposed the index computation already. -- readMatrix m i j = unsafeRead m $! ((i-1)*n+(j-1)) ensuring strictness of all formal parameters in the basic vector/matrix operations, through bang-patterns or seq, brings us from 33s to 30s, and from 12s to 8s, so that helps a lot. the inline pragma on l brings us from 30s to 22s, so that helps a lot, too. afaik, ghc can't inline recursive functions. it will be great if ghc can automatically make specialized version of function it can't inline. so i'm wonder whether INLINE really helps anything? perhaps it can't unroll the (conceptually infinite) body of the loop, but it can bring copies of the definition to the places where the op parameters are known. (let f x = .. in f $! par) vs (let f !x = .. in f par) so the difference is between passing evaluated parameters into functions that don't expect them and passing parameters to functions that expect them evaluated. thanks, that makes sense to me: apart from the boxing/unboxing of evaluated parameters, the function body itself might look different. thanks, claus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re[4]: [Haskell-cafe] idea for avoiding temporaries
to handle the 2d indexing, i replaced readArray m (i,j) by readMatrix m (i,j): {-# INLINE readMatrix #-} readMatrix m ij = unsafeRead m (unsafeIndex matrixBounds ij) matrixBounds :: ((Int,Int),(Int,Int)) matrixBounds = ((1,1),(n,n)) i'm still trying to understand why unsafeIndex is so much faster than index. to prepare for further experiments, i tried to include the default implementation for method index in my source (which includes all the other optimisations discussed here), as myindex: {-# INLINE readMatrix #-} readMatrix m ij = unsafeRead m (index matrixBounds ij) myindex b i | inRange b i = unsafeIndex b i | otherwise = error Error in array index now, the measurement that confuses me is this: time ./CG array 10 readMatrix calls index: 16s readMatrix calls myindex: 9s so just calling an in-module copy of the default code for index, with bounds-check, is almost as fast as calling unsafeIndex, and almost twice as fast as calling the official index.. can anyone explain this effect? claus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[6]: [Haskell-cafe] idea for avoiding temporaries
Hello Claus, Monday, March 12, 2007, 6:03:28 PM, you wrote: readMatrix calls index: 16s readMatrix calls myindex: 9s so just calling an in-module copy of the default code for index, with bounds-check, is almost as fast as calling unsafeIndex, and almost twice as fast as calling the official index.. moreover, look at +RTS -s results. i'm pretty sure that you will find huge difference in memory allocation :) -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Type and State Confusion
Albert, Thanks very much for your explanation. I see now that I confused the state function with the f, but it's still not quite clear. data MyState a b = MyStateC ([a] - ([a], b)) This defines an algebraic data type (...why is it called algebraic?) with two type variables and a unary constructor. instance Monad (MyState a) where return x = MyStateC (\tb - (tb, x)) (MyStateC st) = f = MyStateC (\tb - let (newtb, y) = st tb (MyStateC trans) = f y in trans newtb ) Now, if the instantiated a has type String, Int or whatever, I would understand, but the type of the Monad seems to be built up from two types. You write: ...y has type String. In more detail: in order for foo = toMyState to make sense, these must be the types: foo :: MyState String String st :: [String] - ([String], String) y is forced to have type String for the sake of toMyState. But how do the two occurrences of String in the foo type, in general a and b, match to the single a in the instance declaration? In particular when I have: toMyState :: String - MyState String Int toMyState x = MyStateC (f x) This is mapped onto a list of strings, on which the Prelude sequence is applied. sequence :: Monad m = [m a] - m [a] You write: The = used by sequence is the same = in the MyState monad, since you instantiate m to MyState String. Therefore, sequence performs all the state transformations correctly, since = is correct. So the m becomes MyState String, and therefore the list elements have type (MyState String Int), or the other way around. I understand, from your explanation, how this works from there on, but I'm still confused about what the Monad is. Is it MyState which takes two types, or (MyState String) which takes one type? Or neither? Does it involve some 'sort of currying' of type parameters? Thanks again, Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Maybe and partial functions
On Mon, 12 Mar 2007 11:37:43 + Neil Mitchell [EMAIL PROTECTED] wrote: Catch also checks division by zero, explicit patterns etc. To see the world of pain you would be in if you go down the make everything total route, I suggest you try rewriting this program to be complete: http://darcs.haskell.org/nofib/imaginary/digits-of-e2/Main.lhs (if you do, please post the result to the list) Isn't this just an example of needing to separate data and codata, and so totality and productiveness in order to be productive in a total language? Gen signature.asc Description: PGP signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A valuable new combinator for Parsec?
At Mon, 12 Mar 2007 11:24:48 +0100, Maxime Henrion wrote: pmaybe :: GenParser tok st a - GenParser tok st (Maybe a) pmaybe p = option Nothing (p = return . Just) I've been using it happily with some code of mine. Do people think that it would be generally useful to have in Parsec? I believe I have written that same combinator a few times myself, so I vote yes. j. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] CFP: Prog. Lang for Mechanized Mathematics Workshop
Programming Languages for Mechanized Mathematics Workshop As part of Calculemus 2007 http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/ Hagenberg, Austria [http://www.cas.mcmaster.ca/plmms07/] The intent of this workshop is to examine more closely the intersection between programming languages and mechanized mathematics systems (MMS). By MMS, we understand computer algebra systems (CAS), [automated] theorem provers (TP/ATP), all heading towards the development of fully unified systems (the MMS), sometimes also called universal mathematical assistant systems (MAS) (see Calculemus 2007 http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/). There are various ways in which these two subjects of /programming languages/ and /systems for mathematics/ meet: * Many systems for mathematics contain a dedicated programming language. For instance, most computer algebra systems contain a dedicated language (and are frequently built in that same language); some proof assistants (like the Ltac language for Coq) also have an embedded programming language. Note that in many instances this language captures only algorithmic content, and /declarative/ or /representational/ issues are avoided. * The /mathematical languages/ of many systems for mathematics are very close to a functional programming language. For instance the language of ACL2 is just Lisp, and the language of Coq is very close to Haskell. But even the mathematical language of the HOL system can be used as a functional programming language that is very close to ML and Haskell. On the other hand, these languages also contain very rich specification capabilities, which are rarely available in most computation-oriented programming languages. And even then, many specification languages ((B, Z, Maude, OBJ3, CASL, etc) can still teach MMSes a trick or two regarding representational power. * Conversely, functional programming languages have been getting more mathematical all the time. For instance, they seem to have discovered the value of dependent types rather recently. But they are still not quite ready to 'host' mathematics (the non-success of docon http://www.haskell.org/docon/ being typical). There are some promising languages on the horizon (Epigram http://www.e-pig.org/, Omega http://web.cecs.pdx.edu/%7Esheard/Omega/index.html) as well as some hybrid systems (Agda http://agda.sourceforge.net/, Focal http://focal.inria.fr/site/index.php), although it is unclear if they are truly capable of expressing the full range of ideas present in mathematics. * Systems for mathematics are used to prove programs correct. (One method is to generate correctness conditions from a program that has been annotated in the style of Hoare logic and then prove those conditions in a proof assistant.) An interesting question is what improvements are needed for this both on the side of the mathematical systems and on the side of the programming languages. We are interested in all these issues. We hope that a certain synergy will develop between those issues by having them explored in parallel. These issues have a very colourful history. Many programming language innovations first appeared in either CASes or Proof Assistants, before migrating towards more mainstream languages. One can cite (in no particular order) type inference, dependent types, generics, term-rewriting, first-class types, first-class expressions, first-class modules, code extraction, and so on. However, a number of these innovations were never aggressively pursued by system builders, letting them instead be developped (slowly) by programming language researchers. Some, like type inference and generics have flourished. Others, like first-class types and first-class expressions, are not seemingly being researched by anyone. We want to critically examine what has worked, and what has not. Why are all the current ``popular'' computer algebra systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical CAS? But also look at question like what forms of polymorphism exists in mathematics? What forms of dependent types exist in mathematics? How can MMS regain the upper hand on issues of 'genericity'? What are the biggest barriers to using a more mainstream language as a host language for a CAS or an ATP? This workshop will accept two kinds of submissions: full research papers as well as position papers. Research papers should be nore more than 15 pages in length, and positions papers no more than 3 pages. Submission will be through _EasyChair_. An informal version of the proceedings will be available at the workshop, with a more formal version to appear later. We are looking into having the best papers completed into full papers and published as
[Haskell-cafe] Re: ANN: HSH 1.2.0
On 2007-03-06, Simon Marlow [EMAIL PROTECTED] wrote: John Goerzen wrote: possible to create a pipe going directly from program A to program B. You certainly can pipe directly from one process to another: That only works for 2 processes. What if I have 4 processes, and want to pipe from one to the next, all along, as in ls -l /tmp | tr a-zA-Z | sort | md5sum to give a contrived example -- John ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: idea for avoiding temporaries
On Fri, Mar 09, 2007 at 10:24:14AM +, Simon Marlow wrote: GHC doesn't have any kind of uniqueness analysis right now. It's pretty hard to do in general: imagine a function that takes an array as an argument and delivers an array as a result. It'll probably need two versions: one when the argument is unique, one for when it's not. If you can see all the call sites you might be able to throw away one of these versions, but with separate compilation that's the uncommon case. Ah, yes. I keep on thinking this is used since I studied it carefully as a potential algorithm for jhc... (still undecided, my implementation is too buggy to use in production and jhc has enough bugs as is :) ) http://citeseer.ist.psu.edu/wansbrough98once.html BTW, we don't do any update-avoidance at the moment. The old update analyser was slow and didn't give any significant benefit, so we dropped it. I find a general problem when researching ghc is that a lot of past research projects used it as a base and declare things like 'we integrated this into the ghc 4.04 haskell compiler' but it is not clear whether the code actually made it back into the mainline or not.. Perhaps A section of the wiki is in order that lists the most recent paper that describes various parts of what is actually used in the production ghc. perhaps something like type checker : boxy types and impredicativity paper + Wobbly type GADT inference paper optimizer/simplifier : secrets of haskell inliner paper runtime: eval/apply vs push-enter paper garbage collector: non-stop collection for haskell paper fundep implementation: ? concurrency: STM papers + original concurrency paper (are these accurate BTW?) John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: idea for avoiding temporaries
On Mon, Mar 12, 2007 at 05:21:46PM -0700, John Meacham wrote: type checker : boxy types and impredicativity paper + Wobbly type GADT inference paper Both of those seem to take basic Hindley-Damas-Milner as a prerequisite ... While I've invented two closely related typechecking algorithms, and I'm pretty sure they're both close relatives of HDM, I can't seem to find a readable paper explaining the real HDM algorithm. A pointer to that would be very useful. Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: HS-Plugins 1.0 chokes on simple test, WinXP GHC-6.6
I'm running cygwin on WinXP and got a different failure (below) from the latest darcs hs-plugins. Line 11 is right after the TOP definition. Does anyone have a theory about what's going on here? - Conal looks like the TOP and GHC_LIB_PATH values are the output of external commands, such as ghc --print-libdir, and someone forgot to remove the linefeeds from the output before inserting it in the script? Recent versions of cygwin bash do not by default handle DOS/Windows-style line endings well. See any recent bash release notice on cygwin-announce for details, but here are the juicy bits. According to Eric Blake volunteer cygwin bash maintainer quote 4. This version of bash has a cygwin-specific shell option, named igncr to force bash to ignore \r, independently of cygwin's mount style. As of bash- 3.2.3-5, it controls regular scripts, command substitution, and sourced files. I hope to convince the upstream bash maintainer to accept this patch into the future bash 4.0 even on Linux, rather than keeping it a cygwin-specific patch, but only time will tell. There are several ways to activate this option: 4a. For a single affected script, add this line just after the she-bang: (set -o igncr) 2/dev/null set -o igncr; # comment is needed 4b. For a single script, invoke bash explicitly with the shopt, as in 'bash -o igncr ./myscript' rather than the simpler './myscript'. 4c. To affect all scripts, export the environment variable BASH_ENV, pointing to a file that sets the shell option as desired. Bash will source this file on startup for every script. 4d. Added in the bash-3.2-2 release: export the environment variable SHELLOPTS with igncr included in it. It is read-only from within bash, but you can set it before invoking bash; once in bash, it auto-tracks the current state of 'set -o igncr'. If exported, then all bash child processes inherit the same option settings; with the exception added in 3.2.9-11 that certain interactive options are not inherited in non-interactive use. 5. You can also experiment with the IFS variable for controlling how bash will treat \r during variable expansion. /quote -- Iain Alexander [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] idea for avoiding temporaries
On Fri, Mar 09, 2007 at 10:58:43AM -0500, Jan-Willem Maessen wrote: * Linear or Uniqueness types are almost what we want. I think Josef Svenningson was the one who captured this the best: Uniqueness type *require* that the *caller* of these routines make sure that it is not sharing the data. So we need two copies of our linear algebra library---one which takes unique arrays as arguments and updates in place, and one which takes non-unique arrays and allocates. And we have to pick the right one based on context. What we want, it seems to me, is one library and a compiler which can make informed judgments. wansbrough's simple usage polymorphism paper details an analysis that infers types that are 'polymorphic' in their usage qualities. The paper brings up the possibility of generating specialized versions of functions 'usage-specialization' based on these types. which seems to be exactly the sort of thing you would want out of a compiler for the above. http://citeseer.ist.psu.edu/292462.html it would also seem like it would be possible to actually pass these usage types at run-time and choose operations based on that. This seems like it would be an ideal way to go, it would behave in a very predictable way for haskell programmers used to type specialization and haskell classes and the middle-end work wouldn't be as much as system f is already typed and these usage types would behave like other type variables in a lot of ways after their initial inference. usage specialization could occur via the same RULES mechanism that type specialization uses now... I'd love to hear if anyone has insights / pointers to related work on any of the issues above; I'm especially keen to learn if there's work I didn't know about on fusion of multiple traversals. In my day job with Fortress we are looking at RULES-like approaches, but they founder quickly because the kind of problems David is trying to solve are 90% of what our programmers want to do. I think the simple usage polymorphism paper (and the thesis that goes along with it) can provide some fertile ideas for exploration here.. John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church Encoding Function
On 3/10/07, Robert Dockins [EMAIL PROTECTED] wrote: I'm pretty sure you can define a catamorphism for any regular algebraic data type. I'm not 100% sure what the story is for non-regular (AKA nested) datatypes. They do exist: Initial Algebra Semantics is Enough! Patricia Johann and Neil Ghani. http://crab.rutgers.edu/~pjohann/tlca07.pdf code: http://www.cs.nott.ac.uk/~nxg/Tlca07.hs Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell for Accessibility
Tom Hawkins wrote: I love programming in Haskell, yet even its concise expressions have not saved my tendons from chronic RSI. Has anyone put any thought into building an accessible Haskell development interface for those who may not be able to use a keyboard? One inspirational program is Dasher (http://www.inference.phy.cam.ac.uk/dasher/). Not only is it godsend for people with a wide range of disabilities, Dasher is also a lot of fun to use. Though Dasher is good at general text entry, it's not well suited for programming. However, combining Dasher's statistical inference with Haskell's type inference might yield a graphical, cursor driven interface even more efficient than the conventional keyboard. I've suggested before (http://lambda-the-ultimate.org/node/1354#comment-15935) that Dasher should be able to be hacked into something that is extremely effective for code. Simply using the BNF as generating (rather than matching) the syntax should make it extremely effective and should be rather easy to add to Dasher. Adding things like type-based disambiguation, smart identifier lookup and other such features from normal typing IDEs would be more involved but increase throughput even more. I can see such an interface approaching or even possibly exceeding the speed of typing code. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type and State Confusion
Hans van Thiel wrote: sequence :: Monad m = [m a] - m [a] You write: The = used by sequence is the same = in the MyState monad, since you instantiate m to MyState String. Therefore, sequence performs all the state transformations correctly, since = is correct. So the m becomes MyState String, and therefore the list elements have type (MyState String Int), or the other way around. I understand, from your explanation, how this works from there on, but I'm still confused about what the Monad is. Is it MyState which takes two types, or (MyState String) which takes one type? Or neither? Does it involve some 'sort of currying' of type parameters? The monad is (MyState String) or generally (MyState a) which takes one type. So this is some sort of currying of type parameters. With this in mind, the rest is straightforward: data MyState a b = MyStateC ([a] - ([a], b)) This defines an algebraic data type (...why is it called algebraic?) with two type variables and a unary constructor. instance Monad (MyState a) where return x = MyStateC (\tb - (tb, x)) (MyStateC st) = f = MyStateC (\tb - let (newtb, y) = st tb (MyStateC trans) = f y in trans newtb ) Now, if the instantiated a has type String, Int or whatever, I would understand, but the type of the Monad seems to be built up from two types. The general type of return is return :: (Monad m) = b - m b Tailor-made to our case, m = MyState a, return :: b - MyState a b Similarly, the general type of = is (=) :: (Monad m) = m b - (b - m c) - m c Tailor-made to our case, m = MyState a, (=) :: MyState a b - (b - MyState a c) - MyState a c If we now consider foo = toMyState then a=String, b=String, c=Int. Note again that the part (MyState a), or now (MyState String), is the monad. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Maybe and partial functions
Dougal Stanton wrote: The Maybe construction is very useful for explicitly handling circumstances where the function cannot produce a sensible answer. But how far should this notion be taken? When you're writing a function which you realise may not produce what you want, in what circumstances would you use a Maybe, and when would you just throw an error? It seems that if I cannot foresee how the function will be used, I need to be very general. Following the convention of Data.Map.lookup, I will use a Monad or MonadZero or MonadError. Perhaps even an ArrowZero. Every function is used in two circumstances. One circumstance is front-line code, where nobody is trusted and every invalid call is caught and handled. This is best done as above. Another circumstance is core code, where all data have been screened by the front-line code and there is no point repeating checks and handlers again and again and again. (How many times do you have to re-validate data? Take it to the extreme: If the code binds [0] to xs, do you have to check not (null xs) every alternate line of code? Every extra check and its associated Maybe or Monad type clutters up code, and after a threshold introduces risk of logical errors rather than reduces risk of data errors.) For core code, I may provide an unchecked version of my function, in case just use the identity monad is easier said than done. (It may still throw an error, if it is impossible to avoid a check linguistically, e.g., pattern matching, but at least there is no clutter from handlers or extra types, e.g., head, foldr1, etc.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Church Encoding Function
Joachim Breitner wrote: Hi, Am Samstag, den 10.03.2007, 14:52 -0500 schrieb Stefan Monnier: I'm pretty sure you can define a catamorphism for any regular algebraic data type. Actually, so-called negative occurrences in (regular) data types cause problems. Try to define the catamorphism of data Exp = Num Int | Lam (Exp - Exp) | App Exp Exp to see the problem, I guess Robert is still true as this Exp contains a non-algebraic type ((-)), therefore is not a regular algebraic type. (Based on an assumed meaning of “algebraic data type”). But let’s see... Am I right to assume that I have found a catamorphism if and only if the that function, applied to the data type constructors (in the right order) gives me the identity on this data type? maybe Nothing Just == id :: Maybe - Maybe \b - if b then True else False == id :: Bool - Bool foldr (:) []== id :: [a] - [a] uncurry (,) == id :: (a,b) - (a,b) either Left Right == id :: Either a b - Either a b Does that also mean that catamorphism for a given type are unique (besides argument re-ordering)? Now some brainstorming about the above Exp. I guess we want: exp Num Lam App e == id e therefore exp :: (Int - Exp) ((Exp - Exp) - Exp) (Exp - Exp - Exp) Exp now we want the return type to not matter exp :: forall b. (Int - b) ((Exp - Exp) - b) (Exp - Exp - b) Exp So my guess would be: exp f _ _ (Num i) = f i exp _ f _ (Lam g) = f g exp _ _ f (App e1 e2) = f e1 e2 Looks a bit stupid, but seems to work, especially as there is not much a function with type (Exp - Exp) - b can do, at least on it’s own. Is that a catamorphism? Greetings, Joachim Catamorphisms, folds, are the mediating arrows of initial algebras and thus are unique. I believe those equations combined with the free theorem that such functions would have, do guarantee that it would be that arrow. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe