- Haskell - Haskell.org

Re: [Haskell] Re: Re: RE: Extensible records: Static duck typing
by Andrzej Jaworski 22 Feb '08

22 Feb '08

Johannes Waldmann <waldmann(a)imn.htwk-leipzig.de> has asked me to clarify my claims here. But I say: why not to ask Chris Okasaki himself? Manuel Chakravarty has recently published this: http://www.cse.unsw.edu.au/~chak/papers/WC07.html so he might take the question too. >From my perspective there are too many language extension proposals like Generic Haskell addressing deriving extensions, Named Instances (http://www.cs.uni-bonn.de/~ralf/hw2001/4.pdf ) and many other I do not care to remember. To my mathematical mind Functor should be made a superclass of Monad before any such extensions were considered. This however costs almost a Ferrari :-) Exactly a Porsche: http://research.microsoft.com/~simonpj/papers/haskell-retrospective/Haskell… pages 62 - 64. Regards, -Andrzej Jaworski

1 0

Extensible records: Static duck typing
by Bulat Ziganshin 22 Feb '08

22 Feb '08

Hello haskell, the principle of duck typing used in dynamic OOP languages such as Ruby and Python, is simple: if some object supports Quack method, then it can be passed to any routine that expects an object of some Duck type this principle allows to build programs in quick and easy way: we just add to objects implementations of all the methods required: e = new Entry {label := "Hi", color := blue, getValue := getEntryValue, setValue := setEntryValue} e.display -- uses color/label properties e.saveToFile -- uses getValue property of course, drawback of duck typing that when we forgot to setup some field, this will be detected only at runtime - as usual for dynamic typing Haskell can provide benefits of both static and duck typing with type inference by means of extensible records. type of 'e' in this case will be {Entry | getValue::IO String, setValue::String->IO()}, i.e. Entry record type extended with getValue/setValue fields. serialization function may look like this: saveToFile x = writeToFile "data" (show x.getValue) and its implementation infers its type: saveToFile :: {...| getValue::(Show a) => a->IO() } -> IO () where {...| getValue::a} means "any record type which includes getValue field of type a". type of our 'e' conforms to this type signature, so `e` can be passed to saveToFile in safe manner and this is completely checked at compile time without any explicitly written type signatures this becomes even more important when we want to create objects belonging to more than one object hierarchy. by requiring that each possible property should be explicitly declared, we may ensure that properties used in different modules can't be mixed up: module A: property getValue module B: property getValue module C: import A; import B -- conflict: from where getValue should be imported? it may be interesting to compare extensible records with OOP and type classes approaches - it seems that e.r. is just like type class instances created "at the place" and linked to the concrete object rather than whole type so, implementation of extensible records in haskell compilers would allow to 1) give us simple, natural way to make bindings to various OOP libraries. i've seen bindings in gtk2hs/wxHaskell and now they use a lot of type hackery 2) compete with dynamic OOP languages in the areas of scripting, fast prototyping, web programming and even make possible to use the same techniques in larger apps, again increasing programmers productivity also, extensible records may be useful for merging haskell into jvm/.net world - as a way to provide haskell access to their OOP libs ps: there are many papers on adding extensible records to Haskell, in particular you can read http://research.microsoft.com/Users/simonpj/Papers/recpro.ps.gz -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

14 34

alsa-midi, midi, event-list, non-negative
by Henning Thielemann 21 Feb '08

21 Feb '08

