Why GADTs?

Unison 1.5 added GADTs, which let each constructor of a type fix that type's parameters. That may sound like a small thing, but it gives us a way to have the compiler keep track of facts we'd otherwise have to remember ourselves. I've been using them in three places in the Alygn Health service on Unison Cloud: route guards, table definitions, and migrations. Each section below is a before-and-after. The snippets are cut-down stand-ins for the real code, but they live in this project, so the working examples all typecheck (the deliberate mistakes are shown as plain snippets, along with the errors they produce).

Guards that return what they checked

Before, a guard only checked where the request came from, and handed nothing on, so a handler that needed the signed-in reader had to look the session up itself:

type before.Guard
  = gadtEvidence.before.Guard.Unguarded
  | gadtEvidence.before.Guard.SameOrigin

type before.Endpoint
  = gadtEvidence.before.Endpoint.Health
  | gadtEvidence.before.Endpoint.AccountRecords

before.guardFor : before.Endpoint -> before.Guard
before.guardFor = cases
  before.Endpoint.Health         -> before.Guard.Unguarded
  before.Endpoint.AccountRecords -> SameOrigin

before.withGuard :
  HttpRequest -> before.Guard -> '{g} HttpResponse ->{g} HttpResponse
before.withGuard request guard handler =
  match guard with
    before.Guard.Unguarded -> handler()
    SameOrigin -> if sameOrigin request then handler() else forbidden

before.serveRecords : HttpRequest -> HttpResponse
before.serveRecords request = match authenticate request with
  Some reader -> ok ("records for " Text.++ accountId reader)
  None        -> signInRequired

So, whether a request is signed in was each handler's business rather than its guard's, and nothing stopped us from giving an account endpoint the Unguarded guard in the first place.

After, the session lookup moves into the guard, and the type's index - the type parameter ev - says what a guard proves, and what an endpoint's handler needs in order to run:

type after.Guard ev where
  gadtEvidence.after.Guard.SameOriginReader : after.Guard Reader
  gadtEvidence.after.Guard.Unguarded : after.Guard ()

type after.Endpoint ev where
  gadtEvidence.after.Endpoint.AccountRecords : after.Endpoint Reader
  gadtEvidence.after.Endpoint.Health : after.Endpoint ()

after.guardFor : after.Endpoint ev -> after.Guard ev
after.guardFor = cases
  after.Endpoint.Health         -> after.Guard.Unguarded
  after.Endpoint.AccountRecords -> SameOriginReader

So, withGuard doesn't just check the request; it hands the handler the evidence it found:

after.withGuard :
  HttpRequest
  -> after.Guard ev
  -> (ev ->{g} HttpResponse)
  ->{g} HttpResponse
after.withGuard request guard handler = match guard with
  after.Guard.Unguarded -> handler()
  SameOriginReader      ->
    match (sameOrigin request, authenticate request) with
      (false, _)          -> forbidden
      (true, Some reader) -> handler reader
      (true, None)        -> signInRequired

after.dispatch : after.Endpoint ev -> ev -> HttpResponse
after.dispatch endpoint evidence = match endpoint with
  after.Endpoint.Health         -> ok "up"
  after.Endpoint.AccountRecords -> after.serveRecords evidence

after.serveRecords : Reader -> HttpResponse
after.serveRecords reader =
  use Text ++
  ok ("records for " ++ accountId reader)

In after.dispatch, matching on AccountRecords refines ev to Reader, which is why serveRecords evidence typechecks. Better still, an account endpoint left unguarded no longer does:

  after.Endpoint.AccountRecords -> after.Guard.Unguarded

I found a value  of type:  after.Guard Unit
where I expected to find:  after.Guard Reader

One constructor per table

Before, a table's name was just a string, typed out wherever it was used. Here, the accessor and the schema entry each spell out "submissions", and nothing ties the types the accessor claims to the schema's typeLinks:

type NamedTable k v = gadtEvidence.NamedTable.NamedTable Text

named : Text -> NamedTable k v
named name = NamedTable name

before.submissions : NamedTable SubmissionId Submission
before.submissions = named "submissions"

before.schema : [TableSpec]
before.schema =
  [ TableSpec
      "submissions" (typeLink SubmissionId) (typeLink Submission)
  , TableSpec "accounts" (typeLink AccountId) (typeLink Account)
  , TableSpec
      "submissions-v1"
      (typeLink SubmissionId)
      (typeLink SubmissionV1)
  ]

So, any new call site can claim whatever types it likes. This one compiles, but reading through it would ask for Text where the table stores Submission:

oops : NamedTable SubmissionId Text  -- should be Submission, not Text
oops = NamedTable.named "submissions"

After, each table is declared just once, rather than at every use. Its constructor fixes the key and value types:

type Table k v where
  gadtEvidence.after.Table.Accounts : Table AccountId Account
  gadtEvidence.after.Table.Submissions :
    Table SubmissionId Submission
  gadtEvidence.after.Table.SubmissionsV1 :
    Table SubmissionId SubmissionV1

Then spec reads a table's name and type links off that constructor (we'll get to how in a moment). Every accessor and the schema read from there, so this replaces both copies from before.

