Generics for the masses

Ralf Hinze. Generics for the masses. In Kathleen Fisher, editor, Proceedings of ICFP'04, Snowbird, Utah, September 19-22, 2004.

Mentioned (with no link) on LtU1.

Hinze shows how to program generically in Haskell 98, making extensive use of type classes.

Those interested in generic programming should make sure they are familiar with references cited in section 5 (many of which were discussed here in the past).

A Functional Quantum Programming Language

We introduce the language QML, a functional language for quantum computations on finite types. Its design is guided by its categorical semantics: QML programs are interpreted by morphisms in the category FQC of finite quantum computations realizable as quantum gates.

Warning - it's a draft. From the Types Forum.

Description Logics in Literate Haskell

Experiments from Graham Klyne:

This file is my attempt to better understand the structure and uses
of Description Logic (DL) languages for knowledge reresentation and inference, with the ultimate aim of better understanding the capabilities and limitations of the Semantic Web ontology language OWL, whose design draws much from Description Logic languages.

See also rdfweb-dev post, "Haskell vs. Ada vs. C++ vs. Awk vs. ..., An Experiment in Software Prototyping Productivity" (PS format)

Implementing Declarative Parallel Bottom-Avoiding Choice

Implementing Declarative Parallel Bottom-Avoiding Choice. Andre Rauber Du Bois, Robert Pointon, Hans-Wolfgang Loidl, Phil Trinder. Symposium on Computer Architecture and High Performance Computing (SBAC-PAD) 2002.

Non-deterministic choice supports efficient parallel speculation, but unrestricted non-determinism destroys the referential transparency of purely-declarative languages by removing unfoldability and it bears the danger of wasting resources on unncessary computations. While numerous choice mechanisms have been proposed that preserve unfoldability, and some concurrent implementations exist, we believe that no compiled parallel implementation has previously been constructed. This paper presents the design, smantics, implementation and use of a family of bottom-avoiding choice operators for Glasgow parallel Haskell. The subtle semantic properties of our choice operations are described, including a careful classification using an existing framework, together with a discussion of operational semantics issues and the pragmatics of distributed memory implementation.

amb breaks referential transparency (e.g., think about (\x.x+x)(3 amb 5) - how many choice points are there?)

This paper presents the problems, and shows how to implementat bottom-avoiding choice operators in Galsgow parallel Haskell (GPH).

The paper is worth checking out for the references alone, which can server as a useful guide to the subject of non-determinism in functional languages. Section 3 of the paper summarizes the semantic properties of the choice operators, and can be a good place to start reading if you are familiar with the subject.

Graham Hutton: Programming in Haskell

The first five chapters of Hutton's introductory Haskell book are online.

The chapters cover fairly basic features, and wouldn't be of interest to the Haskell experts among us, except as teaching material.

However, those intrigued by all the recent references to Haskell can get a taste of what Haskell is about from this readable introduction.

Scrap more boilerplate

Scrap more boilerplate. Ralf Laemmel and Simon Peyton Jones. ICFP'04.

We extend the "scrap your boilerplate" style of generic programming in Haskell to accomplish an additional range of applications. This includes several forms of serialisation and de-serialisation, test-set generation, type validation, and type erasure. To this end, we provide a well-designed reflection API for datatypes and constructors, and we also provide more general means of extending generic functions for given monomorphic or polymorphic types. The presented approach is readily supported in the GHC implementation of Haskell.

The previous "boilerplate" paper was discussed here in the past.

This is a interesting paper and there are many reasons why I should link to it, but I'll let you guess the number 1 reason (hint: check section 10).

Morrow & First-class Labels

First-class labels for extensible rows. (draft)
Daan Leijen.
Submitted to POPL'05. (PDF, BibTeX)

Abstract: This paper describes a type system for extensible records and variants with first-class labels; labels are polymorphic and can be passed as arguments. This increases the expressiveness of conventional record calculi significantly, and we show how we can encode intersection types, closed-world overloading, type case, label selective calculi, and first-class messages. We formally motivate the need for row equality predicates to express type constraints in the presence of polymorphic labels. This naturally leads to an orthogonal treatment of unrestricted row polymorphism that can be used to express first-class patterns. Based on the theory of qualified types, we present an effective type inference algorithm and efficient compilation method. The type inference algorithm, including the discussed extensions, is fully implemented in the experimental Morrow compiler.

Always trust Daan to come up with something both elegant and practical...! However the examples involving bottom (undefined) labels left me skeptical.

Acute: high-level programming language design for distributed computation

Acute: high-level programming language design for distributed computation

This work is exploring the design space of high-level languages for distributed computation, focussing on typing, naming, and version change. We have designed, formally specified and implemented an experimental language, Acute. This extends an OCaml core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built programs. It is expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store primitives, disentangling the language runtime from communication.

This requires a synthesis of novel and existing features:

  • type-safe interaction between programs, with marshal and unmarshal primitives;
  • dynamic loading and controlled rebinding to local resources;
  • modules and abstract types with abstraction boundaries that are respected by interaction;
  • global names, generated either freshly or based on module hashes: at the type level, as runtime names for abstract types; and at the term level, as channel names and other interaction handles;
  • versions and version constraints, integrated with type identity;
  • local concurrency and thread thunkification; and
  • second-order polymorphism with a namecase construct.
The language design deals with the interplay among these features and the core. The semantic definition tracks abstraction boundaries, global names, and hashes throughout compilation and execution, but still admits an efficient implementation strategy.

For more info, see the Main site, from which you can view papers and sample code.

Streaming Representation-Changers

Jeremy Gibbons (2004). Streaming Representation-Changers. To appear in Mathematics of Program Construction, July 2004.

Unfolds generate data structures, and folds consume them. A hylomorphism is a fold after an unfold, generating then consuming a virtual data structure. A metamorphism is the opposite composition, an unfold after a fold; typically, it will convert from one data representation to another. In general, metamorphisms are less interesting than hylomorphisms: there is no automatic fusion to deforest the intermediate virtual data structure. However, under certain conditions fusion is possible: some of the work of the unfold can be done before all of the work of the fold is complete. This permits streaming metamorphisms, and among other things allows conversion of infinite data representations. We present the theory of metamorphisms and outline some examples.

More origami work from Gibbons.

This paper is related to several previous papers by Gibbons that were mentioned here (e.g., spigot pi, arithmetic coding), and it could be said that it summarizes the main results. I don't think this paper was linked to directly, so here goes.

Wobbly types

Wobbly types: type inference for generalised algebraic data types

Simon Peyton Jones, Geoffrey Washburn, and Stephanie Weirich.
July 2004

Generalised algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types", are a simple but powerful generalisation of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult.

It is time to pluck the fruit. Can GADTs be added to Haskell, without losing type inference, or requiring unacceptably heavy type annotations? Can this be done without completely rewriting the already-complex Haskell type-inference engine, and without complex interactions with (say) type classes? We answer these questions in the affirmative, giving a type system that explains just what type annotations are required, and a prototype implementation that implements it. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms.

Edit: Made the title into a hyperlink, as the "Postscript" link could easily get lost in a sea of blue text...

Edit 2:Quoted the article with a plain-ol' <blockquote> instead. Better?

XML feed