HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.59k stars 142 forks source link

Add record update syntax #613

Open edusporto opened 2 weeks ago

edusporto commented 2 weeks ago

This PR adds syntax to update records without completely de-constructing and re-constructing them.

The added syntax is for example:

change : (Pair String String) -> (Pair String String)
| p = record p { fst: (String/append "hel" "lo") }
//    --------------------------------------------

I don't think @VictorTaelin will like the syntax like this, so I would like to hear some suggestions on how it should be.

The code in this PR already translates it into JS using object update syntax, which shouldn't be worse performance-wise than the previous method of creating a new record from scratch.

The reduction code for this term is not the best it could be. If there were an additional compilation stage to change terms after checking but before reducing, we could force every constructor to have all of its fields named and sorted (maybe inserted into a map), so the actual updating would be trivial and performant.