June 2014 - Haskell - Haskell.org

ANNOUNCE: vty-5.1 and vty-examples-5.0
by Corey O'Connor 07 Jun '14

07 Jun '14

The work never ends but, *pokes*, seems cooked to me! vty 5.1 is out: - http://hackage.haskell.org/package/vty All parts of vty have received care and a whole bunch of testing. Highlights: - Naming convention matches the Haskell standard. - User and application configurable input to event mapping. see Graphics.Vty.Config - Layer support. see Graphics.Vty.Picture - Cropping and padding of images. Great for implementing vertical splits in Yi, for instance. - Improved compatibility. - Improved performance. Full CHANGELOG: * https://raw.githubusercontent.com/coreyoconnor/vty/master/CHANGELOG -Corey O'Connor coreyoconnor(a)gmail.com http://corebotllc.com/

2 2

Final call for talk proposals: HOPE'14 (Workshop on Higher-Order Programming with Effects, affiliated with ICFP'14)
by Neelakantan Krishnaswami 06 Jun '14

06 Jun '14

---------------------------------------------------------------------- CALL FOR TALK PROPOSALS HOPE 2014 The 3rd ACM SIGPLAN Workshop on Higher-Order Programming with Effects August 31, 2014 Gothenburg, Sweden (the day before ICFP 2014) http://hope2014.mpi-sws.org ---------------------------------------------------------------------- HOPE 2014 aims at bringing together researchers interested in the design, semantics, implementation, and verification of higher-order effectful programs. It will be *informal*, consisting of invited talks, contributed talks on work in progress, and open-ended discussion sessions. --------------------- Goals of the Workshop --------------------- A recurring theme in many papers at ICFP, and in the research of many ICFP attendees, is the interaction of higher-order programming with various kinds of effects: storage effects, I/O, control effects, concurrency, etc. While effects are of critical importance in many applications, they also make it hard to build, maintain, and reason about one's code. Higher-order languages (both functional and object-oriented) provide a variety of abstraction mechanisms to help "tame" or "encapsulate" effects (e.g. monads, ADTs, ownership types, typestate, first-class events, transactions, Hoare Type Theory, session types, substructural and region-based type systems), and a number of different semantic models and verification technologies have been developed in order to codify and exploit the benefits of this encapsulation (e.g. bisimulations, step-indexed Kripke logical relations, higher-order separation logic, game semantics, various modal logics). But there remain many open problems, and the field is highly active. The goal of the HOPE workshop is to bring researchers from a variety of different backgrounds and perspectives together to exchange new and exciting ideas concerning the design, semantics, implementation, and verification of higher-order effectful programs. We want HOPE to be as informal and interactive as possible. The program will thus involve a combination of invited talks, contributed talks about work in progress, and open-ended discussion sessions. There will be no published proceedings, but participants will be invited to submit working documents, talk slides, etc. to be posted on this website. ----------------------- Call for Talk Proposals ----------------------- We solicit proposals for contributed talks. Proposals should be at most 2 pages, in either plain text or PDF format, and should specify how long a talk the speaker wishes to give. By default, contributed talks will be 30 minutes long, but proposals for shorter or longer talks will also be considered. Speakers may also submit supplementary material (e.g. a full paper, talk slides) if they desire, which PC members are free (but not expected) to read. We are interested in talks on all topics related to the interaction of higher-order programming and computational effects. Talks about work in progress are particularly encouraged. If you have any questions about the relevance of a particular topic, please contact the PC chairs at the address hope2014 AT mpi-sws.org. Deadline for talk proposals: June 13, 2014 (Friday) Notification of acceptance: July 4, 2014 (Friday) Workshop: August 31, 2014 (Sunday) The submission website is now open: https://www.easychair.org/conferences/?conf=hope2014 --------------- Invited Speaker --------------- Verifying Security Properties of SES Programs Philippa Gardner, Imperial College London Secure ECMAScript (SES) is a subset of JavaScript, designed in such a way that untrusted code can safety co-exist with trusted code. We introduce a program logic for verifying security properties of SES programs. It follows separation logic in that we can make local assertions about local state. It is different from separation logic in that we can also make global assertions about the global state and its interface with the local state. For example, we can globally assert that untrusted objects do not contain pointers to local trusted objects. Such assertions are key for describing security properties of common SES programs. This logic builds on the work of Gardner, Maffeis and Smith on reasoning about a core fragment of JavaScript (POPL2012), and the recent work of Smith on extending the logic to handle higher-order functions. This is joint work with Gareth Smith and Thomas Wood, Imperial. --------------------- Workshop Organization --------------------- Program Co-Chairs: Neel Krishnaswami (University of Birmingham) Hongseok Yang (University of Oxford) Program Committee: Zena Ariola (University of Oregon) Ohad Kammar (University of Cambridge) Ioannis Kassios (ETH Zurich) Naoki Kobayashi (University of Tokyo) Paul Blain Levy (University of Birmingham) Aleks Nanevski (IMDEA) Scott Owens (University of Kent) Sam Staton (Radboud University Nijmegen) Steve Zdancewic (University of Pennsylvania)

