# A Quickie: Manipulating Records in Amulet

Amulet, unlike some other languages, has records figured out. Much like in ML (and PureScript), they are their own, first-class entities in the language as opposed to being syntax sugar for defining a product constructor and projection functions.

### Records are good

Being entities in the language, it’s logical to characterize them by their introduction and elimination judgements^{1}.

Records are introduced with record literals:

\[ \frac{ \Gamma \vdash \overline{e \downarrow \tau} }{ \Gamma \vdash \{ \overline{\mathtt{x} = e} \} \downarrow \{ \overline{\mathtt{x} : \tau} \} } \]

And eliminated by projecting a single field:

\[ \frac{ \Gamma \vdash r \downarrow \{ \alpha | \mathtt{x} : \tau \} }{ \Gamma \vdash r.\mathtt{x} \uparrow \tau } \]

Records also support monomorphic update:

\[ \frac{ \Gamma \vdash r \downarrow \{ \alpha | \mathtt{x} : \tau \} \quad \Gamma \vdash e \downarrow \tau }{ \Gamma \vdash \{ r\ \mathtt{with\ x} = e \} \downarrow \{ \alpha | \mathtt{x} : \tau \} } \]

### Records are.. kinda bad?

Unfortunately, the rather minimalistic vocabulary for talking about records makes them slightly worthless. There’s no way to extend a record, or to remove a key; Changing the type of a key is also forbidden, with the only workaround being enumerating all of the keys you *don’t* want to change.

And, rather amusingly, given the trash-talking I pulled in the first paragraph, updating nested records is still a nightmare.

```
> let my_record = { x = 1, y = { z = 3 } }
my_record : { x : int, y : { z : int } }
> { my_record with y = { my_record.y with z = 4 } }
_ = { x = 1, y = { z = 4 } }
```

Yikes. Can we do better?

### An aside: Functional Dependencies

Amulet recently learned how to cope with functional dependencies. Functional dependencies extend multi-param type classes by allowing the programmer to restrict the relationships between parameters. To summarize it rather terribly:

```
(* an arbitrary relationship between types *)
class r 'a 'b
(* a function between types *)
class f 'a 'b | 'a -> 'b
(* a one-to-one mapping *)
class o 'a 'b | 'a -> 'b, 'b -> 'a
```

### Never mind, records are good

As of today, Amulet knows the magic `row_cons`

type class, inspired by PureScript’s class of the same name.

```
class
row_cons 'record ('key : string) 'type 'new
| 'record 'key 'type -> 'new (* 1 *)
, 'new 'key -> 'record 'type (* 2 *)
begin
val extend_row : forall 'key -> 'type -> 'record -> 'new
val restrict_row : forall 'key -> 'new -> 'type * 'record
end
```

This class has built-in solving rules corresponding to the two functional dependencies:

- If the original
`record`

, the`key`

to be inserted, and its`type`

are all known, then the`new`

record can be solved for; - If both the
`key`

that was inserted, and the`new`

record, it is possible to solve for the old`record`

and the`type`

of the`key`

.

Note that rule 2 almost lets `row_cons`

be solved for in reverse. Indeed, this is expressed by the type of `restrict_row`

, which discovers both the `type`

and the original `record`

.

Using the `row_cons`

class and its magical methods…

- Records can be extended:

- Records can be restricted:

And, given a suitable framework of optics, records can be updated nicely:

### God, those are some ugly types

It’s worth pointing out that making an optic that works for all fields, parametrised by a type-level string, is not easy or pretty, but it is work that only needs to be done once.

```
type optic 'p 'a 's <- 'p 'a 'a -> 'p 's 's
class
Amc.row_cons 'r 'k 't 'n
=> has_lens 'r 'k 't 'n
| 'k 'n -> 'r 't
begin
val rlens : strong 'p => proxy 'k -> optic 'p 't 'n
end
instance
Amc.known_string 'key
* Amc.row_cons 'record 'key 'type 'new
=> has_lens 'record 'key 'type 'new
begin
let rlens _ =
let view r =
let (x, _) = Amc.restrict_row @'key r
x
let set x r =
let (_, r') = Amc.restrict_row @'key r
Amc.extend_row @'key x r'
lens view set
end
let r
: forall 'key -> forall 'record 'type 'new 'p.
Amc.known_string 'key
* has_lens 'record 'key 'type 'new
* strong 'p
=> optic 'p 'type 'new =
fun x -> rlens @'record (Proxy : proxy 'key) x
```

Sorry for the short post, but that’s it for today.

Record fields \(\mathtt{x}\) are typeset in monospaced font to make it apparent that they are unfortunately not first-class in the language, but rather part of the syntax. Since Amulet’s type system is inherently bidirectional, the judgement \(\Gamma \vdash e \uparrow \tau\) represents type inference while \(\Gamma \vdash e \downarrow \tau\) stands for type checking.↩︎