Last autumn I found the 'alsa-midi' package by Soenke Hahn for controlling digital music instruments over MIDI and I wanted to avoid duplicate MIDI definitions. Thus I started extracting MIDI code from the Haskore project. Months later I ended up with some more packages: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/alsa-midi This is a simple interface to the sequencer part of ALSA (Advanced Linux Sound Architecture) It lets you control and communicate with external music synthesizers via MIDI. However with its release it becomes deprecated because I recently became aware of the more complete approach http://code.haskell.org/alsa/ which we should merge with, I think. The library is built on top of http://hackage.haskell.org/cgi-bin/hackage-scripts/package/midi which provides definitions of MIDI events and MIDI streams and reading and writing MIDI files. This in turn is built on top of http://hackage.haskell.org/cgi-bin/hackage-scripts/package/event-list which provides data structures for lists containing events and a time stamp. Pauses before the first and after the last event are supported. The data structures can be used to represent MIDI files, OpenSoundControl message streams, music performances or other streams of temporal events. Internally it uses lists of elements of alternating types, that is [b,a,b,...,a,b] or [a,b,a,...,a,b]. These data structures could be useful of its own, but are not exposed so far. This is eventually built on top of http://hackage.haskell.org/cgi-bin/hackage-scripts/package/non-negative which provides a class for non-negative numbers, a wrapper which can turn any ordered numeric type into a member of that class, and a lazy number type for non-negative numbers (a generalization of Peano numbers). You may also want to check if the experimental version of http://hackage.haskell.org/cgi-bin/hackage-scripts/package/jack is useful for you. Happy installation!

1 0

*** JOB OFFER *** related to realtime 3D graphics, animation and reactive content
by Peter Verswyvelen 21 Feb '08

21 Feb '08

<http://www.anygma.com/> Anygma is a startup company focusing on generating easy-to-use tools for creating audio-visual 2D/3D content, in the area of entertainment, media, corporate communication and the internet. <http://www.anygma.com/> Anygma has recently raised new capital in order to fund the development of a new platform targeted towards artists and designers for generating procedural and reactive geometry, animations and games. We are looking for talented and passionate computer scientists and software engineers to help us design and implement a prototype of this platform. If you are interested in applying Haskell, OpenGL, and some C/C++, to create such a platform, feel free to apply for the job by sending an email to <mailto://peter%3CAT%3Enazooka%3CDOT%3Ecom> peter AT nazooka DOT com. More information about the job offer can be found <http://www.anygma.com/JobOfferA.html> here. Thank you, Peter Verswyvelen, Software Architect, www.anygma.com <http://www.anygma.com/> PS: This job offer was already placed in the Haskell Café a while ago, but I was advised there to place it in the main Haskell list. I hope this is not considered as spam.

1 0

CFP: Continuation Fest 2008
by oleg＠okmij.org 20 Feb '08

20 Feb '08

Call for Talk Proposals Continuation Fest 2008 April 13, Tokyo, Japan http://logic.cs.tsukuba.ac.jp/~kam/Continuation2008/ Continuations are used, and constantly re-discovered, in web programming, logic, event-based concurrency, linguistics, transactional systems, optimization, program generation and verification. Programming language systems -- including Scheme, OCaml, Ruby, Python, Haskell, Coq -- are (re-)implementing continuations, generators, iterators and related control structures. Continuations are also being studied for their own sake. We call for an informal gathering of people working in all these areas -- language designers, users, and researchers who study or use continuations in academic or practical work or as a hobby. The goal is to exchange ideas, terminology, new results, experience reports, works in progress, open problems, and friendly feedback -- as well as meet each other and strengthen the community. We plan a combination of 7-8 broadly accessible talks and 1-2 invited talks, with plenty of breaks for socializing and informal conversations. An evening event is planned. Participants are invited to submit working notes, source files, and abstracts for distribution to the attendees, but as the workshop has no formal proceedings, contributions may still be submitted for publication elsewhere. We solicit talk proposals, about 2 paragraphs long. The proposal should include the desired talk duration and be emailed to CF2008(a)logic.cs.tsukuba.ac.jp The proposals will be evaluated by the Program Committee, who also would advise the authors on the duration of the talk and on making it as accessible as possible. The topics of interest include, but are not at all limited to: -- descriptions of uses of continuations in program generation, linguistics, proof theory, model checking, -- system demonstrations -- libraries using continuations, such as generators -- verifying programs that use continuations explicitly or implicitly (exceptions, concurrency, backtracking) -- type systems of continuations and their formalizations -- open problems Important dates: March 31, 2008: The deadline for the talk proposals April 13, 2008: The Fest Program committee: Chris Barker (New York) Shiro Kawai (Scheme Arts) Oleg Kiselyov (FNMOC) Chung-chieh Shan (Chair, Rutgers) Taiichi Yuasa (Kyoto) Organizing Committee: Kenichi Asai (Ochanomizu) Yukiyoshi Kameyama (Chair, Tsukuba) Inquiries: CF2008(a)logic.cs.tsukuba.ac.jp