1 0

Re: [Haskell] [Haskell-cafe] PROPOSAL: Record field type inference
by John Meacham 04 Jun '14

04 Jun '14

Yeah, I am familier with that, this is fairly orthogonal actually and both can be used together to good effect. This proposal is more about making records 'lightweight', as in, I have a recursive function that takes 5 or so recursive values and they all have to be passed as independent options (or a tuple) right now which is error prone, by making a lightweight inferred record we get named parameters that are infered just like they were listed as options and CPR analysis will even ensure there is no run time penalty, the fields will be expanded out as positional parameters internally. An issue with OverloadedRecordFields is that it relies on a lot of type system complexity, This builds on the existing DisambiguateRecordFields extension and simply removes the restriction that the records with the same field names be defined in different modules. since field names declared this way don't share a namespace with functions this isn't an issue. Notably, everything to disambiguate fields can take place in the renamer and the fields can be typechecked exactly as if they were top level pattern bindings. Another possible extension is allowing it to infer scoped type variables as well for a parameterized record type. working on something concrete for that with my jhc implementation, the issue is that the record will have to be parameterized by a type to keep them from escaping. Perhaps just a single type parameter that is existentially instantiated, syntax being data R t = R {fa,fb,fc} or putting the data declaration in a local where or let binding. but that will require some more work. (and scoped type variables in jhc are a little iffy at the moment as is) John On Tue, Jun 3, 2014 at 11:33 PM, Carter Schonwald <carter.schonwald(a)gmail.com> wrote: > Hey John > in some respects, this sounds like syntax sugar around > https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields > have you had a look at that? (its not quite merged into HEAD yet, but that > due soon i'm told) > > > On Wed, Jun 4, 2014 at 2:26 AM, John Meacham <john(a)repetae.net> wrote: >> >> This is also available as html at >> >> http://repetae.net/computer/jhc/record_inference.html >> >> Record Type Inference >> ===================== >> >> An extension to the named field mechanism that will greatly enhance the >> utility of them when combined with the existing >> `DisambiguateRecordFields`, >> `RecordPuns`, and `RecordWildCards`. >> >> The proposal is to allow the types of record fields to be inferred by the >> normal type inference engine. It would look like >> >> ~~~~ {.haskell} >> data Rec = Rec {fieldA,fieldB,fieldC} >> >> f Rec { .. } = Rec { .. } where >> fieldA = True >> fieldB = 4 >> ~~~~ >> >> This would infer the types `Bool`, `Int`, and `forall a . a` for the >> fields of >> the record constructor and `f :: Rec -> Rec` for f. For the purposes of >> type >> checking the fields are treated as monomorphic and not generalized but >> defaulted like normal after typechecking the module. Other than infering >> the >> types of the record fields, the records have the normal syntax. The >> extensions >> `RecordPuns`, `RecordWildCards` and `DisambiguateRecordFields` will be >> enabled >> when record field inference is enabled. >> >> Selector functions will not be created for infered records, as in, the >> names >> are field labels and not functions. This means they do not share a >> namespace >> with functions and do not conflict with each other. Multiple records may >> have >> the same field names in the same module. This means the following is fine. >> >> ~~~~ {.haskell} >> data Rec1 = Rec1 {input, withFoo, withoutFoo } >> data Rec2 = Rec2 {input, withBar, withoutBar } >> >> f Rec1 { .. } = case input of >> [] -> Rec1 { .. } >> (x:xs) -> if hasFoo x >> then Rec1 { withFoo = x:withFoo, .. } >> else Rec1 { withoutFoo = x:withoutFoo, .. } >> ~~~~ >> >> Possible extensions >> ------------------- >> >> ### as-pattern disambiguation >> >> In order to make the disambiguation of record fields more useful without >> relying on the type checker for disambiguation, We can declare that >> variables >> explicitly bound to a constsructor in a pattern match use that constructor >> to >> disambiguate fields for operations on the variable. This is a purely >> syntactic >> transformation that can happen before typechecking. It can be used as >> follows. >> >> ~~~~ {.haskell} >> -- use the input bound by a Rec1 to update the input bound by a Rec2 >> f r1@Rec1 { input } r2@Rec2 {} = case input of >> xs | any hasBar xs = f r1 { input = [] } r2 { input } >> ~~~~ >> >> ### Field label inference >> >> It is concievable that we may want to infer the fields themselves of a >> record, >> as in: >> >> ~~~~ {.haskell} >> -- infer that R has the field labels bob and susan >> data R = R { ..} >> f x@R {bob} = R {susan = bob} >> ~~~~ >> >> In order to implement this, a pass through the file will collect every >> field >> label that is used with an explicit R constructor and treat the record as >> if >> it were declared with those names as infered fields. >> _______________________________________________ >> Haskell-Cafe mailing list >> Haskell-Cafe(a)haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe > > -- John Meacham - http://notanumber.net/

1 0

PROPOSAL: Record field type inference
by John Meacham 04 Jun '14

04 Jun '14

This is also available as html at http://repetae.net/computer/jhc/record_inference.html Record Type Inference ===================== An extension to the named field mechanism that will greatly enhance the utility of them when combined with the existing `DisambiguateRecordFields`, `RecordPuns`, and `RecordWildCards`. The proposal is to allow the types of record fields to be inferred by the normal type inference engine. It would look like ~~~~ {.haskell} data Rec = Rec {fieldA,fieldB,fieldC} f Rec { .. } = Rec { .. } where fieldA = True fieldB = 4 ~~~~ This would infer the types `Bool`, `Int`, and `forall a . a` for the fields of the record constructor and `f :: Rec -> Rec` for f. For the purposes of type checking the fields are treated as monomorphic and not generalized but defaulted like normal after typechecking the module. Other than infering the types of the record fields, the records have the normal syntax. The extensions `RecordPuns`, `RecordWildCards` and `DisambiguateRecordFields` will be enabled when record field inference is enabled. Selector functions will not be created for infered records, as in, the names are field labels and not functions. This means they do not share a namespace with functions and do not conflict with each other. Multiple records may have the same field names in the same module. This means the following is fine. ~~~~ {.haskell} data Rec1 = Rec1 {input, withFoo, withoutFoo } data Rec2 = Rec2 {input, withBar, withoutBar } f Rec1 { .. } = case input of [] -> Rec1 { .. } (x:xs) -> if hasFoo x then Rec1 { withFoo = x:withFoo, .. } else Rec1 { withoutFoo = x:withoutFoo, .. } ~~~~ Possible extensions ------------------- ### as-pattern disambiguation In order to make the disambiguation of record fields more useful without relying on the type checker for disambiguation, We can declare that variables explicitly bound to a constsructor in a pattern match use that constructor to disambiguate fields for operations on the variable. This is a purely syntactic transformation that can happen before typechecking. It can be used as follows. ~~~~ {.haskell} -- use the input bound by a Rec1 to update the input bound by a Rec2 f r1@Rec1 { input } r2@Rec2 {} = case input of xs | any hasBar xs = f r1 { input = [] } r2 { input } ~~~~ ### Field label inference It is concievable that we may want to infer the fields themselves of a record, as in: ~~~~ {.haskell} -- infer that R has the field labels bob and susan data R = R { ..} f x@R {bob} = R {susan = bob} ~~~~ In order to implement this, a pass through the file will collect every field label that is used with an explicit R constructor and treat the record as if it were declared with those names as infered fields.

1 0

Core libraries committee seeking self-nominations
by Edward Kmett 04 Jun '14

04 Jun '14

The first year of the Haskell Core Libraries Committee <http://www.haskell.org/haskellwiki/Core_Libraries_Committee> is winding down, and we are seeking self-nominations to replace two outgoing committee members. Doug Beardsley and Brent Yorgey have offered to be the first two members of the committee to have their slots come up for renewal. To nominate yourself, please send an email to core-libraries-committee(a)haskell.org by June 30th and include any information that you think will help us reach a decision. The core libraries committee acts as the collective maintainer of many packages that glue together the Haskell Platform, but which otherwise do not have an individual maintainer. See Library Submissions <http://www.haskell.org/haskellwiki/Library_submissions> for more details about which packages fall to the committee for maintenance. As we are now talking on more of the implementation effort for the Applicative-Monad Proposal, bringing Foldable and Traversable into Prelude, performing active maintenance on vector, etc., you should be forewarned that these are becoming increasingly active positions now that GHC 7.8 has shipped and we are ramping up for more active participation in the GHC release process. Regards, Edward Kmett Haskell Core Libraries Committee Chair

1 0

ICFP 2014 Student Volunteer Programme
by David Van Horn 03 Jun '14

03 Jun '14

[With apologies for cross-posting] Please forward this to anyone who may be interested! ICFP Student Volunteer Programme http://icfpconference.org/icfp2014/sv.html We are looking for student volunteers to help with the running of ICFP 2014 in Gothenburg, Sweden. If you are a student (part-time, full-time, undergraduate, masters or PhD), and would like free registration in exchange for helping out, please consider applying! As a student volunteer, you will receive the following: * Free conference registration, including workshops and electronic proceedings * Free lunches and refreshments during breaks. * Free conference banquet ticket and access to student-only social events. * An ICFP 2014 Student Volunteers T-shirt. In return you will be expected to help with the running of the conference. Possible jobs include assisting with technical sessions, workshops, tutorials and panels and helping at the registration desk. Please note that student volunteers are responsible for their own travel arrangements and accommodation. You should be available for at least three full days between 31st of August and the 6th of September 2014 in order to offer 16 hours of volunteering work. Note that we will prioritise students who will be available the full week. Naturally presentations etc. at workshops and technical sessions take precedence. Application Deadline: 15th June 2014 Initial Acceptance and Reserve List announcement: 30th June 2014 For more information, and instructions on how to apply, please see the student volunteer information page at http://icfpconference.org/icfp2014/sv.html.

1 0

ANNOUNCE: jhc 0.8.2
by John Meacham 02 Jun '14

02 Jun '14

Lots of internal improvements in this one, so may be of more interest to developers http://repetae.net/computer/jhc/ - completely replaced the front end parser/lexer with a new more flexible one. My rewritten one is about 3,250 lines shorter. - The new one uses a general precedence parser for application as well as infix operators, allowing consistent handling of bang, irrefutable, and @ patterns and allows prefix and infix operators with a higher precedence than application to be defined. Incidentally, this allows for ~ and @ in expressions. (~) = negate (prefixr 11) gives us a nice strongly binding negative and @ (infixr 12) is perfect for type directed name resolution without further overloading the humble dot. they parse exactly the same as they do in patterns so no new magic is being added to the symbols other than allowing them in expressions. - Layout algorithm is fully in the lexer now, no lexer/parser interaction needed and useful transformations happen between the two simplifying the parser. - updated a lot of the external libraries to new versions - improvements to the build based on feedback, now gives much better error messages about what went wrong. - include an experimental utility to automatically download 3rd party packages from hackage and install them, it has some kinks, but even if it can't do it automatically, it provides a template for easily modifying the package to work. - removed the last of the cabal-cruft from the library build system. - fixed a lot of bugs relating to errors not being caught early by jhc so they produce a cryptic message from the compiler later, attach source location to more errors for better reporting. - ghc 7.8 compatibilty contributed by others. (thanks!) - infix type constructor extension supported - field punning extension now supported - new option -fno-sugar to turn off all desugaring that would introduce any hidden dependencies, all literals are unboxed under it. WYSIWYG. - unboxed kinds now more general, work in more places - record field names may overlap - more efficient binary representation using LEB128 - Data.String added with mild magic. -- John Meacham - http://notanumber.net/

1 0

WPTE 2014: Call for Participation
by David Sabel 02 Jun '14

02 Jun '14

CALL FOR PARTICIPATION First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE'14) affiliated with RTA/TLCA 2014 (a FLoC 2014 workshop, FLoC is part of the Vienna Summer of Logic 2014) 13th July 2014, Vienna, Austria http://www.ki.informatik.uni-frankfurt.de/WPTE14 =========================================================================== The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area. Registration ============ http://vsl2014.at/registration/ Note that early registration ends on June 8th! Program ======= * Andy Gill Invited talk, TBA * William Mansky and Elsa Gunter Verifying Optimizations for Concurrent Programs * Masanori Nagashima, Tomofumi Kato, Masahiko Sakai and Naoki Nishida Inverse Unfold Problem and Its Heuristic Solving * David Sabel Structural Rewriting in the Pi-Calculus * Guillaume Madelaine, Cedric Lhoussaine and Joachim Niehren Attractor Equivalence: An Observational Semantics for Reaction Networks * Naoki Nishida, Makishi Yanagisawa and Karl Gmeiner On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings * Manfred Schmidt-Schauss and David Sabel Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report) * Yuki Chiba Verifying the Correctness of Tupling Transformations based on Conditional Rewriting * Karl Gmeiner and Naoki Nishida Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems * Georg Moser and Michael Schaper A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems

1 0

UNIF 2014: Call for Participation
by Temur Kutsia 01 Jun '14

01 Jun '14

==================================================== Call for Participation UNIF 2014 The 28th International Workshop on Unification July 13, 2014. Vienna, Austria a FLoC workshop hosted by RTA-TLCA and IJCAR http://vsl2014.at/unif ==================================================== Invited Speakers ---------------- * Jordi Levy, IIIA, CSIC, Barcelona, Spain * Jose Meseguer, University of Illinois at Urbana-Champaign, USA: Extensible Symbolic System Analysis Program ------- http://vsl2014.at/meetings/UNIF-program.html Registration ------------ http://vsl2014.at/registration (Don't forget the early registration deadline: June 8) We look forward to seeing you in Vienna! The UNIF 2014 organizers: Temur Kutsia Christophe Ringeissen

1 0

2nd CfP: SCSS 2014
by Temur Kutsia 01 Jun '14

01 Jun '14

SCSS 2014 Symbolic Computation in Software Science 6th International Symposium Second Call for Papers Gammarth, La Marsa, Tunisia, December 7-11, 2014 http://www.easychair.org/smart-program/SCSS2014/ Scope -------- The purpose of SCSS 2014 is to promote research on theoretical and practical aspects of symbolic computation in software science. The symposium provides a forum for active dialog between researchers from several fields of computer algebra, algebraic geometry, algorithmic combinatorics, computational logic, and software analysis and verification. SCSS 2014 solicits both regular and tool papers on all aspects of symbolic computation and their applications in software science. The topics of the symposium include, but are not limited to the following: - automated reasoning - algorithm (program) synthesis and/or verification - formal methods for the analysis of network security - termination analysis and complexity analysis of algorithms (programs) - extraction of specifications from algorithms (programs) - theorem proving methods and techniques - proof carrying code - generation of inductive assertion for algorithm (programs) - algorithm (program) transformations - formalization and computerization of knowledge (maths, medicine, economy, etc.) - component-based programming - computational origami - query languages (in particular for XML documents) - semantic web and cloud computing Invited Speakers ---------------- Nikolaj Bjorner (Microsoft Research) TBA Program Chairs -------------- Temur Kutsia (RISC, Johannes Kepler University Linz, Austria) Andrei Voronkov (University of Manchester, UK) Program Committee ------------------ Elvira Albert (Complutense University of Madrid, Spain) Adel Bouhoula (Higher School of Communications of Tunis, Tunisia) James H. Davenport (University of Bath, UK) Roberto Giacobazzi (University of Verona, Italy) Arie Gurfinkel (Carnegie Mellon University, USA) Nao Hirokawa (JAIST, Japan) Tetsuo Ida (University of Tsukuba, Japan) Florent Jacquemard (INRIA - IRCAM, France) Laura Kovacs (Chalmers University of Technology, Sweden) Temur Kutsia (RISC, Johannes Kepler University Linz, Austria) - chair Ali Mili (New Jersey Institute of Technology, USA) Joel Ouaknine (Oxford University, UK) Ruzica Piskac (Yale University, USA) Andrei Voronkov (University of Manchester, UK) - chair Dongming Wang (Beihang University, China and UPMC-CNRS, France) General Chairs --------------- Adel Bouhoula (Higher School of Communications of Tunis, Tunisia) Tetsuo Ida (University of Tsukuba, Japan) Local Chair ----------- Mohamed Becha Kaaniche (University of Carthage, Tunisia) Important Dates --------------- June 23, 2014: Abstract submission deadline June 30, 2014: Paper submission deadline August 25, 2014: Notification September 22, 2014: Camera-ready copy deadline December 7-11, 2014: SCSS 2014 in Gammarth Submission ---------- Submission is via EasyChair: https://www.easychair.org/conferences/?conf=scss2014 Submissions are invited in two categories: regular research papers and tool papers. - Regular research papers must not exceed 12 pages in the EasyChair Class format, with up to 3 additional pages for technical appendices. - Tool papers must not exceed 6 pages in the EasyChair Class format. Publication ---------- The proceedings will be published in the EasyChair Proceedings in Computing. We plan also to have a special issue of the Journal of Symbolic Computation on SCSS 2014. The full version of selected papers will be considered for the publication of the special issue subjected to the normal peer review process of the journal.

1 0