Nested struct updates

[leonardo]

Some supposed improvements of Idris language over Haskell:

10 things Idris improved 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.

[Centril]

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.

@leonardo

// A Idris-inspired syntax:
let c2 = Customer { account.accound_id: 2, ..c1 };

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

@leonardo

Something similar in Rust (currently not allowed):

let c2 = Customer { account.accound_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.

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)