- Haskell - Haskell.org

final test: Research Job in Compositional Reasoning and Analysis @ Heriot-Watt Univ., Scotland, UK
by Joe Wells 18 Oct '01

18 Oct '01

Research Position Useful Logics, Types, Rewriting, and their Automation (ULTRA) Group Computing and Electrical Engineering Department Heriot-Watt University Edinburgh, Scotland, UK Description of the Position A research position is available on an EC-funded project working under the supervision of Joe Wells. The position is in the ULTRA (Useful Logics, Types, Rewriting, and their Automation) group in the Department of Computing and Electrical Engineering at Heriot-Watt University in Edinburgh, the capital of Scotland. The work will be done in close coordination with the DART (Dynamic Assembly, Reconfiguration, and Type-checking) consortium (Genova Univ., HWU, Imperial Coll., and Torino Univ.) as well as the Church Project (Boston Coll., Boston Univ., Harvard Univ., HWU, Wellesley Coll., etc.). The researcher will probably help with some of the following tasks: * Designing new type systems for compositional (modular) analysis of systems that may involve one or more aspects of concurrency, mobility, modularity, objects, run-time code generation, etc. * Designing analysis algorithms for the new type systems. * Designing theories (e.g., "calculi") for reasoning about the meaning of dynamic software assembly, i.e., doing in a non-traditional order one or more of type checking, code generation, linking, loading, etc. * Making software systems incorporating the new type systems, algorithms, and calculi. * Writing scientific reports on the work done. The position is initially for 1 to 2 years, with extensions up to 3 years total possible depending on salary, experience, performance, and funding. Applications to spend a shorter period (e.g., the sabbatical leave of an established academic) will be considered, but the research area is pretty much predetermined. The salary will be commensurate with qualifications and experience in the range from 21290 GBP to 26229 GBP per year. It is preferred that the researcher will start in the period from 2002-01-01 to 2002-03-01. It is preferred that before starting the researcher will have completed a Ph.D. in a relevant discipline within Computer Science. Applicants from outside the European Economic Area (EEA) will be considered. The researcher will probably use some of the following knowledge areas: * Formal calculi for reasoning about the meaning of computer systems (including computer programs), especially those with aspects of (a) modules, linking, and loading, (b) concurrency, (c) mobility, (d) staged compilation, (e) objects, (f) resource usage, etc. * Analysis of systems represented in formal calculi. * Constraint solving and unification. * Type systems, especially those with intersection and union types. * Programming languages used for any of the above. Applying for the Position To formally apply for this position, please do the following before the closing date of 2001-11-02: * Arrange for 3 letters of reference to be sent as soon as possible. If (by mistake) someone tells you the letters are not needed yet, please have the letters sent anyway, because no one will be chosen for an interview until after we see the letters. See below for what we hope to see in a letter of reference. * Send the following yourself as soon as possible: + your complete curriculum vitae, + a brief statement (one paragraph is enough) explaining why you think your research accomplishments and interests would be a good match for the job, + web pointers to or paper copies of from 0 to 3 publications of yours which you think are relevant, and + contact details for the people writing your letters of reference. * Contact the Heriot-Watt Personnel Office and get them to send you an "application pack". This contains an application form, an equal opportunities monitoring form, information for applicants with disabilities, and some additional information about Heriot-Watt and the position. * Fill out and return the application form and the equal opportunities monitoring form. (If your curriculum vitae is well constructed, then some of the information requested on the application form will be redundant, in which case it is reasonable to just write "see c.v." in the blanks.) * Although not required, it will be appreciated if you inform Joe Wells as soon as possible that you are applying so that he knows to ask our personnel office for your application materials immediately after they arrive. * Anyone who might need a work permit if hired (usually someone who is not a citizen of an EEA country) should also do the following. In addition to possibly being e-mailed or faxed, each letter of reference should also be sent by post on official-looking stationery paper and should include details on your whereabouts over the last two years. A work permit application also needs copies of any degree certificates, so it is a good idea to send those also. Please include the reference code 133/01/L in all communications to help prevent your application from getting mixed up. Please convert Microsoft Word documents to a public, standard, and non-proprietary format, e.g., PDF, HTML, or PostScript. PDF is best, because some of our staff will encounter difficulties with HTML or PostScript. Please ask the people writing letters of reference for you to include details of: * the capacity in which they know you, * your skills, abilities and performance in relation to the post applied for, * your employment record including details of your role and service dates, * your record in terms of attendance, timeliness, and discipline, * their view of your suitability for the post as a whole, in light of the attached details and their knowledge of your experience and abilities, * any further relevant information which would assist us in making an appointment. Informal inquiries should be directed to Joe Wells at: web: http://www.cee.hw.ac.uk/~jbw/ e-mail: jbw(a)cee.hw.ac.uk fax: +44 131 449 3834 Formal applications and/or requests for materials for completing a formal application should be directed to the Heriot-Watt Personnel Office at: web: http://www.hw.ac.uk/personnel/ e-mail: personnel(a)hw.ac.uk voice mail: +44 131 451 3475 fax: +44 131 451 3475 minicom: +44 131 451 8212 post: The Personnel Office Lord Balerno Building Heriot-Watt University EDINBURGH EH14 4AS GREAT BRITAIN

1 0

Re: Haskell 98 - Standard Prelude - Floating Class
by Marcin 'Qrczak' Kowalczyk 18 Oct '01

18 Oct '01

