Extensible records

[pchiusano]

We brainstormed this a while back, but just capturing it here as an issue.

-- an anonymous record type, similar to (Nat, Float) but w/ named fields
{ x : Nat, y : Float }
x = { x = 1, y = 39.0 }

-- don't need to declare fields in advance, just use them

-- orthogonal, but we'd like type aliases
type alias Pt = { x : Float, y : Float }

-- could also do - this alias allows extra fields besides 'x' and 'y'
type alias Pt rest = { x : Float, y : Float | rest }

-- record type with name, email, and possibly more fields
{ name : Text, email : Text | rest }
-- alternate "... rest" means "and some other fields 'rest'"
{ name : Text, email : Text ... rest }

-- field access, straw man syntax
(@name) : { name : x | rest } -> x

> List.map @name [{name = "hi", phone = "294-192-3934"}]
= ["hi"]

-- fields can be multiple segments, for nested get/set/modify
-- fields can't be symbolic (can't have a field called +++)
(@user/email) : { user : { email : x | r1 } | r2 } -> x
-- potentially @user.email
-- potentially .user.email (if we get rid of absolute names in term syntax)
-- or switch absolute names to __root__.foo.bar.baz

> List.map @user/email [{user = {email = "paul.chiusano@gmail.com"}}]
= ["paul.chiusano@gmail.com"]

-- nice syntax sugar for record destructuring
foo = cases
  {name = "Paul", email, age} | age > 3 -> name ++ "  " email

blah = cases
  {name = "Paul", email, age | rest} -> rest -- stuff doesn't have 'name' and 'email'

> blah { name = "Paul", age = 40, email = "paul@foo.com", favColor = "blue" }
= { favColor = "blue" }

-- field set
x = {user = {email = "paul@foo.com"}, favoriteColor = "blue"} 

x' = x { user/email = "su@bar.com" }

> x'
= { user = {email = "su@bar.com"}, favoriteColor = "blue" }

-- syntax sugar for setting multiple fields
x { name = "Bob", user/email = "paul@bar.com" }

-- alternate, inspired by JS "spread" syntax
{ ...x, name = "Bob" }
-- alternate, following the type syntax
{ name = "Bob" | x }
-- alternate, using '...' to mean "and the rest is x" (type syntax could be same)
{ name = "Bob" ... x }

-- syntax sugar for declaring / consing a field, use := instead of =
x { favoriteMovie := "2001: A Space Oddessy" }

-- syntax for modify ???

-- field set / modify / (user shouldn't have to look at these types typically)
(set @user/email) : { user : { email : x | r1  } | r2 } 
                 -> x2 
                 -> { user : { email : x2 | r1 } | r2 }

-- field modify (user shouldn't have to look at this typically
(modify @user/email) : { user : { email : x | r1  } | r2 } 
                 -> (x -> x2) 
                 -> { user : { email : x2 | r1 } | r2 }

(cons @name)   : { rest } -> a -> { name : a | rest }
(uncons @name) : { name : x | rest } -> { rest }

@dolio has idea for paper that would let us implement this, the Dan Liejnn scoped record labels paper. It does have the somewhat odd behavior that that cons shadows the existing copy of the field, but has nice and simple types for cons / uncons (don't need 'has field' and 'lacks field constraints'). Implementation would "just" need to add some constructors to term and type ASTs and some changes to the typechecker (and we could just delete the existing magic syntax hack implementation of records).

[kristiannotari]

Not sure if this is the right place to comment about this proposal, so feel free to delete this. I'd like to point out that to me, coming from js/ts world and from unison type signatures, reading { a: x | rest } means "a record with one property a which could either be x or rest" due to the | symbol meaning or typically. I don't see why there should be many ways to accomplish the same "...and the rest" thing, cause to me they seems like complicating reading code (or reading scratch files if the format is then standardized to a default when pretty printing). If fields are comma separated, I'd keep the ...x syntax as one of the comma separated list of properties, as in { a, b, ...rest } as the only and default way. But maybe you already tried and it doesn't work well for some cases?

[chuwy]

That must be out of scope of plain extensible records, but I also really like how you can reflect on record types in TypeScript:

type Person = { name: String, age: number | undefined }
type Meta = { id: number, createdAt: Date }

type PersonWithMeta = Meta & Person   // combined
type WithoutNulls = Partial<Person>  // name also could be undefined now
type IdWithName = Pick<"id" | "name", PersonWithMeta>  // { id: number, name: string }