记录的点语法（Dot syntax for records）

简而言之，.field 是一个后缀投影操作符，其结合优先级高于函数应用。

词法结构（Lexical structure）

.foo 是一个合法名称，表示记录字段（新的 Name 构造器 RF "foo"）
以大写字母 F 开头的 Foo.bar.baz 是一个词素，即带命名空间的标识符：DotSepIdent ["baz", "bar", "Foo"]
以小写字母 f 开头的 foo.bar.baz 是三个词素：foo、.bar、.baz
.foo.bar.baz 是三个词素：.foo、.bar、.baz
如果你想要 Constructor.field，必须写成 (Constructor).field。
所有模块名必须以大写字母开头。

`simpleExpr` 的新语法

结合优先级高于应用（simpleExpr）的表达式，如变量或括号表达式，现在被称为 simplerExpr，并插入了一层新的语法。

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

(.foo) 是一个名称，因此你可以用它来定义一个名为 .foo 的函数（见下方的 .squared）
(.foo.bar) 是一个括号表达式

语法糖展开规则（Desugaring rules）

(.field1 .field2 .field3) 会被展开为 (\x => .field3 (.field2 (.field1 x)))
(simpleExpr .field1 .field2 .field3) 会被展开为 ((.field .field2 .field3) simpleExpr)

记录展开（Record elaboration）

新增了一个编译指示 %prefix_record_projections，默认开启（on）
对于记录 R 的每个字段 f，我们会得到：
- 命名空间 R 下的投影 f``（与现在一致），除非 ``%prefix_record_projections 被关闭（off）
- 命名空间 R 下的投影 .f，定义相同

示例代码（Example code）

record Point where
  constructor MkPoint
  x : Double
  y : Double

该记录会生成两个投影：* .x : Point -> Double * .y : Point -> Double

由于 %prefix_record_projections 默认开启，还会得到：* x : Point -> Double * y : Point -> Double

为避免短标识符污染全局命名空间，可以这样做：

%prefix_record_projections off

record Rect where
  constructor MkRect
  topLeft : Point
  bottomRight : Point

对于 Rect，不会生成前缀投影：

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

我们来定义一些常量：

pt : Point
pt = MkPoint 4.2 6.6

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

用户自定义的投影同样有效。（应该这样吗？）

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

最后，来看一些示例：

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 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]