Where before.submissions typed out the name and stated its types by hand, the accessor now just opens the constructor, which supplies both:

open : Table k v -> NamedTable k v
open table = named (TableSpec.name (spec table))

after.submissions : NamedTable SubmissionId Submission
after.submissions = open Submissions

And where before.schema was a hand-written list, the schema is now read off the same specs. SomeTable hides the indices, so every table fits in one list:

type SomeTable where
  gadtEvidence.after.SomeTable.SomeTable : Table k v -> SomeTable

all : [SomeTable]
all =
  [ SomeTable Submissions
  , SomeTable Accounts
  , SomeTable SubmissionsV1
  ]

after.schema : [TableSpec]
after.schema = List.map (cases SomeTable table -> spec table) all

Now the same mistake doesn't make it past the typechecker:

oops : NamedTable SubmissionId Text
oops = after.Table.open after.Table.Submissions

I found a value  of type:  NamedTable SubmissionId Submission
where I expected to find:  NamedTable SubmissionId Text

type Stored a where
  gadtEvidence.after.Stored.AccountIdS : Stored AccountId
  gadtEvidence.after.Stored.AccountS : Stored Account
  gadtEvidence.after.Stored.SubmissionIdS : Stored SubmissionId
  gadtEvidence.after.Stored.SubmissionS : Stored Submission
  gadtEvidence.after.Stored.SubmissionV1S : Stored SubmissionV1

link : Stored a -> Type
link = cases
  SubmissionIdS -> typeLink SubmissionId
  SubmissionS   -> typeLink Submission
  SubmissionV1S -> typeLink SubmissionV1
  AccountIdS    -> typeLink AccountId
  AccountS      -> typeLink Account

type Parts k v
  = gadtEvidence.after.Parts.Parts Text (Stored k) (Stored v)

parts : Table k v -> Parts k v
parts = cases
  Submissions   -> Parts "submissions" SubmissionIdS SubmissionS
  Accounts      -> Parts "accounts" AccountIdS AccountS
  SubmissionsV1 -> Parts "submissions-v1" SubmissionIdS SubmissionV1S

spec : Table k v -> TableSpec
spec table =
  (Parts name key value) = parts table
  TableSpec name (link key) (link value)

after.Table.Accounts -> Parts "accounts" AccountIdS SubmissionS

I found a value  of type:  Parts AccountId Submission
where I expected to find:  Parts AccountId Account

When you Migrate, I hope you are (up)Lifted

Before, a shape migration opened both tables by name and stated their types by hand:

before.migrationTwelve : '{Rows} ()
before.migrationTwelve =
  do
    old : [(SubmissionId, SubmissionV1)]
    old = readAll (named "submissions-v1")
    writeAll
      (named "submissions")
      (List.map (cases (key, row) -> (key, addDeficit row)) old)

It's short, but it has the problem from the previous section twice over: two names and a type annotation, none of which are checked against the schema. Swap the two names and it still compiles, then tries to read rows of the new shape as SubmissionV1 when it runs:

old = readAll (NamedTable.named "submissions")
writeAll (NamedTable.named "submissions-v1") (List.map (cases (key, row) -> (key, addDeficit row)) old)

After, the read, convert and write loop is written once, and a migration becomes a value naming two tables and a conversion:

type RowLift where
  gadtEvidence.after.RowLift.RowLift :
    Table k old -> Table k new -> (old -> new) -> RowLift

liftRows : RowLift ->{Rows} ()
liftRows = cases
  RowLift source target convert ->
    rows = readAll (open source)
    writeAll
      (open target)
      (List.map (cases (key, row) -> (key, convert row)) rows)

after.migrationTwelve : RowLift
after.migrationTwelve = RowLift SubmissionsV1 Submissions addDeficit

Admittedly, this is more code for one migration, so why bother? There are two reasons.

First, each row lift after this one is a single declaration, once its conversion is defined. RowLift hides the old and new value types, as SomeTable does, so lifts of different record types fit in one list. In our service, one migration moves four tables as a list of four lifts, and the shared code also reads every converted row back afterwards — a check each earlier shape migration had written out by hand.

Second, the mistakes above no longer compile. The tables' indices fix the direction, so the same swap is caught:

RowLift after.Table.Submissions after.Table.SubmissionsV1 addDeficit

The 3rd argument to `RowLift`
          has type:  SubmissionV1 -> Submission
    but I expected:  Submission -> SubmissionV1

They also fix the key type, so a lift between tables with different keys is caught too:

RowLift after.Table.Accounts after.Table.Submissions (account -> Submission (Account.email account) None)

The 2nd argument to `RowLift`
          has type:  Table SubmissionId Submission
    but I expected:  Table AccountId new

Closing thoughts

Our service has 73 endpoints and 98 tables, so this wasn't just a toy example. The derived schema came out equal to the hand-written list it replaced, so the change needed no data migration; here, theSameSchemaEitherWay checks the same thing.

If you'd like to use any of this without writing it yourself, the table and migration pieces are in @nusentry/blueprint as of 8.5.0: blueprint.lift for row lifts, and TypedSpec for table specs checked through a witness.