mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 00:10:31 +03:00
196 lines
4.9 KiB
ReStructuredText
196 lines
4.9 KiB
ReStructuredText
Dot syntax for records
|
|
======================
|
|
|
|
.. role:: idris(code)
|
|
:language: idris
|
|
|
|
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.
|
|
|
|
.. code-block:: idris
|
|
|
|
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
|
|
------------
|
|
|
|
.. code-block:: idris
|
|
|
|
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:
|
|
|
|
.. code-block:: idris
|
|
|
|
%prefix_record_projections off
|
|
|
|
record Rect where
|
|
constructor MkRect
|
|
topLeft : Point
|
|
bottomRight : Point
|
|
|
|
For ``Rect``, we don't get the prefix projections:
|
|
|
|
.. code-block:: idris
|
|
|
|
Main> :t topLeft
|
|
(interactive):1:4--1:11:Undefined name topLeft
|
|
Main> :t .topLeft
|
|
\{rec:0} => .topLeft rec : ?_ -> Point
|
|
|
|
Let's define some constants:
|
|
|
|
.. code-block:: idris
|
|
|
|
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?)
|
|
|
|
.. code-block:: idris
|
|
|
|
(.squared) : Double -> Double
|
|
(.squared) x = x * x
|
|
|
|
Finally, the examples:
|
|
|
|
.. code-block:: idris
|
|
|
|
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
|
|
|
|
-- but for compatibility, we support the old syntax, too
|
|
printLn $ (record { topLeft->x = 3 } rect).topLeft.x
|
|
|
|
-- prints 2.1
|
|
printLn $ (record { topLeft.x $= (+1) } rect).topLeft.x
|
|
printLn $ (record { topLeft->x $= (+1) } rect).topLeft.x
|
|
|
|
Parses but does not typecheck:
|
|
|
|
.. code-block:: idris
|
|
|
|
-- 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]
|