# A Quickie: Manipulating Records in Amulet

Posted on September 22, 2019
Word count: 416

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 judgements1.

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 \} }$

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:

1. If the original record, the key to be inserted, and its type are all known, then the new record can be solved for;
2. 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…

1. Records can be extended:
> Amc.extend_row @"foo" true { x = 1 }
_ : { foo : bool, x : int } =
{ foo = true, x = 1 }
1. Records can be restricted:
> Amc.restrict_row @"x" { x = 1 }
_ : int * { } = (1, { x = 1 })

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

> { x = { y = 2 } } |> (r @"x" <<< r @"y") ^~ succ
_ : { x : { y : int } } =
{ x = { y = 3 } }

### 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.

1. 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.↩︎