You are here: UUCS>Uhc Web>ErikKnoop (27 Nov 2007, UnknownUser)EditAttach
-- ErikKnoop - November 7th 2003

General Reading Material

Working on:

  • "Static types for Dynamic Documents", Mark Brian Shields, Ph.D. thesis
  • "Typing Haskell in Haskell", Mark P. Jones, In Proceedings of the 1999 Haskell Workshop , Paris, France, October 1999. Published in Technical Report UU-CS-1999-28, Department of Computer Science, University of Utrecht.(new reference)

Summaries

"A Static Semantics for Haskell"

Author: Karl Filip Faxén
Location:Journal of Functional Programming Vol 12, Issue 5., or through the home page of the author in compressed postscript

This article is a very technical one about the exact meaning of some constructs. Informal specifications in the Haskell 98 report are formally notated in this article. Due to the complexity of the Haskell language, this article isn't particularly easy to read or understand. Despite the difficulty it offers great insights in how a language works "behind the scenes".

"The (revised) Haskell 98 report"

Editor: Simon Peyton Jones
Location: www.haskell.org

The official Haskell 98 language specification. I think there isn't much to summerize about this article.

"A Polymorphic Type System for Extensible Records and Variants"

Authors: Benedict R. Gaster and Mark P. Jones

This article describes a way to implemented extendible records and variants. Very usefull because of the clear style and the excellent examples. Further it contains type rules and translation mechanisms.

"First-Class Modules for Haskell"

Authors: Mark Shields and Simon Peyton Jones

An article about how the module system of Haskell could be lifted to one with more possibilities. They use records to achieve these possibilities.

"A formal specification of the Haskell 98 module system"

Authors: Iavor S. Diatchki, Mark P. Jones and Thomas Hallgren

A specification of how the Haskell 98 module worksb and what is capabilities are. Further an implementation of it is given in Haskell itself.

Derivable Type Classes

Authors: Ralf Hinze and Simon Peyton Jones

This article describes a way to write type-classes in a generic way, using generic functions.

Chapter 9 of the Clean Manual: Uniqueness Typing

Author: ?

A simple introduction on how to use uniqueness types, but no technical background.

"Type-Indexed Rows"

Authors: Mark Shields and Erik Meijer

An interesting article about an alternative approach to extendible records. Records and variants are indexed by their type rather than positional (or with their labels).

"Lightweight Extensible records for Haskell"

Authors: Mark P. Jones and Simon Peyton Jones

An evaluation of wat the implementation of Trex has offered the programmers. Contains usefull research directions.

"Type inference for records in a natural extension of ML"

Author: Didier Remy

A very technical and complicated article about how records could be included in ML.

"Typing record concatenation for free"

Author: Didier Remy

An interesting article about how 2 records could be concatenated without doing difficult things in our type inferencing.

Examples

Below there are some examples which are ment to illustrate the translation needed.

We'll start with a very simple example

g1 :: Int -> Rec {xl :: Int}
g1 = \(x::Int) -> Rec {xl = x}

It's easy to derive this type annotation from the body of
g
itself. A translation of this code fragment will look like the code below.

g1' :: Int -> Rec {xl :: Int}
g1' \(x::Int) -> insertAt 0 x EmptyRec

In this example it is never needed to pass the offset at which
x
should be inserted to the function, since it is always inserted in the empty record (or, even better, the empty row). This means that the offset simply is a constant. And this constant can immediatly be filled in.

It becomes a little more complicated if we want to insert to labels into the empty row. Consider the following example.

g2 :: Int -> Int -> Rec {xl :: Int, yl :: Int}
g2 = \(x::Int) (y::Int) -> Rec {xl = x, yl =y}

The translation will intuitively happen in two passes, one for each label. So after the first pass, the code fragment will look like the code below.

g2' :: Int -> Int -> Rec {xl :: Int, yl :: Int}
g2' = \(x::Int) (y::Int) -> insertAt 1 y (Rec {xl = x})

For now, I have chosen for a simple lexicographical ordering, and in that case, the yl is "greater than" the xl, and as such, y should be inserted at position 1. After the second pass, the code example would look like the following.

g2'' :: Int -> Int -> Rec {xl :: Int, yl :: Int}
g2'' = \(x::Int) (y::Int) -> insertAt 1 y (insertAt 0 x EmptyRec)

Using this mechanism, we can translate any expression which inserts labels into an empty row, or more general a closed row. A closed row is some row which ends with a fixed "tail", i.e. which doesn't end with some row variable, indicating that any row can occur there. Some attention still has, however, to be paid to the function insertAt, which also needs a label as it's parameter.

More challenging are the examples which contain open rows. Consider the following code example.

f1 :: (r\yl) => Rec r -> Int -> Rec {xl :: Int | r}
f1 = \r (x::Int) -> Rec {xl = x | r}

The following code fragment is a simple translation of this example.

f1' :: Offset -> Rec r -> Int -> Rec {xl :: Int | r}
f1' = \ox r (x::Int) -> insertAt ox x r

So, the constraint propagates to an explicit parameter of the function, indicating at which position x should be inserted into the record r. It is now interesting to look at the caller-site of f1, and how that translates into the caller-site of f1'.

f1 EmptyRec 3

So we should f1' also pass the offset a which the label xl could be inserted into EmptyRec. This fairly trivial.

f1' 0 EmptyRec 3

Further complications could be added. One could think of
  • First class labels.
  • Leaving the constraints out if they could be inferred.
  • etc.

Deliverables

At the end of the seminar I've given a presentation of which the slides are available (pdf). I've also written a small report on the things I've done and this is available in (ps) and (pdf). And last but not least, the prototype, which is full of inconsistencies and bugs, is available.

Contact

If you have suggestions, comments or whatever, don't hesitate but send me an e-mail!
Topic revision: r6 - 27 Nov 2007, UnknownUser
 

This site is powered by FoswikiCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UUCS? Send feedback