Nested struct updates


#1

Some supposed improvements of Idris language over Haskell:

Given two records:

record Account where
  constructor MkAccount
  accound_id : String
  address : String

record Customer where
  constructor MkCustomer
  name : String
  address : String
  account : Account

Idris gives you a simple built-in syntax to update nested records:

update_billing_address : Customer -> String -> Customer
update_billing_address customer address =
  record { account->address = address } customer

Similar Rust code:

struct Account {
    accound_id: u64, // No string
    address: String,
}

struct Customer {
    name: String,
    address: String,
    account: Account,
}

fn main() {
    let a1 = Account { accound_id: 1, address: "xx".into() };
    let c1 = Customer { name: "nnn".into(), address: "yy".into(), account: a1 };

    // You can't do this in Rust here:
    let c2 = Customer { account: Account { accound_id: 2, ..a1 }, ..c1 };
    
    // A Idris-inspired syntax:
    let c2 = Customer { account.accound_id: 2, ..c1 };
}

Idris also allows to apply a function over a field in a nested record, like this (with the $= operator):

concat_billing_address : Customer -> String -> Customer
concat_billing_address customer complement =
  record { account->address $= (++ complement) } customer

Something similar in Rust (currently not allowed):

let c2 = Customer { account.account_id: account.accound_id + 2, ..c1 };

The syntax shown here could be useful if you want to use Rust with immutable data, in a more functional style.


#2

I’ve also thought about this; Idris’s changes seem to be quite nice and bring into the language features that the lens package offers.

Seems natural; Can’t see any faults with this other than potentially encouraging overuse of public fields. But using this internally seems fine.

The beauty of the Idris syntax here is that it is point-free whereas

account.accound_id: account.accound_id + 2

is not point free.

I wonder if it would be possible to apply a lambda or a function somehow. Strawman syntax:

let c2 = Customer { account.account_id(|id| id + 1), ..c1 };

or just applying a function directly:

let c2 = Customer { account.account_id(plus_one), ..c1 };

perhaps even (for this particular case):

let c2 = Customer { account.account_id += 1, ..c1 };

(we would extend this to all assignment operators)