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 }

[sellout]

Extensible records + implicit arguments is also my favorite form of ad-hoc polymorphism, so this could also be progress in that direction.

[chuwy]

Hey @sellout!

Extensible records + implicit arguments is also my favorite form of ad-hoc polymorphism

Can you show an example of this approach? I've never heard about it and super curious.

[sellout]

@chuwy Unfortunately, there isn’t much in the way of languages that support both of these features, but to give a Unison-y example with some not-yet-extant features:

1. define type classes as synonyms for extensible record types

type alias Functor f = forall rest. { map : ∀ a b. (a -> b) -> f a -> f b … rest }
type alias Applicative f = Functor f ⩓ { pure : ∀ a. a -> f a, (<*>) : f (a -> b) -> f a -> f b }
type alias Monad f = Applicative f ⩓ { (>>=) : ∀ a b. f a -> (a -> f b) -> f b }

this additionally requires a record type merge operation (⩓).

2. define instances as record values

idMonad : Monad Id
idMonad = {
  map = fn (Id a) -> Id (fn a),
  pure = a -> Id a,
  -- the rest of the instance
}

because the types are extensible, this term satisfies Functor Id, Applicative Id, and Monad Id.

3. add constraints as implicit parameters

join : {Monad m} -> m (m a) -> m a
join {m} x =
  use m (>>=)
  x >>= id

this requires implicit parameters, which Unison also doesn’t have yet. This example uses a syntax like Idris, but that likely conflicts with the extensible record syntax in Unison.

I like implicit parameters over constraints because they allow things like having multiple “instances” for a single constraint, with the ability to be explicit when there’s more than one in scope. Scala does this (although with a number of issues), and I’ve implemented a dependent version of this in Idris (but without extensible records, it leaves something to be desired).

(edited to use the type alias syntax from the issue description, which I had overlooked before)