More ergonomic records

[fmease]

Meta: Task: Expand

Current design #18, #42 (here with #102 implemented):

@public
data Thing (A: Type): Type of
    thing 'A
        (::foo: A)
        (::bar: Text): Thing A

t: Thing = Thing.thing (foo = 3) (bar = "bar")
t1: Thing = Thing.thing (foo = t::foo) (bar = t::bar ++ "!")

Proposal 0 (Nov 24, 2021)

@public
record Thing (A: Type): Type of
    foo: A
    bar: Text

-- unsure about the following syntax
t0: Thing = Thing{ (foo 3) (bar "bar") }
t1: Thing = Thing{ (bar t0::bar ++ "!") t0 }

Proposal 1 (Dec 21, 2021)

@public
data Thing (A: Type): Type record thing of
    foo: A
    bar: Text

t0: Thing = thing (foo = 3) (bar = "bar")
t1: Thing = thing 3 "bar"
t2: Thing = thing (bar = t0::bar ++ "!") (= t0::foo) ;;; no update syntax aorn

Variation 1

PRO (compared to proposal 1 baseline): We define a new binding thing and thus it should be a bit more prominent/visible. In baseline, it gets lost in the noisy line.

@public
data Thing (A: Type): Type of
    record thing of
        foo: A
        bar: Text

Variation 2

@public
data record Thing (A: Type): Type of
    thing of
        foo: A
        bar: Text

Unanswered Questions

• Should record be preceded by of
• Should the record constructor be namespaced?
• How do record updates look like?

Note: Order of fields is part of the API anyway because fields may be dependent.

[fmease]

We finally have a found a good design, see #174.