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 (newName
constructorRF "foo"
)Foo.bar.baz
starting with uppercaseF
is one lexeme, a namespaced identifier:DotSepIdent ["baz", "bar", "Foo"]
foo.bar.baz
starting with lowercasef
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 ison
by default - for every field
f
of a recordR
, we get:- projection
f
in namespaceR
(exactly like now), unless%prefix_record_projections
isoff
- projection
.f
in namespaceR
with the same definition
- projection
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]