Extensible Records

[Barney Hilken]

>
> Hugs.Trex> :t let f opts x = (opt1="default"|opts) in f
> let {...} in f :: a\opt1 => Rec a -> b -> Rec (opt1 :: [Char] | a)

This completely loses the aim of optional arguments: with this type,  
the argument 'opts' cannot have a field 'opt1' (as shown by the  
context 'a\opt1'). The type we want should say that 'opts' cannot  
have any fields except 'opt1' (though that is optional). Flex cannot  
express this type.

>  (btw, what is "Flex-like"?)

What I meant by "Flex-like" systems is that they can only extend  
record types by fixed fields. As well as the usual extraction and  
deletion of fields, I want first-class operators:

(+:) :: r `Disjoint` s => r -> s -> r :+: s
	x +: y is the concatenation of two records x and y, under the  
condition that they have no fields in common
	r :+: s is the type of x +: y, assuming x::r and y::s

(|:) :: r `Subrecord` s => s -> r -> s
	x |: y is the update of x by y, under the condition that every field  
of y is a field of x of the same type
	the type of x |: y is the same as the type of x

The conditions on the types of these operators are important, as they  
catch common errors. For example, if a function 'f' has optional  
arguments 'opt1::x1, ... optn::xn' you want 'f {optt1 = val}' to give  
a type error because you've misspelled 'opt1', not simply to ignore  
it. In other words, you need a condition that the fields of the  
record argument of f are a subset of {opt1, .., optn}.

These operators can be defined using type families: download the code  
from
	http://homepage.ntlworld.com/b.hilken/files/Records.hs
This code would only need minimal extensions to GHC to make it  
completely useable.


> some time ago (was that really 2 years? trac claims it was), i
> suggested that any record system with first-class labels needs
> language support for type sharing: if i import modules A and B,
> each of which introduces a record-label X, i need some way of
> telling the type system that A.X ~ B.X (Trex solved that problem
> by not requiring label declarations at all, but Trex labels weren't
> first-class objects, either).

I believe this issue is completely independent of records. Exactly  
the same problem would arise if the same datatype with the same  
constructors was defined in two different modules. To solve this we  
need a mechanism whereby identically defined types in different  
modules can be identified.

> i propose to start "Records project" by composing list of
> requirements/applications to fulfill; we can keep it on Wiki page.
> this will create base for language theorists to investigate various
> solutions. i think they will be more motivated seeing our large
> interest in this extension

I am happy to contribute to this, but I am strongly biased in favour  
of my own records system!

Barney.