Proposal: FirstClassFieldUpdates

[Jon Fairbairn]

Simon Peyton-Jones <simonpj at microsoft.com>
writes:

> | Proposal: FirstClassFieldUpdates
> | 
> | Summary: Add some syntax that makes field updates into
> | functions.
>
> I'm wary about occupying too much "syntactic space" with
> Haskell's named-field notation. If you had a keyword, like
> update { foo = bar } meaning \x. x { foo = bar } that'd get
> you into a new syntactic space.

It'd also make the syntax too noisy to be of any interest.

> But braces alone are so precious that I'm not sure that record
> updates justify consuming them.

I'm not particularly wedded to braces, it's simply that they are
the syntax already used for updates, so to make updates first
class that is the obvious choice.

For first class updates I'd be happy with something like “foo :=
bar”, but then I would want the syntax of record construction to
be something similar.

For some reason, the use of braces in record syntax differs from
all others I can think of: all the rest are x {something;
something; something} and can replaced by layout. So braces
(with commas) for records at all is an irregularity.

>
> On a related matter, people want to use record syntax for
> GADTs and existentials. For record selection and
> construction these are more or less fine (ie one can make a
> sensible spec). But record update is another matter. Haskell
> 98 says that record update can change the type of a record
> (contrary to some posts in this thread), but the
> specification becomes really rather tricky for GADTs and
> existentials. Indeed, I was going to propose that in H Prime
> we might consider making update *not* change the type,
> backing away from the current H98 story, but one that makes
> the spec a lot easier. But various people have been arguing
> in favour of the H98 story so I may have an uphill struggle!

I'm coming back to this stuff rather late; I can't say I
understand the interactions between GADTs, existentials and
records. In the absence of those developments what I would have
liked to have seen would have been a decomposition of data
declarations and the resulting types into orthogonal parts. For
one thing, allowing “Constr a b c” for construction and pattern
matching on something that was declared as “Constr {x::A, y::B,
z::C}” looks improper to me, and another is the restricted
nature of Haskell’s union types (cf what I started to talk about
at AngloHaskell; see
<http://www.cl.cam.ac.uk/~jf15/Haskell-notes/AngloHaskell2009-Not-Talk.xhtml>
for some notes on that)

So the outline would be (forgive the poor choice of keywords
here):

1. distinguishable types

The type “dtype Constr T1 T2…” would correspond to a single
alternative of a data declaration (dtype is just an arbitrary
keyword from distinguishable type). The idea is that two dtypes
only match if their (fully qualified) constructors match.

2. Symmentric unions of distinguishable types

A type (dtype1 | dtype2 | …) corresponds to the alternatives of
a data declaration. Note that “|” can only be used on
distinguishable types (and unions of distinguishable types). So
a non-record-syntax data declaration

data Widget = Thing1 A | Thing2 B | …

could still be valid but now be a shorthand for 

type Widget = dtype Thing1 A | dtype Thing2 B | …

One of the benefits of this is that the type of anything can be
written down without having to refer to any declarations.

3. Once that is done, we can come up with a design for records:

field1:=x . field2:=y . … $ emptyRecord

Now “field:=x”; is a first class function, polymorphic on all
records that have “field” as a field. We might want to choose
some nicer syntax for emptyRecord, (“{}” if you like), but the
only other expression syntax needed is the pseudo operator “:=”,
though some syntax for the types would need to be designed.
“record (field1::Type1, …)” would do, with “record ()” for the
empty record. There is no /need/ to use up precious braces ;-).

* * *

You’ll complain that this isn’t fully worked out, and as I say,
I don’t know how it interacts with GADTs and other things I’m
not up to date with. But as far as I remember, I could simulate
all of this in Ponder’s type system, so it shouldn’t be too hard
for someone au fait with the way things are currently done to
specify it properly.

-- 
Jón Fairbairn                                 Jon.Fairbairn at cl.cam.ac.uk