3
$\begingroup$

Suppose I have a concat function with a signature using extension types:

def concat
 (p : [i] A {}) -- faceless
 (q : [i] A {i=0 ↦ p 1}) -- one face
 : [i] A {i=0 ↦ p 0, i=1 ↦ q 1}

I am using Cubical Agda's approach to represent interval-elimination, say, p i where p : [i] A {rua} is implemented as IApp(Ref(p), Arg(Ref(i)), rua) where rua contains the faces in the type of p. This gives the reduction sufficient (I believe) type information so in the type checker I can have normalize : Term -> Term instead of normalize : Term -> Type -> Term.

So here, p 0 is represented as IApp(Ref(p), Arg(Ref(i)), no-face) because that's what the type signature says. So there is no special type-directed reduction for it.

However, when I supply {an argument x that actually has some faces} to it (so like, x : [i] A {i=0 ↦ y}), type-checking x : [i] A {} loses the faces I needed, and leads to some type errors (the LHS of the result path is a stuck term x 0 because p has no face (even though x does have)).

I wonder if:

  1. My representation of interval application is incorrect, or
  2. This is a known issue with extension types itself, or
  3. Am I doing substitution wrongly, or
  4. Is there something else that I should be aware of?
$\endgroup$

1 Answer 1

3
$\begingroup$

Your core representation of extension type application is the right one. The issue in the example is in the conversion from an extension with faces to the faceless. In the surface language, it can be implicit (as some form of subtyping), but in the core language it should be explicit.

Given p : [i] A {faces}, we forget its faces by eta-expansion (using lambda for extension abstraction): (λ i. p i) : [i] A {}. Here the p i application is represented according to your scheme, as IApp(p, i, faces).

When concat is applied to (λ i. p i), the return type is instantiated to [i] A {i=0 ↦ (λ i. p i) 0, i=1 ↦ q 1}, and (λ i. p i) 0 reduces to p 0, but this application is annotated with the original faces of p. So everything is well-typed and we don't lose track of the faces.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.