diff --git a/language/Records.md b/language/Records.md
index 5bb0add..c15d03c 100644
--- a/language/Records.md
+++ b/language/Records.md
@@ -20,13 +20,36 @@ Fields of records can be accessed using a dot, followed by the label of the fiel
 ["Functional Programming","JavaScript"]
 ```
 
+Type synonyms for record types are created with the `type` keyword:
+
+```purs
+type Point =
+  { x :: Number
+  , y :: Number
+  }
+```
+
 ## Kinds
 
-`{ ... }` is just syntactic sugar for the `Record` type constructor, so `{ language ::  String }` is the same as `Record ( language :: String )`.
+`{ ... }` is syntactic sugar for the `Record` type constructor. This type constructor is parameterized by a row of types:
 
-The Record type constructor is parameterized by a row of types. In kind notation, `Record` has kind `Row Type -> Type`. That is, it takes a row of types to a type.
+```purescript
+-- these types are equivalent
+type Language = { language :: String }
+type Language' = Record ( language :: String )
+```
 
-`( language :: String )` denotes a row of types (something of kind `Row Type`), so it can be passed to `Record` to construct a type, namely `Record ( language :: String )`.
+A `Record` is constructed from a row type and represents a product type in which all fields in the row type are present. Using kind notation, `Record` has the kind `Row Type -> Type` -- that is, it takes a row of types and produces a type.
+
+Because `( language :: String )` denotes a row of types (and therefore has the kind `Row Type`), it can be passed to the `Record` constructor or to the `{ ... }` syntax for `Record` to construct a type:
+
+```purescript
+type LanguageRow = ( language :: String ) -- has kind Row Type
+
+-- these are equivalent
+type Language = Record LanguageRow
+type Language' = { | LanguageRow }
+```
 
 ## Extending Records
 
@@ -79,6 +102,61 @@ A record update function can also be defined by using an `_` inplace of the reco
 _ { fieldName = newValue }
 ```
 
+## Record Puns
+
+_Record puns_ enable concise code when record fields have the same name as other values. This feature is useful for constructing records and pattern matching.
+
+### Constructing
+
+```purs
+origin :: Point
+origin = { x, y }
+-- origin = { x: x, y: y } -- Equivalent
+  where
+    x = 0.0
+    y = 0.0
+```
+
+### Pattern Matching
+
+```purs
+showPoint :: Point -> String
+showPoint { x, y } = show x <> ", " <> show y
+-- showPoint { x : x, y : y } = show x <> ", " <> show y -- Equivalent
+```
+
+### Not for Record Updates
+
+Note that puns may not be used for record updates.
+
+```purescript
+setX :: Number -> Point -> Point
+setX x point = point { x = x }
+-- setX x point = point { x } -- Not allowed
+```
+
+## Further Record Operations
+
+The [`record`](https://pursuit.purescript.org/packages/purescript-record) package enables additional record operations, such as `merge`, `union`, and efficient ways to create records (see [Record.Builder](https://pursuit.purescript.org/packages/purescript-record/docs/Record.Builder)).
+
+Here's an example of using the `disjointUnion` function to add a `z` field to a `Point` record. The `to3d` function merges the original record `p` with another record `{ z }` created from this new `Number`:
+
+```purescript
+import Record (disjointUnion)
+
+type Point3d =
+  { x :: Number
+  , y :: Number
+  , z :: Number
+  }
+
+to3d :: Point -> Number -> Point3d
+to3d p z = disjointUnion p { z }
+
+-- Equivalent to:
+to3d p z = { x: p.x, y: p.y, z }
+```
+
 ## Field Names
 
 Symbols which are illegal value identifiers, such as title-cased identifiers or ones containing spaces, can be used to identify a field by enclosing it in double-quotes: