RFC: Dot syntax for records

[ziman]

Here's one way of doing it. I mostly wanted to hack up something to start a discussion from (and to toy with) so my choices are definitely not final or anything. But they seem to work together.

Discussion and suggestions on any aspect are welcome.

Overview

Long story short, .field is a postfix projection operator that binds tighter than function application.

Lexical structure:

• .foo is a valid name, which stands for record fields (new Name constructor RF "foo")
• Foo.bar.baz starting with uppercase F is one lexeme, a namespaced identifier: NSIdent ["baz", "bar", "Foo"]
• foo.bar.baz starting with lowercase f is three lexemes: foo, .bar, .baz
• .foo.bar.baz is three lexemes: .foo, .bar, .baz
• If you want Constructor.field, you have to write (Constructor).field.
• All module names must start with an uppercase letter.

New syntax of simpleExpr:

Expressions binding tighter than application (simpleExpr), such as variables or parenthesised expressions, have been renamed to simplerExpr, and an extra layer of syntax has been inserted.

simpleExpr ::= (.field)+               -- parses as PRecordProjection
             | simplerExpr (.field)+   -- parses as PRecordFieldAccess
             | simplerExpr             -- (parses as whatever it used to)

• (.foo) is a name, so you can use it to e.g. define a function called .foo (see .squared below)
• (.foo.bar) is a parenthesised expression

Desugaring rules

• (.field1 .field2 .field3) desugars to (\x => .field3 (.field2 (.field1 x)))
• (simpleExpr .field1 .field2 .field3) desugars to ((.field .field2 .field3) simpleExpr)

Record elaboration

• there is a new pragma %undotted_record_projections, which is on by default
• for every field f of a record R, we get:
  • projection f in namespace R (exactly like now), unless %undotted_record_projections is off
  • projection .f in namespace R with the same definition

Example code

record Point where
  constructor MkPoint
  x : Double
  y : Double

This record creates two projections:

• .x : Point -> Double
• .y : Point -> Double

Because %undotted_record_projections are on by default, we also get:

• x : Point -> Double
• y : Point -> Double

To prevent cluttering the ordinary global name space with short identifiers, we can do this:

%undotted_record_projections off

record Rect where
  constructor MkRect
  topLeft : Point
  bottomRight : Point

For Rect, we don't get the undotted projections:

Main> :t topLeft
(interactive):1:4--1:11:Undefined name topLeft
Main> :t .topLeft
\{rec:0} => .topLeft rec : ?_ -> Point

Let's define some constants:

pt : Point
pt = MkPoint 4.2 6.6

rect : Rect
rect =
  MkRect
    (MkPoint 1.1 2.5)
    (MkPoint 4.3 6.3)

User-defined projections work, too. (Should they?)

(.squared) : Double -> Double
(.squared) x = x * x

Finally, the examples:

main : IO ()
main = do
  -- desugars to (.x pt)
  -- prints 4.2
  printLn $ pt.x

  -- prints 4.2, too
  -- maybe we want to make this a parse error?
  printLn $ pt .x

  -- prints 10.8
  printLn $ pt.x + pt.y

  -- works fine with namespacing
  -- prints 4.2
  printLn $ (Main.pt).x

  -- the LHS can be an arbitrary expression
  -- prints 4.2
  printLn $ (MkPoint pt.y pt.x).y

  -- user-defined projection
  -- prints 17.64
  printLn $ pt.x.squared

  -- prints [1.0, 3.0]
  printLn $ map (.x) [MkPoint 1 2, MkPoint 3 4]

  -- .topLeft.y desugars to (\x => .y (.topLeft x))
  -- prints [2.5, 2.5]
  printLn $ map (.topLeft.y) [rect, rect]

  -- desugars to (.topLeft.x rect + .bottomRight.y rect)
  -- prints 7.4
  printLn $ rect.topLeft.x + rect.bottomRight.y

  -- qualified names work, too
  -- all these print 4.2
  printLn $ Main.Point.(.x) pt
  printLn $ Point.(.x) pt
  printLn $ (.x) pt
  printLn $ .x pt

  -- haskell-style projections work, too
  printLn $ Main.Point.x pt
  printLn $ Point.x pt
  printLn $ (x) pt
  printLn $ x pt

  -- record update syntax uses dots now
  -- prints 3.0
  printLn $ (record { topLeft.x = 3 } rect).topLeft.x

  -- prints 2.1
  printLn $ (record { topLeft.x $= (+1) } rect).topLeft.x

Parses but does not typecheck:

  -- parses as: map.x [MkPoint 1 2, MkPoint 3 4]
  -- maybe we should disallow spaces before dots?
  --
  printLn $ map .x [MkPoint 1 2, MkPoint 3 4]

[edwinb]

I think this is lovely, and a feature that has been occasionally requested but nobody has thought through how it would fit with the rest of the language until now. Thanks for doing it!

As far as I can see, the only thing that's incompatible with existing code is the requirement for an upper case letter at the start of a module name, which is a convention that people seem to use anyway. And we've kind of committed to the case of the initial letter having some meaning already anyway, so I'm not worried about that new requirement.

I'll leave this a little bit for any further comments, but I think I'm happy to merge if you think it's ready to go.

[jfdm]

To be that person, once this PR has been merged then let's take @ziman original comment explaining the change and add it to the documentation!

[edwinb]

Hmm, the test failure here is odd. Is it related to the recent patch to fix number display?

I have one more annoying request (sorry!) - please could you add the details to the CHANGELOG? Just to say record dot syntax is added is fine, I'll refine it later with a link to the docs. Not that that's stopping the merge, but I'd like to encourage the habit in everyone now that we've had a releaase :).

[edwinb]

Oh dear, my occurs check fix broke the test output here. Let's see if I've fixed the conflicts successfully...

[edwinb]

Apparently I didn't. I'm going to merge anyway and then push a fix. Thanks for your work on this!