[Haskell] extensible records using associated types

[Barney Hilken]

I'm sorry if this example has already been posted, but I couldn't  
find it by searching the archives. If it's new (and works properly),  
it provides more evidence that ATs are a good thing.



You can use associated type synonyms to implement polymorphic  
extensible records.
 
-


We will represent records as values of the form
N1 x1 (N2 x2 ... (Nn xn Empty)...)
with corresponding type
N1 a1 (N2 a2 ... (Nn an Empty)...)
where the field name N is defined by the declaration
data N a r = N a r

For convenience, we define the type of field name constructors:

>type Constructor n = forall a. forall r. a -> r -> n a r

so that N :: Constructor N for each field name N.

Next we define a class (:<:) whose purpose is to tell the compiler in  
which order to store fields:


>class (m :: * -> * -> *) :<: (n :: * -> * -> *)

The idea is that if N and M are distinct field names which might  
appear the same record, then there must be an instance of exactly one  
of N :<: M and M :<: N.


The class Contains n r asserts that r is a record type with a field  
labelled n:


>class Contains n r where
>type Project n r
>type Delete n r 
>project :: Constructor n -> r -> Project n r
>delete :: Constructor n -> r -> Delete n r

There are two associated types: Project n r is the type of the n  
field, and Delete n r is the type of the rest of the record. The  
functions project and delete give the corresponding values.


The class Lacks n r asserts that r is a record type without a field  
labelled n:


>class Lacks n r where   
>type Extend n a r  
 
>extend :: Constructor n -> a -> r -> Extend n a r

There is one associated type: Extend n a r is the type of the record  
obtained by adding a field of type a labelled n. Note that according  
to the AT paper, the parameter a should come last, but this order is  
much more convenient. The function extend adds the new field to the  
record.


The class Disjoint r s asserts that r and s are record types with no  
fields in common:


>class Disjoint r s where
>type Union r s  
>union :: r -> s -> Union r s

There is one associated type: Union r s is the type of the merged  
record, and union is the merge function.



Next we define the empty record:

>data Empty = Empty

It has no fields, so has no instances of Contains, but lots of  
instances of Lacks:


>instance Lacks n Empty where
>type Extend n a Empty = n a Empty
>extend nn x Empty = nn x Empty  

It is also disjoint from everything:

>instance Disjoint Empty r where
>type Union Empty r = r  
>union Empty t = t   


Each field name must be defined as a data type together with  
instances of the classes Contains, Lacks and Disjoint as follows:


>data N a r = N a r

The type N a r certainly contains a field named N:

>instance Contains N (N a r) where
>type Project N (N a r) = a  
>type Delete N (N a r) = r   
>project N (N x t) = x   
>delete N (N x t) = t

It also Contains all the fields of r, though you only need to check  
names which are below N:


>instance m :<: N, Contains m r => Contains m (N a r) where
>type Project m (N a r) = Project m r
>type Delete m (N a r) = N a (Delete m r)
>project mm (N x t) = project mm t   
>delete mm (N x t) = N x (delete mm t)   

Similarly, it Lacks all the fields which r Lacks, except for N  
itself. This is where we really need the ordering :<: to ensure that  
m is not equal to N. There are two cases, m :<: N:


>instance m :<: N, Lacks m r => Lacks m (N a r) where
>type Extend m b (N a r) = N a (Extend m b r)
>extend mm y (N x t) = N x (extend mm y t)   

and N :<: m:

>instance N :<: m => Lacks m (N a r) where
>type Extend m b (N a r) = m b (N a r)
>extend mm y (N x t) = mm y (N x t)  

To ensure that N a r is disjoint from s, it is enough that r is  
disjoint from s and N is not in their union:


>	instance Disjoint r s, Lacks N (Union r s) => Disjoint (N a r) s  
where

>type Union (N a r) s = Extend N a (Union r s)
>union (N x t) u = extend N x (union t u)


Finally, we must maintain the ordering :<:. It has to be a global  
linear order, so if we know the last field name was M, we can define:


>instance M :<: N
>instance m :<:

Re: [Haskell] extensible records using associated types

[Barney Hilken]

Of course, under Usage, I should have written:

The record {N1 = x1, ... Nn = xn} should be constructed as (extend N1  
x1 $ ... $ extend Nn xn $ Empty).


Sorry about any confusion!

Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] extensible records using associated types

[Barney Hilken]

The implementation of records using types data N a r = N a r might  
well be inefficient, and I don't know enough about the workings of  
the compiler to see whether it could be improved by unboxing and  
strictness. But the real point of my post was the classes Contains,  
Lacks and Disjoint which give you extensibility. To give another  
example, if Haskell had non-extensible records {N1 = x1, ..., Nn =  
xn} of type {N1 :: a1, ..., Nn :: an} we could use the same technique  
to make them extensible.


Assume we can represent the field names N somehow as values (N ::  
Constructor N). Then we can define instances of the form


instance Contains Nj {N1 :: a1, ..., Nj :: aj, ..., Nn :: an} where
type Project Nj {N1 :: a1, ..., Nj :: aj, ..., Nn :: an} = aj
		type Delete Nj {N1 :: a1, ..., Nj :: aj, ..., Nn :: an} = {N1 ::  
a1, ..., Nn :: an}

project Nj {N1 = x1, ..., Nj = xj, ..., Nn = xn} = xj
		delete Nj {N1 = x1, ..., Nj = xj, ..., Nn = xn} = {N1 = x1, ..., Nn  
= xn}


instance Lacks M {N1 :: a1, ..., Nn :: an} where
		type Extend M a {N1 :: a1, ..., Nn :: an} = {M :: a, N1 :: a1, ...,  
Nn :: an}
		type extend M x {N1 = x1, ..., Nn = xn} = {M = x, N1 = x1, ..., Nn  
= xn}


	instance Disjoint {N1 :: a1, ..., Nn :: an} {M1 :: b1, ..., Mm ::  
bm} where

type Union {N1 :: a1, ..., Nn :: an} {M1 :: b1, ..., Mm :: bm}
= {N1 :: a1, ..., Nn :: an, M1 :: b1, ..., Mm :: bm}
union {N1 = x1, ..., Nn = xn} {M1 = y1, ..., Mm = ym}
= {N1 = x1, ..., Nn = xn, M1 = y1, ..., Mm = ym}

Of course, there are a lot of these (exponential in the number of  
field names!) so you don't really want to generate them all. But  
exactly the same classes (modulo the definition of Constructor, which  
should be hidden anyway) give you extensibility, so any code you  
write will work with either implementation.


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] extensible records using associated types

[Barney Hilken]

Manuel M T Chakravarty:
This is problematic as the instance heads are distinguished only by  
the