1 0

Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
by Wolfgang Jeltsch 19 Feb '08

19 Feb '08

Am Dienstag, 19. Februar 2008 21:44 schrieben Sie: > * Support of type-level Booleans (Wolfgang?) Attached is just a quickly hacked Boolean module. Nothing very special. I’d be happy if you could prettify this (choose better names, add documentation, etc.). Thanks for any effort. Best wishes, Wolfgang

1 1

Funded PhD studentships at the University Of Kent
by S.J.Thompson 18 Feb '08

18 Feb '08

Funding is available for the following PhD studentships within the TCS group at the University of Kent. Applicants should contact the project supervisor directly for further details. Project Supervisor: Dr Olaf Chitil (O.Chitil(a)kent.ac.uk) Project Title: Tracing Functional Programs with Hat Hat (www.haskell.org/hat) is a sophisticated tool for locating faults in Haskell programs. Hat consists of a trace generation system plus various tools for viewing a trace. The aim of the research project is to improve Hat by both extending it and easing its application in practise: (1) Apply several theoretical results of a recent EPSRC project on tracing in Hat (e.g. algorithmic debugging with functions as finite maps). (2) Integrate the trace generator of Hat into the byte code interpreter of the Glasgow Haskell system (GHC). (3) Enable traced code to call and be called from unmodified non-tracing code, such that Hat can use pre-compiled libraries of GHC. Project Title: The Essence of Transfinite Reductions Project Supervisor: Dr Stefan Kahrs (S.M.Kahrs(a)kent.ac.uk) Infinitary Rewriting is an area of Term Rewriting in which research has studied infinitary terms and infinitary reductions. While the notion of infinitary terms is fairly settled, the existing notions of infinitary reduction leave a lot to be desired - the definitions are suspiciously complicated, the established results less than impressive. Thus, there appears to be a lot of room for improvement. There are different angles that are worth exploring. Firstly, there are several alternative ways to define transfinite reductions. Secondly, one would hope that some of these alternative ways lead to good properties of transfinite reduction. Thirdly, it is not even a priori clear what would constitute such a good property. Project Title: Refactoring Proofs Project Supervisor: Prof Simon Thompson (S.J.Thompson(a)kent.ac.uk) Refactoring allows the programmer to modify the design or structure of a program without changing its behaviour. Recent work in the Functional Programming group at Kent has developed refactoring systems for Haskell 98 (HaRe) and Erlang (Wrangler). Programming and proof have much in common, and indeed under the "propositions as types" analogy, they are different views of the same objects. The aim of this project is to explore how refactoring can be incorporated into proof development systems, and will combine theoretical work, implementation and usability analysis to ensure that the results will be of value to users of proof assistants. The aim of this project is to investigate refactoring for proofs.

1 0

Cfp: 3rd Int'l Workshop on Security and Rewriting Techniques Security (SecReT 2008)
by Santiago Escobar 18 Feb '08

18 Feb '08

