Dot syntax for records

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: DotSepIdent ["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 PPostfixAppPartial
             | simplerExpr (.field)+   -- parses as PPostfixApp
             | 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 %prefix_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 %prefix_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 %prefix_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:

%prefix_record_projections off

record Rect where
  constructor MkRect
  topLeft : Point
  bottomRight : Point

For Rect, we don’t get the prefix 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 $ ({ topLeft.x := 3 } rect).topLeft.x

  -- but for compatibility, we support the old syntax, too
  printLn $ ({ topLeft->x := 3 } rect).topLeft.x

  -- prints 2.1
  printLn $ ({ topLeft.x $= (+1) } rect).topLeft.x
  printLn $ ({ 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]