Allow dependencies between record term elements

[brendanzab]

This allows the elements of record terms to depend on each other. For example, this expression is now valid:

record { x = 1, y = x }
    : Record { x : S32, y : S32 }

This has the helpful side-effect of fixing the scoping glued levels in record terms. Before this change we would trigger a runtime panic on rendering the error message for the following term:

record {
    Elem = String,
    elem = record {},
} : Record {
    Elem : Type,
    elem : Elem,
}

This is because Elem is not bound in the record term!

Now we render the following error:

error: mismatched types
  ┌─ examples/escaping-local.pi:3:12
  │
3 │     elem = record {},
  │            ^^^^^^^^^ expected `String`, found `Record {}`

This also paves the way for allowing us to elaborate let-expressions into record terms in the core language, as is done in 1ML. For example:

let {
    x : S32 = 1,
    y : S32 = x * 2,
} in y - x

Could be sugar for:

(record { x = 1, y = x * 2, body = y - x }
    : Record { x : S32, y : S32, body : S32 })
        .body

This change also brings the typing rules of record terms closer to that of function terms with labelled parameters, which I think is aesthetically appealing, and could eventually help us bring functions and records much closer together in terms of typing rules and syntax.

It does however mean that we no longer allow for out-of order elements in record terms. For example the following is no longer valid:

record { y = 1, x = 2 }
    : Record { x : S32, y : S32 }

I'd like to eventually lift this restriction however, but it might require us to do some topological sorting of field elements in the
elaborator.

Closes #229.

[brendanzab]

This uncovered a variable binding bug that was added in 1afb476 - serves me right for not having a more comprehensive test suite! 🤦‍♂️

It means that dependent functions are completely broken:

> (fun A a => a : Fun (A : Type) -> A -> A)
fun A a => a : Fun (A : Type) -> Fun (t : A) -> A
> (fun A a => a : Fun (A : Type) -> A -> A) S32
thread 'main' panicked at 'called `Option::unwrap()` on a `None` value', pikelet/src/lang/core/semantics.rs:481:52

I'll have to track this down in a later PR, but for now I've commented this stuff out.

[brendanzab]

I've posted more details here: #229 (comment)

[AndrasKovacs]

This also paves the way for allowing us to elaborate let-expressions into record terms in the core language

This is not possible in the presence of dependent types. For example,

let {
    A : Type = Bool
    f : A -> A = not
} in f True

Has no immediately corresponding record type. This is the same reason why let is not derivable from function application in dependent settings. Using identity types we can do an emulation:

record {A = Bool, def-A = refl, f = not, def-f = refl} : 
Record {A : Type, def-A : A = Bool, f : A -> A, def-f : f = transport (\A -> A -> A) (sym def-A) not}

But this requires a very difficult translation from strict equalities to propositional ones. See https://hal.archives-ouvertes.fr/hal-01849166/file/cpp19.pdf

"Translucent types" were a proposed solution addressing dependent definitions in signatures: https://people.mpi-sws.org/~dreyer/courses/modules/harper94.pdf. But this seems ill-justified and ad-hoc in dependent settings.

[brendanzab]

Ah dang, that's disappointing! Yeah I had remembered that it was an issue for doing it with the function application style, but for some reason had thought I might be able to get away with it for records - I think because the definitions of the fields are in scope, unlike in lambdas where they are abstract? Thanks for the correction and pointers to the relevant information!

Should I be concerned if something like the following snippet this type checks and runs ok in my language?

(record {
    A = Bool,
    f = fun a => a : Bool -> Bool,
    body = f true,
} : Record {
    A : Type,
    f : A -> A,
    body : Bool,
}).body

[AndrasKovacs]

So should I be concerned if something like this type checks and runs fine in my language?

No, that's fine with the extended scoping rule for records.

definitions of the fields are in scope, unlike in lambdas where they are abstract

Only in the record constructor expression, not in the record type. In the record type the fields must be abstract.

[brendanzab]

Ah yeah, in the original statement I was referring to elaborating to 'record terms' - ie. 'record constructor expressions' - not record types. 😅 Taking into account the extended scoping rules would elaborating let expressions into record constructors + projection be possible? Ie.

