Dependent Records (first pass)

[brendanzab]

This is a cut down set of requirements for dependent records, in contrast to the more lofty goals described in issue #2.

The following additions will be made to the core syntax:

R ::= l : T, R  -- field type annotation
    | ε         -- empty record type

r ::= l = t, r  -- field value definition
    | ε         -- empty record value

t,T ::= ...
      | Record { R }   -- record types
      | record { r }   -- record values
      | t.l            -- projection

• The same label cannot be used multiple times in the same record.
• For now we will be picky on field order, ie. Record { x : I8, y: I8 } will not be compatible with Record { y: I8, x : I8 }, and record { x = 1, y = 2 } : Record { x : I8, y: I8 } is a type error.
• Field type annotations introduce new values into the type checking context, and may be used in the type annotations of later fields.
• Field value definitions introduce new values into the evaluation context, to be when constructing later fields.
• Care must be taken to preserve these substitutions when projecting fields.

[markbrown]

Following are some rules for the above. For the moment I'll assume there is a Conv rule somewhere, so I'll leave out any normalisation that might be needed later. Also, I'll use x, y, etc as label metavariables, as l looks like 1 with my eyesight these days :-(

Field type annotations introduce new values into the type checking context, and may be used in the type annotations of later fields.

A rule for this (fairly standard, I think) is

Γ  ⊢  T : *
Γ,x:T  ⊢  R : *
-------------------
Γ  ⊢  (x: T, R) : *

Field value definitions introduce new values into the evaluation context, to be when constructing later fields.

I'm not sure how typical this one is. Is the value usually available for later field values? In any case:

Γ  ⊢  t : T
Γ,x:T  ⊢  r : R[t/x]
----------------------------
Γ  ⊢  (x = t, r) : (x: T, R)

Care must be taken to preserve these substitutions when projecting fields.

Right. This can be written out as follows:

Γ  ⊢  t : T
T' = field(T, x)
θ = fsubst(t, T, x)
------------------
Γ  ⊢  t.x : T'θ

where the functions are defined as:

field((x: T, R), x) = T
field((y: T, R), x) = field(R, x), if x != y

fsubst(t, (x: T, R), x) = []
fsubst(t, (y: T, R), x) = fsubst(t, R, x) ++ [t.y/y], if x != y

As an example, say you're in a context where:

t : Record { n: u16, x: Array n i8, y: Array n i8 }
inner_prod : {{ size: Nat }} -> (a1: Array size i8) -> (a2: Array size i8) -> i32

I'm using double braces here to indicate that the size argument needs to be elaborated. Given this, the following term should typecheck:

inner_prod t.x t.y : i32

The two arguments have type Array t.n i8, and therefore size would be bound to t.n.

[brendanzab]

Awesome!

Field value definitions introduce new values into the evaluation context, to be when constructing later fields.

I'm not sure how typical this one is.

Yeah, me neither - but I think it is nice from an ergonomics perspective. It think it's allowed in Agda at least.

Γ  ⊢  t : T
T' = field(T, x)
θ = fsubst(t, T, x)
------------------
Γ  ⊢  t.x : u'θ

Where does u' come from? Was it meant to be T'?

Gonna see if I can try to avoid substitution, as per this blog post - I've pretty much got it eliminated from the rules right now. Would be interesting to see if we could transform these rules to avoid it too. 🤔

I'm using double braces here to indicate that the size argument needs to be elaborated.

My plan at the moment is to use {x:T} -> t for implicit arguments (like forall x. a in Haskell, see #8) and {{x:T}} -> T for instance arguments (like (constraint) => a in haskell, see #13)

[markbrown]

Where does u' come from? Was it meant to be T'?

Yes, sorry. I've edited my original post to fix that.

Gonna see if I can try to avoid substitution, as per this blog post

That's a good idea when formulating the operational semantics, which I think is what that article is written in relation to. Personally I like to start off with rules in the declarative style, since it's easier to check that they mean what you think they mean, and from there proceed to an operational semantics (i.e., syntax-directed rules) using the declarative rules as a guide. But I realise some people like to head straight for an operational semantics in one go.

So, yes, it remains to be figured out how to make the rules bidirectional, where to normalise, how to implement substitution, etc.

[markbrown]

I'm not sure how typical this one is.

Yeah, me neither - but I think it is nice from an ergonomics perspective. It think it's allowed in Agda at least.

For comparison, the version of the rule that doesn't allow this is:

Γ  ⊢  t : T
Γ  ⊢  r : R[t/x]
----------------------------
Γ  ⊢  (x = t, r) : (x: T, R)

That is, we don't add x to the context in the second premise.