context; ie, both instances are for `Lacks m (N a r)'.  Haskell's
instance selection mechanism (with or without associated types)  
selects

instances purely by looking at the arguments of the class; hence, you
cannot use instance context as a kind of guard to guide instance
selection.


A pity. Would resolving instance declarations as Horn clauses be  
useful to deal with any other examples of overlapping instances?



If you don't mind the code for each new label being linear in the  
number of previous labels (so the total code is quadratic in the  
global number of labels) the idea can be rescued.


Get rid of (:<:), and keep the same definitions of Constructor,  
Contains, Lacks, Disjoint and Empty, and the same instances of 'Lacks  
n Empty' and 'Disjoint Empty r'.


For each label 'N', define:

>data N a r = N a r
>
>instance Contains N (N a r) where
>type Project N (N a r) = a  
>type Delete N (N a r) = r   
>project N (N x t) = x   
>delete N (N x t) = t
>
>	instance Disjoint r s, Lacks N (Union r s) => Disjoint (N a r) s  
where

>type Union (N a r) s = Extend N a (Union r s)
>union (N x t) u = extend N x (union t u)

and for each previous label 'M', define:

>instance Contains M r => Contains M (N a r) where
>type Project M (N a r) = Project M r
>type Delete M (N a r) = N a (Delete M r)
>project M (N x t) = project M t 
>delete M (N x t) = N x (delete M t)
>
>instance Lacks M r => Lacks M (N a r) where
>type Extend M b (N a r) = N a (Extend M b r)
>extend M y (N x t) = N x (extend M y t) 
>
>instance Lacks N (M a r) where
>type Extend N b (M a r) = N b (M a r)   
>extend N y (M x t) = N y (M x t)


This saves the bother of fiddling with (:<:) but means that every  
time you import a module which declares labels you would have to  
generate code for the interactions between each new label and each  
existing one.


At least it's not exponential!

Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] extensible records using associated types

[Barney Hilken]

Sorry if people are really bored with this thread, but I thought of  
another advantage of this approach.


Trex (and similar systems) have a limitation that stops you using  
them to define functions with default values. In systems like R (the  
stats package) most functions have a huge number of named parameters  
which usually take default values, but can be changed if necessary.  
In order to define such functions, what you want is an operation  
'update r s' which takes the value of the record 's' (the non-default  
values) for each field which 's' has, and the value of 'r' (the  
default values) for all other fields. The type of 's' should be such  
that it can only have fields which 'r' has, and each such field must  
have the same type, but it doesn't need all the fields of 'r'. The  
type of the result is the same as the type of 'r'.



This can't be typed in Hugs because you can only update particular  
fields, but we can easily add it to (at least the quadratic version  
of) AT-records.


Introduce a class 'subRecord r s' which means that every field of 's'  
is a field of 'r' with the same type:


>class subRecord r s where
>update :: r -> s -> r

The type 'Empty' is a subRecord of everything, and updating by it  
changes nothing:


>instance subRecord r Empty where
>update t Empty = t

For each label 'N' define:

>instance subRecord r s => subRecord (N a r) (N a s) where
>update (N x t) (N y u) = N y (update t u)

For each previous label 'M' define:

>instance subRecord r (M b s) => subRecord (N a r) (M b s) where
>update (N x t) (M y u) = N x (update t (M y u))


There are probably other useful additions to the records system which  
could be coded up in a similar way. In fact, the class 'Disjoint' of  
my original proposal already goes beyond hugs. Until it is clear what  
is useful and what is not, a system like this which requires little  
compiler support has the great advantage that it is easy to change.


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] View patterns in GHC: Request for feedback

[Barney Hilken]

I think you should add the form:

(function -> pattern) @ pattern

as well. The reason you don't need general 'pattern @ pattern' with  
normal patterns is that, if anything is going to match, the two  
patterns must have the same outermost constructor, so you can push  
the @ inside. This doesn't hold for view patterns, and you might well  
want to match against several views.


Of course you can do this with 'both', but the readability is  
terrible, especially if you want to match against more than two  
patterns. Nested 'both' gets extremely long, or do you want to define  
'allThree', 'allFour', ...


The reason I think this might be important is that you could use view  
patterns for records:


(label1 -> x)@(label2 -> y)@(label3 -> z) ...

gives a reasonable syntax for a record pattern, and it would be  
compatible with any form of extensible records.


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Records

[Barney Hilken]

Now that I have a version of ghc with type classes, I have had a go  
at implementing records based on the ideas I mentioned on this list a  
few months ago. The code of my first attempt is available at http:// 
homepage.ntlworld.com/b.hilken/files/Records.hs


I am releasing this to get feedback. I think Haskell needs a records  
system of this kind of generality, and this code at least allows you  
to play around.


From the comment section of the file:
---

Record construction:

EmptyRecis the empty record.
N =: x  is the record with one field labelled N  
carrying data x.
t +: u  is the union of records t and u. Any overlap  
of labels gives a static error.


Record destruction:

t .: N  is the value of field N in record t. A lack  
of field N gives a static error.
t -: N  is record t with field N deleted. A lack of  
field N gives a static error.


Record update:

t |: u  is the record with fields from u where it  
has them, t otherwise. If u has
any fields not in t, or of different types  
from t, there is a static error.

Note that the result has the same type as t.

All these records have types:

EmptyRecis the type of the empty record.
N :=: a is the type of a record with one field  
labelled N carrying data of type a.
r :+: s is the union of record types r and s. Any  
overlap of labels gives a static error.
r :.: N is the type of field N in a record of type  
r. A lack of field N gives a static error.
r :-: N is record type r with field N deleted. A  
lack of field N gives a static error.


Finally some classes to govern the polymorphism:

r `Contains` N  means that r is a record type with a  
field labelled N.
r `Disjoint` s  means that r and s are record types with  
no fields in common.
r `Subrecord` s means that r and s are record types, and  
every field of r also occurs in s (with the same type).


The types of the basic operators are as follows:

(=:) :: n -> a -> n :=: a
(+:) :: r `Disjoint` s => r -> s -> r :+: s
(.:) :: r `Contains` n => r -> n -> r :.: n
(-:) :: r `Contains` n => r -> n -> r :-: n
(|:) :: r `Subrecord` s => s -> r -> s

--

Note that these records are a lot more expressive than the Hugs  
system, as you can not only extend records by adding fields, but also  
take unions of arbitrary (disjoint) records.


Record update is designed for functions with lots of named optional  
arguments. If you define


f opts = ... options.:Optj ...
where
options = (Opt1 =: val1 +: ... +: Optn =: valn) |: opts

then the user can write (for example):

f (Optk =: u +: Optl =: v)

to set just two of the options, leaving the rest as default. This  
also cannot be done in the Hugs system.



The main disadvantage of the current implementation is that you have  
to tell the compiler in which order to store the fields, by defining  
one of the following:


   type instance NameCmp N M = NameLT
   type instance NameCmp N N = NameEQ
   type instance NameCmp N M = NameGT

for each pair of labels N & M in such a way as to give a linear order  
on labels. You need n^2 definitions, where n is the number of labels.  
I would do this in Template Haskell, but it won't yet allow you to  
declare type instances. Maybe some compiler support?


Error messages tend to be cryptic. They mostly complain of missing  
instances, and can run to several pages. There is really no way to  
improve this without building it all in to the compiler!



All comments gratefully received, including suggestions on syntax,  
choice of operators, implementation, explanation, etc.



Barney.


___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Re: [Haskell-cafe] PROPOSAL: Rename haskell@ to haskell-announce@

[Barney Hilken]

From: Isaac Dupree
I haven't been able to see how it makes sense to subscribe to  
haskell@ but not haskell-cafe -- because if a discussion interested  
you, and went in-depth, you might want to be able to read the whole  
thread!  (It is possible to read the archives, but that doesn't  
help if you're inspired to _reply_ to the thread...)


This is exactly what I do. I subscribe to haskell so as not to miss  
anything important, and when something I'm interested in moves to  
haskell-cafe, I use gmane. I think most of the people complaining  
about this issue do the same.


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Extensible records: Static duck typing

[Barney Hilken]

Everyone wants to add extensible records to Haskell. The problem is  
that, in a formally defined language like Haskell, we need to agree  
how they should behave, and there are too many conflicting ideas.


I was involved recently in an attempt to try to sort out some of the  
alternatives (recorded here: http://hackage.haskell.org/trac/ghc/wiki/ExtensibleRecords) 
 which collapsed because of argument over a fundamental question:


	Should {label := "Hi", color := blue} and {color := blue, label :=  
"Hi"} have the same type?


One of the main contributors felt that the answer was no (because it  
allows more different records to be represented, and makes  
implementation simpler), and that we should say so. I felt that most  
people would consider that the answer was yes, and that we shouldn't  
make such a fundamental design decision without some evidence about  
what is best in practice.


The result was that our attempt to sort things out stopped.

This sort of disagreement means that nothing gets done. After my  
experience with the wiki page, I don't believe anything will get done  
until one of the core ghc developers makes some arbitrary decisions  
and implements whatever they want to, which will then eventually  
become part of the standard by default.


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Extensible records: Static duck typing

[Barney Hilken]

The scoped labels paper has an interesting feature in this regard:
labels with different names can be swapped at will, but labels having
the same name (which is allowed) maintain their order.

- Cale


Yes, I know. The problem is that there are TOO MANY proposals, and  
they are all fundamentally incompatible. The scoped labels idea is  
interesting, but is it useful? No-one has written enough code with ANY  
of the proposals to say what their strengths and weaknesses are.


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Extensible records: Static duck typing

[Barney Hilken]

new record (x = 3,y = 4)
subtraction \r -> ( x = 3 | r - x)
replacement \r -> (x := 3 | r) (equivalent to the above)
type (x::Int,y::Char)

degenerate cases:
empty record (|)
subtracting a label (| r - x)

a record can always be determined by the presence of a '|' within
parenthesis.



One of the advantages of the systems with richer polymorphism and more  
predicates is that they need less syntax. It is possible (once you  
have solved the permutation/scoping problem) to use constructors as  
labels, and define all the basic operators on records as standard  
Haskell functions. With this approach you can even treat labels as  
"first-class citizens" and write polymorphic record zip:


	labelZip :: ({n :: a} `Disjoint` {m :: b}) => n -> m -> [a] -> [b] ->  
[{n :: a, m :: b}]

labelZip n m = zipWith (\x y -> {n := x, m := y})

But no-one knows whether this extra expressive power has an  
unacceptable cost in terms of extra complexity, because no-one has  
implemented and used these systems seriously.


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Extensible records: Static duck typing

[Barney Hilken]

2. List the possible features that “records” might mean.  For example:

· Anonymous records as a type.  So {x::Int, y::Bool} is a  
type.  (In Haskell as it stands, records are always associated with  
a named data type.


· Polymorphic field access.  r.x accesses a field in any  
record with field x, not just one record type.


· Polymorphic extension

· Record concatenation

· Are labels first-class?

· etc

Give examples of why each is useful.   Simply writing down these  
features in a clear way would be a useful exercise.  Probably some  
are “must have” for some people, but others might be optional.


This is what I was trying to do with the wiki page. I stopped because  
the only other contributor decided he could no longer contribute, and  
I felt I was talking to myself. If we want to be rational about the  
design, we need real examples to demonstrate what is genuinely useful,  
and I don't have that many of them.


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] RE: Extensible records: Static duck typing

[Barney Hilken]

What about just implementing the cheapest solution that still gets  
us most

of the way?


(3) If it is as cheap (to implement) as advertised then there is no  
great

risk involved. If it turns out the missing features are a great
show-stopper for some people (which I don't believe) then let them  
present
their case afterwards, with good examples at hand. We can still  
decide to

aim for a higher goal in the long term.



If in doubt, chose the solution that is easier to implement.


Since this paper, there have been several proposals which can be 90%  
implemented as libraries, using either functional dependencies or  
associated types. These all have much more expressive type systems  
than the SPJ paper, yet need very little compiler support. The  
question is, which one (if any) should get this small but necessary  
support?


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Re: RE: Extensible records: Static duck typing

[Barney Hilken]

Begin forwarded message:


From: Ben Franksen <[EMAIL PROTECTED]>
Date: 18 February 2008 21:32:29 GMT
To: haskell@haskell.org
Could you be more specific? Which proposals exactly do you mean and  
where

can I read more about them?


Hlist is one of the ones | was thinking of. Two more are "poor man's  
records" a.k.a. Data.Record.hs, whose author certainly believes it  
should be the basis for the new system, and my own system,  
downloadable from http://homepage.ntlworld.com/b.hilken/files/Records.hs


There is a discussion of the various possibilities on the wiki
http://hackage.haskell.org/trac/ghc/wiki/ExtensibleRecords
which you are encouraged to contribute to!

Sorry about the lack of response on cafe, but I only read that when  
people say they are moving their discussion there.


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Re: Re: RE: Extensible records: Static duck typing

[Barney Hilken]

My rationale for these criteria goes like this: efficient access is
necessary if we want to compete with the much simpler record systems  
in
mainstream languages. If records are not as light-weight  
(syntactically as

well as wrt run-time performance) as 'normal' Haskell data types, then
people will be reluctant to use them, especially in library APIs.  
Finally,

having to wait for highly experimental additional extensions to be
available, tried, and tested, would only help to indefinitely post- 
pone the

introduction of a usable record system.


I totally disagree. The great strength of Haskell is that, whenever  
important design decisions have been made, the primary consideration  
has not been practicality, but generality and mathematical foundation.  
When the Haskell committee first started work, many people said lazy  
evaluation was an academic curiosity: mathematically right, but far  
too inefficient for real programs. When Haskell adopted type classes,  
people said they were far too heavy a machinery to solve the  
relatively simple problems of equality, show and numbers. In each case  
the more general, abstract approach has shown enormous advantages in  
the long term. I'm sure the same will be true of associated types,  
which are a lot more complex than functional dependencies, but also  
more general, and more mathematical.


My criteria for choosing a record system would be: continue with the  
philosophy which has served Haskell so well up to now. In other words,  
choose the system which is most general and most mathematically sound;  
get some kind of implementation working so that we can get some  
experience with using it; then worry about efficiency later.


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Re: Re: RE: Extensible records: Static duck typing

[Barney Hilken]

While I agree with your general argument, I wonder if you realize
that functional dependencies have a strong, general, and elegant
mathematical foundation that long predates their use in Haskell?
If you want even a brief glimpse, there's s short article at
http://en.wikipedia.org/wiki/Functional_dependencies that might
give you some ideas.  The mathematics of functional dependencies
plays an important role in the theory of relational databases.

I don't know what you consider as the mathematical foundations
for associated types, nor do I know why you consider that to be
either more general or more "mathematical" (whatever that means)
but I hope you'll enjoy the material on functional dependencies.


I admit I was being unfair on fundeps in calling them less  
mathematical. Nonetheless, something about their addition to Haskell  
grates on my mathematical sensitivities. They feel "bolted on" in a  
way that associated types don't. Probably this is because of my own  
bias which leads me to see Haskell as a subset of dependent type  
theory, and ATs as some kind of sigma type (though I've never tried to  
make this precise).


Barney.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Records in Haskell

[Barney Hilken]

(sorry, I meant to send this to the list, but only sent it to Wolfgang)

Here is my understanding of the current state of the argument:

Instead of Labels, there will be a new kind String, which is not a subkind of 
*, so its elements are not types. The elements of String are strings at the 
type level, written just like normal strings. If you want labels, you can 
define them yourself, either empty:

data Label (a :: String)

or inhabited

data Label (a :: String) = Label

these definitions give you a family of types of the form Label "name", in the 
first case empty (except for undefined), in the second case inhabited by a 
single element (Label :: Label "name")


There are several similar proposals for extensible records defined using 
labels, all of which (as far as I can see) could be defined just as easily 
using the kind String. There is also a proposal for nonextensible records, 
using the same techniques, which has (almost) converged with Simon's latest 
version of TDNR records. The problem with all of these is dealing with 
higher-rank field types: the current implementation of impredicative 
polymorphism isn't general enough to allow update of polymorphic fields.


It seems to me that, if we could solve the (hard) impredicativity problem, we 
would be very close to a design which would
1. be compatible with existing code
2. allow field names to be polymorphic
3. make the future addition of extensible records possible
The question is, should we wait till someone solves the impredicativity 
problem, or go ahead with a cludgy design now?


Barney.


___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Higher types in contexts

[Barney Hilken]

Is there any deep reason why I can't write a polymorphic type in a context? I 
think the record update problem can be (sort of) solved if you could write:

class Has r Rev (forall a. [a] -> [a]) => HRClass r where
setHRClass :: (forall a.[a] -> [a]) -> r -> r

but polymorphic types are not allowed in contexts. Is this one of the problems 
SPJ considers "Hard" or is it a feasible extension?

Barney.


___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Records

[Barney Hilken]

Extensible records for Haskell
--

A proposal for extensible records which is compatible with type
classes and constructor classes, and has a type inference algorithm.
Based on ideas of Sean Bechhofer and implemented within Mark Jones'
'Qualified Types'.

    Barney Hilken   and Giuliano Procida


This is a proposal for an expressive record language. Records are
first class values and can be manipulated by the extraction, addition
and deletion of named fields. Polymorphism is allowed over the types
of fields and over all fields not explicitly mentioned.

This record system is not based on subtyping. Instead, the necessary
constraints on polymorphism are expressed as predicates on types. This
means that Mark Jones' type inference algorithm extends to record
types.

In what follows we present one possible syntax for the record values,
types and predicates. The importance of our proposal is not the
particular syntax, but the logical structure of the type system, and
the way it integrates with type classes.




-- Labels --

Records are collections of named fields. Because of the limits of
namespace, it is necessary to declare which identifiers are to be
considered field names. The declaration

> label A1, ..., An

introduces field names or `labels' A1, ..., An. This also helps in
finding common errors such as typos.


