If you find something interesting here, or if you have a related idea, just contact me (Patrik Jansson).
Applying partial evaluation and deforestation techniques to the instances generated from a polytypic definition should result in code as good as (or better) than hand-written code. This goal of this project is to bring theory and tools from partial evaluation to good use in implementing polytypic programming.
Combine the strong points from Cayenne and Agda to make a language for programming with dependent types. The focus could be more on the theoretical side (language, type system, etc.) or more on the implementation side (how to compile the code: via Haskell? O'Caml?, FLINT (or other intermediate language)?).
Cayenne (paper 1, paper 2), Agda, Alfa, (O)Caml (papers)
Simon Peyton Jones, David Lester. Implementing Functional Languages
A related masters thesis project (Dependent Haskell?) is carried out by Pontus Olsson, supervised by Jan-Willem Roorda and John Hughes.
Idea: Tool and language support for (analytic) mathematics (in physics research etc.) where approximation is important.
In (mathematical/theoretical) physics large chunks of an article can be simplification of a complex (often exact) analytical expressions [the solution of a partial differential equation (PDE)] to a reasonably simple (inexact) form. These simlifications involve clever analytical manipulations (simplifications, integration, etc.) but very often also approximations. Tool support (for example Mathematica) exists for exact manipulation, but there is also a need for managing, simplifying, testing and proving propoerties about the approximations. (Are the approximations consistent? What are the error bounds? What are the main proof obligations?)
More specific project ideas could range from developing a language for expressing common approximations to implementing a connection between Mathematica and a proof checker.
Investigate state-of-the-art about implementing groups, rings, modules, etc. in Haskell or Agda/Cayenne.
Design a language and a semantics for expressing a mixture of proofs, tests and other "certificates of [partial] correctness". Test converage? Proof coverage?
Related to the Programmatica project and the (just started) local project with a similar aim.
A recent paper by Jansson & Jeuring about Data conversion describes polytypic (generic) functions (Arrows) for printing and parsing + gives (informal) proofs of correctness (roughly "print then parse is the identity function (arrow)). It seems possible to formalise this into a generic definition of embedding-projection pairs (which in a constructive setting would be triples (two functions and a proof)).
Related investigations with same paper as the background could be to Quickcheck the existing proofs, or to use automatic proof methods (Twelf).
A recent paper Dictionary passing for polytypic polymorphism by Juan Chen and Andrew W. Appel has shown that a dictionary passing implementation is possible for some polytypic functions inside the SMLNJ compiler. The goal of this project is to investigate to what extent these ideas generalize to a broader polytypic setting how they can be applied using Haskell as the underlying language.
Some parts investigated by Ulf NorellAs part of the Programatica project at OGI, Thomas Hallgren has started implemented a translator from Haskell to Alfa/Agda. Completing this translator would give a large base set of libraries for programming with dependent types and it would also add to the understanding of the difference between polymorphic functional programming (Haskell) and monomorphic type theory (Alfa).
Partly investigated by Christophe DelageUlf Norell: Master's thesis 2002: Functional Generic Programming and Type Theory [ps]
François-Régis Sinot: project work 2001: Polytypic programming and dependent types
For an in-depth treatment of polytypism, see Janssons PhD thesis, Functional Polytypic Programming, or the AFP'98 tutorial.