A Quickie: Manipulating Records in Amulet

Posted on September 22, 2019

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:


And eliminated by projecting a single field:


Records also support monomorphic update:

Γr{αx:τ}ΓeτΓ{r with x=e}{αx:τ}

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.

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

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

     Amc.row_cons 'r 'k 't 'n
  => has_lens 'r 'k 't 'n
  | 'k 'n -> 'r 't
  val rlens : strong 'p => proxy 'k -> optic 'p 't 'n

    Amc.known_string 'key
  * Amc.row_cons 'record 'key 'type 'new
  => has_lens 'record 'key 'type 'new
  let rlens _ =
    let view r =
      let (x, _) = Amc.restrict_row @'key r
    let set x r =
      let (_, r') = Amc.restrict_row @'key r
      Amc.extend_row @'key x r'
    lens view set

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 x\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 Γeτ\Gamma \vdash e \uparrow \tau represents type inference while Γeτ\Gamma \vdash e \downarrow \tau stands for type checking.↩︎