-- Fixed records --

Fixed records are just ML records; their types include complete
information about the types of the fields. The expression

(A1 is v1, ..., An is vn)

denotes a record with fields labelled A1, ..., An containing values
v1, ..., vn respectively. The order of fields is not significant.
This expression has type

(A1 is t1, ..., An is tn)

where v1 :: t1, ..., vn :: tn, following the Haskell convention that
types have the same form as their values. The same expression can be
used as a pattern:

> f (A1 is x1, ..., an is xn) = rhs

where rhs can refer to variables x1, ..., xn.


-- Predicates --

Extensible records use the `predicates' of the type class mechanism to
allow record polymorphism. For each collection of labels A1, ..., An
there is a predicate

Lacks A1, ..., An r

which says that r is a record type with no `Ai' fields (r must be a
constructor variable of kind *). It satisfies

Lacks A1, ..., An r => Lacks B1, ...,Bm r

for any the subset Bi of the Ai. Note that

Lacks A1 r ... Lacks An r => Lacks A1, ..., An r

also holds. For aesthetic reasons, the abbreviation

Rec r

is used when n=0. It says simply that r is a record type.


-- Indeterminate record types --

For each label A there are type constructors

()::: *
add A ::: * -> * -> *
del A ::: * -> *

satisfying

Lacks A ()
Lacks A r => Rec (add A t r)
Rec r => Rec (del A r)

