[Haskell] extensible records using associated types
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
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
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
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
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
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
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@
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
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
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
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
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
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
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
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
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
(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
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
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