Thu, 18 Oct 2001 13:49:11 +0200, Karl-Filip Faxen <kff(a)it.kth.se> pisze: > There are two solutions that I can see: Annotate classes in class > constraints with exactly which methods were used. Thus for the > expression "x+y" the inference algorithm would record the constraint > "Num{+} a" if x and y has type a in the type environment. Then if > an instance declaration for type Wurble omitted +, that instance > declaration would not allow us to simplify "Num{+} Wurble". This is equivalent to putting all methods in separate classes. IMHO missing method definitions should be detected where the instance is defined, not when it's used. You can still define diverging methods explicitly or manually split the class if you really want partial instances. -- __("< Marcin Kowalczyk * qrczak(a)knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

1 0

numbers game
by Graham Hutton 18 Oct '01

18 Oct '01

Dear all, The following new paper may be of interest to readers of this group: http://www.cs.nott.ac.uk/~gmh/countdown.pdf It shows how to develop a Haskell program to solve the numbers game from countdown, a popular quiz show on British television. The aim wasn't to produce solutions as fast as possible (although in absolute terms the program actually performs rather well), but rather to show how the program itself could be developed in systematic way in conjunction with a proof of its correctness. It's the kind of example that could be covered in one or two lectures as part of a Haskell course. Have fun! Graham p.s. The paper will appear as a functional pearl in JFP. +---------------------------------------------------------------------+ | Dr Graham Hutton Email : gmh(a)cs.nott.ac.uk | | Foundations of Programming Group Web : www.cs.nott.ac.uk/~gmh | | School of Computer Science and IT | | University of Nottingham | | Jubilee Campus, Wollaton Road | | Nottingham NG8 1BB | | United Kingdom | +---------------------------------------------------------------------+

1 0

proofs
by Richard 18 Oct '01

18 Oct '01

I want to learn how to go about proving things like (p >>= j) >= k == p >>= (\x->(j x >>= k)) where p >>= k = \s0 -> let (s1, a) = p s0 in k a s1 eg, verifying that the 3 monad laws hold for a specific monad. also, verifying the more numerous laws every arrow should obey. I could teach myself to do it clumsily, but I want to learn from others. would learning category theory help me do this? pointers to documents? proof-assistant software?

3 2

RE: Haskell 98 - Standard Prelude - Floating Class
by Simon Peyton-Jones 18 Oct '01

18 Oct '01

| > 1. Actually, I wouldn't even call that "default | definitions". These ARE | > definitions of sinh and cosh. | | Mathematically, yes. Numerically, no. Even if 'exp' is | implemented with high accuracy, the suggested defaults may | return a very inaccurate (in ulps) result. Take sinh near | zero. sinh(x) with x very close to 0 should return x. With | the above 'default' sinh(x) will return exactly 0 for a | relatively wide interval around 0, which is the wrong result | except for 0 itself. Indeed. The proposal is only to give "default declarations" in the class defn for sinh, cosh, and perhaps as Lennart suggests asinh, acosh, atanh. They give a reasonable first cut if you don't write definitions yourself. But you can overrride them at will. The only reason not to do this (which amounts to giving a default decl of "error") is if the default decl is so awful that it's badly misleading to provide it. Which doesn't look true in this case. I don't propose to change any of the actual instance declarations, because (as Lennart says) it's entirely possible that they have better numerical properties than the default declarations. Simon

5 4

Re: proofs
by Janis Voigtlaender 18 Oct '01

18 Oct '01

I wrote: > Rijk-Jan van Haaften writes: > > > I used 3 main properties for the process: > > ... > > 2. Lifting local let definitions to a higher level > > let > > f = > > let > > g = gExpr > > in > > fExpr > > in > > expr > > > > can be translated into > > ... > > Care has to be taken if g (which might be bound outside this let-block) occurs > in expr, because with the translated version it is now bound to gExpr. Renaming > helps (for some unused g'): > > let > > g' = gExpr > > f = fExpr[g <- g'] > > in > > expr Oops: let g' = gExpr[g <- g'] f = fExpr[g <- g'] in expr Hope, I got it right now. Janis. -- Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

1 0

Re: proofs
by Janis Voigtlaender 18 Oct '01

18 Oct '01

Rijk-Jan van Haaften writes: > I used 3 main properties for the process: > ... > 2. Lifting local let definitions to a higher level > let > f = > let > g = gExpr > in > fExpr > in > expr > > can be translated into > let > g = gExpr > f = fExpr > in > expr > > The definition of g which is local for f in the first > expression is made more global in the second > one. Care has to be taken if g (which might be bound outside this let-block) occurs in expr, because with the translated version it is now bound to gExpr. Renaming helps (for some unused g'): > let > g' = gExpr > f = fExpr[g <- g'] > in > expr -- Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

1 0

ANNOUNCE: linkchk-0.01 released
by Jens-Ulrik Petersen 18 Oct '01

18 Oct '01

Two months after the first release, linkchk version 0.01 is released! New in this version: * displays ping time instead of ok status * IPv6 support * command option to set delay between pings * uses netstat instead of /proc/net/route * uses popenhs * uses automake and autoconf The source and rpm files are available from: http://www.01.246.ne.jp/~juhp/haskell/linkchk/ Feedback, comments and code contributions appreciated, Jens

1 0

please add me
by lo janus 18 Oct '01

18 Oct '01

me(a)lojanus.com

1 0

Examples of some nice Haskell programs
by Andre W B Furtado 17 Oct '01

17 Oct '01

There are some nice examples (binaries) of [Haskell + HOpenGL] programs at: www.cin.ufpe.br/~haskell/hopengl/examples.html I think they may be of interest to the community because they confirm that it's really possible to use Haskell in the development of complex, fast and robust graphic applications and games that involve animation and other interesting issues (texturing, lighting, checking and analyzing multiple user inputs, etc.) -- Andre

1 0