Given a type t and a record type r with no A field, add A t r
constructs the type of records with all the fields of r, and
additionally, an A field of type t. When applied to an appropriate
fixed record type:

   add A1 t1 (A2 is t2, ..., An is tn) = (A1 is t1, A2 is t2, ..., An is tn)

In this way fixed record types may be considered as successive
applications of add constructors to the null record type.

Given any record type r, del A r constructs the type of records which
do not have an A field, but are otherwise like r. If r does not have
an A field, then del A r = r.

If r is an indeterminate record type (possibly a simple type variable)
then add A t r is also an indeterminate record type, likewise del A
r. There may be many different ways of expressing the same record
type.


-- Polymorphic record operations --

For each label A there are three functions

A   :: Lacks A r => add A t r -> t
add A   :: Lacks A r => t -> r -> add A t r
del A   :: Rec r => r -> del A r

of extraction, extension and deletion:

Aj (A1 is v1, ..., An is vn) = vj
add A1 v1 (A2 is v2, ..., An is vn) = (A1 is v1, A2 is v2, ..., An is vn)
del A1 (A1 is v1, ..., An is vn) = (A2 is v2, ..., An is vn)
del B (A1 is v1, ..., An is vn) = (A1 is v1, ..., An is vn)

The type system protects against failure and name-clash by insisting
that a field exists before it is extracted, and is absent before it is
added. Deletion does not require the existence of the field as this is
more expressive.

Partial pattern matching is also possible:

> f (A1 is x1, ..., An is xn | y) = rhs

If xj has type tj, y has type u and rhs has type v then

f :: Lacks A1, ..., An u => add A1 t1 (... add An tn u) -> v


-- Copatterns --

Pattern matching can be duallized in a useful way for record
definition. The equations

> A1 x = rhs1
   .
   .
   .
> An x = rhsn

(where rhsj has type tj) define record

x :: (A1 is t1, ..., An is tn)

with field Aj given by rhsj. Thi