let {
    A : Type = Bool
    f : A -> A = not
} in f True

would be elaborated to:

(record {
    A = Bool,
    f = not,
    body = f true,
} : Record {
    A : Type,
    f : A -> A,
    body : Bool,
}).body

[AndrasKovacs]

Not possible. Consider any example where a type of a definition is only well-typed up to a previous definition:

let {
  A : Type = Bool
  a : A = true
  p : Id A a true = refl
} in p

Id A a true is only valid if A = Bool by definition, which is not available in the record type.

[brendanzab]

So the Id A a true needs the definition of a in the type, but it's not - it's been split off into the record constructor expression:

(record {
    A = Bool,
    a = true,
    p = refl,
    body = p,
} : Record {
    A : Type,
    a : A,
    p : Id A a true,
    body : Id A a true,
}).body

I guess I'm still a bit confused because even so, by the time you are checking the field p = refl with the goal Id A a true, don't you have the following in the context:

• A : Type = Bool
• a : A = true

The same would go for the field body = f with the goal Id A a true, where you have the following in the context:

• A : Type = Bool
• a : A = true
• p : Id A a true = refl

Or should I not be adding the definitions to the context when checking record constructor expressions like this? Sorry for my slowness - still getting to grips with dependent types! I might also need to finally get around to implementing identity types - maybe the issue would be more apparent to me then? 😅

[brendanzab]

Or maybe I need some example where refl : Id A a true is used in some part of a type annotation. So that in order for the annotation to be a valid type, you'd need to know the definition of a?

[brendanzab]

So yeah, I think I'm understanding the issue now - it's just I found the previous examples didn't capture this.

The problem is that some annotations in let bindings need to access the contents of a definition in order to be able to be considered valid types. Splitting the definitions from the delarations as is done when desugaring let expressions to records means that the declarations can no longer access previous definitions. This reduces what you can express with let bindings, unless you can figure out some way to expose the definitions of fields in the record types, which is what the linked resources you mentioned in your original comment address.

[AndrasKovacs]

Correct. The relevant part in the Id A a true example is A, not a. This type itself is not well-typed unless A = Bool, because true : Bool.

[Blaisorblade]

"Translucent types" were a proposed solution addressing dependent definitions in signatures: https://people.mpi-sws.org/~dreyer/courses/modules/harper94.pdf. But this seems ill-justified and ad-hoc in dependent settings.

(Got here from a question on ##dependent) When you say “ad-hoc”, would you consider singleton types/kinds (as in PFPL) to solve the ad-hoc part? I guess the problem becomes the complexity of their metatheory and typechecking algorithms...

[AndrasKovacs]

The singletons in PFPL are very much among the ad-hoc solutions. It builds on a) equality reflection b) subtyping. The former is undecidable in TT, the latter is hugely painful in type inference. In contrast, the native let-definitions that it tries to replace are trivial both in metatheory and in implementation. All categorical semantics rely on explicit substitutions, and the let rule is just a minimal way to add explicit substitutions back to the surface syntax.

The standard & decidable way to talk about partial information is propositional equality, and the standard & decidable way to assume definitional equality is the let-rule. An iterated mixing of sigmas, lets and projections with identity types is the best solution for translucency that I know about. Of course, we may add syntactic sugar on top of this in an implementation.

The extended scoping rule for record constructors, discussed here, can be also viewed as sugar which (conceptually) computes to a mixing of let-s and sigma pairing constructors.

[brendanzab]

So yeah, I've looked into this a bit - it seems like you might be able to add manifest fields to an intensional type theory without adding singletons to the core language? I could be wrong though! See “Manifest Fields and Module Mechanisms in Intensional Type Theory” by Zhaohui Luo. There was also some manifest fields implemented as an Agda library, which is based on “Dependently Typed Records in Type Theory” by Robert Pollack. I'm guessing this doesn't solve the issue of subtyping though? Like you might need to compile it to a core language with some coercions in to selectively 'forget' the definitions of the manifest fields?