# Record MVP

###### tags: `Juvix` `juvix-project` `records`

$$
\newcommand\Let{\mathbf{let}\:}
\newcommand\In{\:\mathbf{in}\:}
\newcommand\Return{\:\mathbf{return}\:}
\newcommand\RV[1]{\langle #1 \rangle}
\newcommand\Lett{\mathbf{let}\text-\RV{}}
$$

## Names

Implementing the [current design] of records still has some unanswered questions about the bound names $\bar y$ in $\Let \RV{\bar y} = e \dotsb$:

[current design]: https://hackmd.io/Xlvu82eFQ_m-cebUWAtGsw?view

- they are bound variables, so they must be added to the local context in dependency order
- in the current spec, they can be given in any order
- the name resolution step happens before type checking, so the information to reorder them is not yet available.

It might be possible to get around this by using `PatternVar` instead, but I understand that is on the way out at some point so adding more uses of it is probably not the right way to go.

With all this in mind, I think in the initial implementation we simply require (when checking the $\Lett$ expression) that the names $\bar y$ be in the same order as in the type of $e$. Allowing them to be permuted can be added in future.

With the names in the `let` corresponding exactly to those in the type of `e`, the constructor can be

RecElim [Symbol]              -- names bound
        (Elim primTy primVal) -- record to deconstruct
        (Term primTy primVal) -- return type
        (Term primTy primVal) -- body

and the representation in core of $\Let \RV{\bar y} = e \Return x.A \In s$ can be `RecElim 𝑦̄ 𝑒 𝐴 𝑠`. One variable ($x$, corresponding to the record) is bound in `𝐴`, and one in `𝑠` for each field, with the rightmost field being index `0`.

## Field lookups

Since the $\Lett$ form is (I think) also going to be added to the frontend language, it could be possible to have that be the *only* way to eliminate a record in the MVP implementation, leaving lookup expressions and the passes required to later iterations.

## Do records have $η$?

Not yet, no, because the evaluator isn't type aware. When it is, then since these records are non-recursive, I don't see why they shouldn't.

## Renaming?

Sure. Not in the MVP, probably, but soon after.

Something like
`let {val = x} = e return ... in x`
desugaring to
`let {val} = e return ... in (let x = val in x)`.

## Does this design actually work?

I never gave an example before, so here's a couple

sig pair : (a : ty) -> (b : a -> ty) -> ty
let pair a b = {1 fst : a; 1 snd : b fst}

-- ω because the snd field is being dropped
sig fst : pair a b -(ω)-> a
let fst #a p = let {fst; snd} = p return _ => a in fst

sig snd : (p : pair a b) -(ω)-> b (fst p)
let fst #b p =
  let    {fst; snd} = p
  return x => (let {fst; snd} = x return ty in b fst)
  in     snd


sig two : ty -> ty
let two a = {2 val : a}

sig app : (a -> a -> b) -> two a -> b
let app #b f p =
  let {val} = p return _ => b in f val val

The body of `snd` looks a bit weird with the nested let, but that's because this is currently the unsugared core form. It would be possible to automatically have the fields be in scope in the `return` clause by adding a desugar step that inserts this extra `let`.

## Is the $x$ in $\Return x. A$ really needed?

I think so? But if not I'll be more than happy to remove it.