******************************************************************** SecReT 2008 3rd International Workshop on Security and Rewriting Techniques http://www.dsic.upv.es/workshops/secret08 Sunday, June 22, 2008, Pittsburgh, USA Affiliated workshop of the 21st IEEE Computer Security Foundations Symposium (CSF) and the 23rd IEEE Symposium on Logic In Computer Science (LICS) IMPORTANT DATES Abstract Submission March 31, 2008 Full Paper Submission April 6, 2008 Acceptance Notification May 12, 2008 Camera Ready May 26, 2008 Workshop June 22, 2008 SCOPE The aim of this workshop is to bring together rewriting researchers and security experts, in order to foster their interaction and develop future collaborations in this area, provide a forum for presenting new ideas and work in progress, and enable newcomers to learn about current activities in this area. The workshop focuses on the use of rewriting techniques in all aspects of security. Specific topics include: authentication, encryption, access control and authorization, protocol verification, specification of policies, intrusion detection, integrity of information, control of information leakage, control of distributed and mobile code, etc. Previous instances of SecRet were held in 2006 (S. Servolo, Venice, Italy), and 2007 (Paris, France). LOCATION SecReT'08 will be held at Carnegie Mellon University in Pittsburgh, Pennsylvania, USA. The workshop is associated with the 21st IEEE Computer Security Foundations Symposium (CSF'08) and the 23rd IEEE Symposium on Logic in Computer Science (LICS'08). SUBMISSION PROCEDURE Submission is web-based via a link available in the main web page. Submissions must be received by April 6, 2008. In addition, a title and abstract must be submitted by March 31, 2008. Submitted papers should be at most 15 pages in the ENTCS style, and should include an abstract and the author's information. See the author's instructions of ENTCS style at http://www.entcs.org. PUBLICATION Accepted papers will be published in a preliminary volume available during the workshop. After the workshop, a final version of the proceedings will be published in the Elsevier series Electronic Notes in Theoretical Computer Science (ENTCS). INVITED SPEAKERS Hubert Comon Cachan, France Jonathan Millen MITRE, USA PROGRAM CO-CHAIRS Daniel Dougherty Worcester Polytechnic Institute, USA Santiago Escobar Technical University of Valencia, Spain PROGRAM COMMITTEE Pierpaolo Degano Pisa, Italy Daniel Dougherty Worcester, USA Santiago Escobar Valencia, Spain Maribel Fernandez King's College London, UK Thomas Genet IRISA Rennes, France Joshua Guttman MITRE, USA Catherine Meadows NRL, USA Monica Nesi L'Aquila, Italy Michael Rusinowitch Lorraine, France Ralf Treinen Paris-7, France ********************************************************************

1 0

Lemmas about type functions
by Louis-Julien Guillemette 16 Feb '08

16 Feb '08

Hi all, I've been using GHC's type families somewhat extensively in my type-preserving compiler (BTW, they work great), and quite often I come across the need to prove lemmas about those functions. As far as I understand there's currently no way to handle such lemmas purely at the type level, and I have to encode them as term-level functions. I wonder if I'm missing something, or otherwise if there are plans to provide some way to do this kind of type-level reasoning. Here's a simple example. I encode (de Bruijn) type contexts as lists of types of this form: (t0, (t1, (... , ()...))) I sometimes concatenate type contexts, and need a lemma stating that appending an empty context leaves it unchanged (ts ++ [] == ts). type family Cat ts0 ts type instance Cat () ts' = ts' type instance Cat (s, ts) ts' = (s, Cat ts ts') That is, I need to coerce: Exp (Cat ts ()) into: Exp ts The way I presently do it is through a term-level function that produces a witness that the two types are equivalent, like this: data Equiv s t where Equiv :: (s ~ t) => Equiv s t cat_nil :: EnvRep ts -> Equiv (Cat ts ()) ts cat_nil R0 = Equiv cat_nil (Rs _ ts_r) = case cat_nil ts_r of Equiv -> Equiv coerce :: EnvRep ts -> Exp (Cat ts ()) -> Exp ts coerce ts_r e = case cat_nil ts_r of Equiv -> e Louis

2 1

Downtime, Sat 2008-02-16 1500-1600 UTC: {darcs, hackage, cvs}.haskell.org
by Ian Lynagh 15 Feb '08

15 Feb '08

Hi all, On Saturday 2008-02-16 (tomorrow), monk, which serves as darcs.haskell.org hackage.haskell.org cvs.haskell.org will go down for maintenance sometime probably between 1500 and 1600 UTC. All going well, the outage should be short. Sorry for any inconcenience caused. Thanks Ian

1 0