let binders in record

[andrevidela]

• [x] I have read CONTRIBUTING.md.
• [x] I have checked that there is no existing PR/issue about my proposal.

Summary

Allow let bindings in the body of record definitions.

Motivation

Records abstract over a lot of boilerplate over using data. However, they are limited in ways that data isn't. One thing that data declarations allow but record do not is the ability to write let-binders in the type of a constructor. For example:

record Monoid where
  constructor MkMon
  carrier : Type
  neutral : carrier
  op : carrier -> carrier -> carrier

data MonoidLaw : Type where
  MkMonLaw : (mon : Monoid) -> let
    ty : Type
    ty = mon.carrier
    (+) : ty -> ty -> ty
    (+) = mon.op
    i : ty
    i = mon.neutral
    in (idR : forall a . a + i = a) ->
       (idL : forall a . i + a = a) ->
       (assoc : forall a, b, c : a + (b + c) = (a + b) + c) ->
       MonoidLaw

This is currently impossible with a record. And in itself it's not too problematic, but data does not synthesize projections functions, unlike records. This proposal fill the hole in the design space by providing the ability to write let in record defintions.

The proposal

Allow let blocs in the body of records that allow definitions to be reused multiple times in subsequent fields.

For typechecking reasons, the let blocks in records only allow clauses with type information. This is because each let binder must be lifted to the top-level where type inference is brittle and because the types of each field must be easily computable, we require each field to be given a type

Examples

record Monoid where
  constructor MkMon
  carrier : Type
  neutral : carrier
  op : carrier -> carrier -> Type

record MonLaws (mon : Monoid) where
  constructor MkMonLaws
  let (+) : mon.carrier -> mon.carrier -> Type
      (+) = mon.op
      i : mon.carrier
      i = mon.neutral
  neutralIdL : forall a . a + i = a
  neutralIdR : forall a . i + a = a
  opAssoc : forall a, b, c . a + (b + c) = (a + b) + c

The block of definitions can be written after the let:

record MonLaws (mon : Monoid) where
  constructor MkMonLaws
  let 
    (+) : mon.carrier -> mon.carrier -> Type
    (+) = mon.op
    i : mon.carrier
    i = mon.neutral
  …

let blocks can be interleaved with fields:

record MonLaws where
  constructor MkMonLaws
  mon : Monoid
  let 
    (+) : mon.carrier -> mon.carrier -> Type
    (+) = mon.op
    i : mon.carrier
    i = mon.neutral
  …

Technical implementation

Thankfully, for everyone's sanity, this can be implemented as a desugaring step. Any let block is translated to a let…in… when the record is converted to data:

record A where
  constructor MkA
  let v : B
      v = b
  f : g v

is desugared to

data A : Type where
  MkA : let v : B
            v = b
        in g v -> A

Which itself is converted to a top-level definition:

v : B
v = b

data A : Type where
  MkA : g v -> A

Interleaved let-blocks result in nested let…in…:

record A where
  constructor MkA
  f1 : B
  let d1 : D1
      d1 = …
  f2 : C
  let d2 : D2
      d2 = …
  f3 : F

Becomes

data A : Type where
  MkA : (f1 : B) -> 
        let d1 : D1 ; d1 = … in (f2 : C) -> 
        let d2 : D2 ; d2 = … in (f3 : F) -> A

Alternatives considered

Agda-style

Agda provides the same feature but the syntax is "flipped":

record A where
  constructor MkA

  op : A -> A -> Set
  op = …

  field
    a1 : A
    a2 : op a1 a1

that is, the fields need to occur in a field block and the bound definitions appear in the body of the record.

Because this is a breaking change and does not bring new functionality, there is no reason to do this. However, it allows let bound definitions to be accessed via record projections. This specific feature is out of scope for this proposal in Idris.

Conclusion

This bring feature parity between record and data while keeping the ergonomic benefits of record syntax. By ensuring it's merely a desugaring step it does not introduce additional typechecking challenges.

A prototype implementation is available here https://github.com/andrevidela/Idris2/tree/let-record-body

[gallais]

Note that Agda also gives you access to these definitions as some sort of defined projections out of the record.

open import Agda.Builtin.Nat

record ANat : Set where
  constructor mkANat
  field
    theNat : Nat
  itsSuc : Nat
  itsSuc = suc theNat
open ANat public

update : ANat → ANat
update n = record n { theNat = itsSuc n }

[andrevidela]

Is this a feature of records or is this a feature of modules? I assumed it was the latter.

edit: After some thinking I've come to the conclusion that we can probably hack it (obtain the value from the elaborated top-level definitions, pass around the context appropriately, etc), but I'd say it's out of scope for this specific feature.

[gallais]

It's a feature of the way we desugar record declarations into modules of mutual definitions so I'd say the interpretation is pretty open-ended.

I agree the current feature is useful as-is; just highlighting that the comparison with Agda can be deceiving.