Add support for accessing/projecting record type fields

[Gabriella439]

Fixes #1079

[winitzki]

This rule is for record literals. We also need a corresponding rule for record types here.

[winitzki]

t ⇥ { x : T, … }
────────────────
t.x ⇥ T

[winitzki]

We probably need a rule where t is a record type and then t.{} ⇥ {}?

[winitzki]

It seems we need rules like this:

Γ ⊢ t : { ts… }
─────────── ; t is a record literal
t.{} ⇥ {=}


Γ ⊢ t : Type
───────── ; t is a record type
t.{} ⇥ {}

So, we need to type-check t before beta-normalizing t.{}. Until this change, beta-normalization never needed a type-checking phase but now it seems we have to introduce a dependency on type-checking. Also, it is not clear where Γ would come from. How did you implement this in Haskell?

A test for this is to beta-normalize λ(x : { a : Bool }) → x.{}, which should give λ(x : { a : Bool }) → {=}. The beta-normalizer only looks at x.{} and does not use the information about the declared type of x. So, the beta-normalizer somehow needs to decide what to do with x.{} without knowing the type of x. Until now, only a record value x was allowed. If we now allow also record types as x, then we need to decide whether x.{} reduces to {=} or to {}.

[winitzki]

One workaround is simply to disallow t.{} in the type checker unless t is a either a record value or a literal record type. Then we can first beta-normalize t.{...} for literal record types t, and if that does not match, then beta-normalize t.{} ⇥ {=} for all t without any checking.

This will disallow beta-normalizing t.{} if t is a variable carrying a record type but allow beta-normalizing t.{} if t is a variable carrying a record value, which is a bit ugly because it's asymmetric.

At the same time perhaps it is the right solution because we should not be beta-normalizing λ(t : Type) → t.{} to λ(t : Type) → {} really.

Another solution is a breaking change: delete the distinction between record types and record values; there will be just "records". Allow using the syntax { a = x, b = y} and {a: x, b: y} interchangeably. Then {a: Natural, b: Bool} and {a = Natural, b = Bool} will become the same term, and so will { a: 1, b: True} and { a = 1, b = True}. Records containing types will be used as types for records containing values:

{ a: 1, b: True} : {a: Natural, b: Bool} or equivalently { a: 1, b: True} : {a = Natural, b = Bool}

This gets records closer to the Json syntax.

Typing will become trickier though. Currently, the type of {a = Bool} is {a: Type} while the type of {a : Bool} is Type.

Also, the syntax {=} will become equivalent to {}, which is perhaps a bad idea because we would like to distinguish them.

So, it seems that it's not really workable to conflate record values and record types.

[MonoidMusician]

Making record types and record values the same thing isn't feasible, because { a : Type, b : Type } /= Type, so you would just have record “types” all the way down and never get to a universe. (I've thought a lot about this before.)

[winitzki]

Yes, that makes sense.

I have updated the description of the workaround I'm proposing.