12
$\begingroup$

Self Types are known for being a simple extension to the Calculus of Constructions that allow it to derive all inductive datatypes of a proof assistant like Coq and Agda, without a "hardcoded" native datatype system. I am now trying to answer if we can also derive the features of Cubical Type Theory. It seems like most essential features, including higher inductive types, Path, Interval and so on can, indeed, be derived from Self alone. But some corners are still missing. I'm posting this as a question to sum up my progress and ask for a helping hand.

Explaining Self Types (for context)

For those still unfamiliar, let me explain what Self types are. It is simple: remember that, in a dependently-typed language, f(x) : B(x)? That is, the type returned by an application has access to the applied argument? In a self-dependently-typed language, f(x) : B(f,x), i.e., the returned type can also access the applied function. That's all. This allows us to derive inductive datatypes naturally. For example, Nat can be defined as:

Nat : Type
  ∀self(P : Nat -> Type) ->
  ∀(zero : P(λz. λs. z)) ->
  ∀(succ : ∀(n : Nat) -> P (λz. λs. s n)) ->
  P self

With its induction principle being:

nat-ind : (n : Nat) -> P(0) -> ((n : Nat) -> P n -> P (succ n)) -> P n
nat-ind = λn. λz. λs. n P z (λx. s (nat-ind x z s))

Notice the self variable on the first of Nat. When we call n P, it is substituted by n itself, allowing nat-ind to return P(n). This was the only thing preventing λ-encoded datatypes to replace native datatypes on raw type theory.

Encoding Path and Interval

The cool thing about encoding data with Self is that it isn't restricted by the limitations of a native datatype implementation. That allows us to do things that weren't expected by the "language designer". For example, we're able to implement "constructors with conditions that compute". We can encode Int as a pair of two Nats such that int (succ a) (succ b) reduces to int a b. Similarly, nothing prevents us from creating constructors that return "other datatype". Higher Inductive Types can then be encoded with constructors that return the equality type.

With that in mind, my plan to derive HoTT with Self is to encode the Interval type as a "boolean", except with a third constructor that enforces the first two to be equal. For that, we need a notion of equality, so I use the cubical Path, which is, too, encoded an inductive datatype, but one with only one constructor: the path abstraction. In Agda pseudocode, it would be written as:

data I : Set where
  i0 : I
  i1 : I
  ie : Path _ i0 i1

data Path (A : I -> Set) : A i0 -> A i1 -> Set where
  abs : (t : (i : I) -> A i) -> Path A (t i0) (t i1)

Note that Path and I are mutually recursive: Path uses I for its endpoints, and I uses Path to ensure it can only be pattern-matched accompanied by a proof that both branches are equal. This is different from the usual interval type (which can't be pattern-matched at all), but thanks to Path, the effect is the same. The full representation with Self is:

I : Set
  ∀self(P: (i : I) -> Set) ->
  ∀(I0 : P i0) ->
  ∀(I1 : P i1) ->
  ∀(IE : Path P I0 I1) ->
  P(self)

i0 : I
  λP. λi0. λi1. λie. i0

i1 : I
  λP. λi0. λi1. λie. i1

ie : Path (λi. I) i0 i1
  λP. λabs. abs (λi. i)
  
Path (A : I -> Set) (a : A i0) (b : A i1) : Set
  ∀self(P : (a : A i0) -> (b : A i1) -> Path A a b -> Set) ->
  ∀(Abs: (t : (i : I) -> A i) -> P (t i0) (t i1) (abs A t)) ->
  P a b self

abs (A: I -> Type) (t : (i : I) -> A i): Path A (t i0) (t i1)
  λP. λabs. abs t

This encoding allows us to derive other Path primitives as functions.

Path application

Path application allows us to apply a Path A a b to an i : I and get either a or b. Since Path's only constructor is the path abstraction, then app is just the identity:

app (A : I -> Set) (a : A i0) (b : A i1) (e : Path A a b) (i : I) : A i
  i A a b e

Path reflexivity

We can implement refl, as expected, as a constant path:

refl (A : Set) (x : A) : Path (λi. A) x x
  λP. λabs. abs (λi. x)

Path congruence

We can apply a function to both sides of a Path:

cong (A : Set) 
     (B : A -> Set)
     (x : A)
     (y : A)
     (f : ∀ (a : A) -> B(a))
     (p : Path (λi. A) x y)
     : Path (λi. B (app (λi. A) x y p i)) (f x) (f y)
  λP. λabs. abs (λi. f (app (λi. A) x y p i))

Function extensionality

As expected, funext is very simple for the Path type. We just create a path abstraction that flips i and x:

funext
  (A : Type)
  (B : A -> Type)
  (f : ∀(x : A) -> B x)
  (g : ∀(x : A) -> B x)
  (h : ∀(x : A) -> Path (λi. B x) (f x) (g x))
  : Path (λi. ∀(x : A) -> B x) f g
  abs (λi. ∀(x : A) -> B x) (λi. λx. app (λi. B x) (f x) (g x) (h x) i)

Transport

Now the problem. While Path is great to work with, in order to be a reasonable equality type, we need a transport operation. Defining that seems to be non-trivial. After consulting the Cubical Agda paper, I've managed to implement its transport and transpPi:

transp (A : I -> Set) (i : I) (x : A i0) : A i1
  ?transp

transport (A : Set) (B : Set) (p : Path (λi. Set) A B) (a : A) : B
  transp (λi. app (λi. Set) A B p i) i0 a

transpPi (A : I -> Set) (B : (i : I) -> A(i) -> Set) (f : (x : A i0) -> B i0 x) (x : A i1) : B i1 x
  let fx : B i0 (transp _ i0 x)
         = f (transport (A i1) (A i0) (abs (λi. Set) (λi. A (not i))) x)
      be : Path (λi. Set) (B i0 (transp _ i0 x)) (B i1 (transp _ i1 x))
         = abs (λi. Set) (λj. B j (transp (λi. A (max (not i) j)) j x)
  in transport _ _ be fx

But as for transp, I do not know what to do. Agda says it is a primitive and isn't precise about how it computes. It does say, though, that transp _ i1 x = x; but that requires A to be constant when i = i1, otherwise we'd have x : A i0 and x : A i1 simultaneously, which is ill-typed! This is the first problem: we can't enforce that a function is constant on CoC+Self alone; replicating that would require some "hardcoded" access to a "count_variable_uses(x, term)" function. The second problem is that, on the i0 case, seems like we'd need to type-case on A i0, in order to specialize x : A i0 as x : ∀ (k : P i0) -> Q i0 k and then call transpPi. The nice thing is, since the only type former is Pi, this would complete the proof. But how would such type-case primitive work?

Questions

Finally, my questions are.

  1. Since, in CoC+Self, inside transp, we can't enforce that A is constant when i=i1, is there any other to write transp that doesn't require such ability?

  2. Is my reasoning that type-case is necessary to "pattern-match" on A i0 : Type right? If so, what is the correct elimination rule for Type?

  3. How exactly transp computes? The paper mentioned affirms that transp _ i1 x = x, but what about the other two cases (transp _ i0 x and transp _ ie x)? Is it possible to write how they would look like (even if just as a pseudo-code)?

(You can type-check the proofs above using this file and Formality.)

$\endgroup$
  • 2
    $\begingroup$ What are the categorical semantics of Self types? $\endgroup$ – Mike Shulman Sep 23 at 3:37
  • $\begingroup$ I see the type of your Nat refers to Nat. Do you have a reference for why/where/when this kind if "recursion" is sound? $\endgroup$ – Stefan Sep 23 at 14:35
  • 1
    $\begingroup$ @MikeShulman I don't know, check Aaron Stump's original paper for a more formal presentation. $\endgroup$ – MaiaVictor Sep 23 at 17:08
  • $\begingroup$ @Stefan the usage of Nat in Nat is necessary for Scott Encodings. I don't think it makes sense to reason about the soundness of a particular feature in isolation, it depends on the language on which said feature is inserted. Looking for sound languages that admit Scott Encodings might provide some answer to your question. Some may want to avoid Scott in favor of Church encodings which are easier to deal with, but I personally find that a mistake. $\endgroup$ – MaiaVictor Sep 23 at 17:14
  • $\begingroup$ @MaiaVictor: my question was indeed if you could point me to a sound language that admits this kind of encoding $\endgroup$ – Stefan Sep 23 at 17:59
8
$\begingroup$

This is not an answer but a very long comment.

I find the idea quite interesting. To keep things focused, I think it would be very good to have a clear idea of what it means for the encoding of cubical type theory to be correct, namely that it is sound and conservative.

Soundness just means you can encode everything (for instance, that you did not forget to encode cong) and that all the expected judgmental equalities (conversions) that are supposed to hold do hold. This should be the easy part.

Conservativity means that the encoding cannot do more than what it is supposed to. Suppose A is a type in cubical type theory and let A' be its encoding using self-types. Then we want

If A' is inhabited in type theory with self-types then A is inhabited in cubical type theory.

And given another type B encoded by B', we want:

If A' ≣ B' in type theory with self-types then A ≣ B' in cubical type theory.

I would particularly worry about the interval type I. In cubical type theory this is not a type! It is a pre-type that is treated specially. However, you are encoding it as an ordinary type, just like any other, and that sounds very fishy. I think there is a proof in cubical type theory showing that I cannot be an ordinary type but I don't remember it off the top of my head.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ I agree. From my experience, it makes sense that I cannot be an ordinary type, and I think I even see where things would break down: "transp" seems to require a "typecase" that treats "I" in a very "special" way. Regardless, the fact that all the definitions above behave identically to the "hardcoded" cubical primitives makes me think that, if we look into it further, we may find some "clever way" to let these definitions be internal libraries, keeping the language implementation itself minimal, which is my ultimate goal. $\endgroup$ – MaiaVictor Sep 21 at 18:25
  • $\begingroup$ For example, perhaps there is a whole class of "special types" (not just I) that can be "lifted" out of self-encodings into something that is more "part of the language". Or not, but answering that question even negatively (as in, "Interval must be a primitive") would give me insights about its nature (and then I'd accept it as a primitive on Formality :P). Regardless, I find it very unlikely that "transp" as a primitive will turn out to be the simplest way to add cubical features to a proof language. $\endgroup$ – MaiaVictor Sep 21 at 18:28
  • $\begingroup$ At the very least all the cubes I ⨉ I ⨉ ... ⨉I are special also. I do not think the interval must be special, but there should be distinction between pre-types and types. I wonder how exactly Cubical Agda gets around this. $\endgroup$ – Andrej Bauer Sep 21 at 18:40
  • $\begingroup$ Yep, seems like I is special exactly in the sense that a I in the context isn't like a normal variable in context. I hope I can get a deeper understanding of "why" and "how" it differs precisely. $\endgroup$ – MaiaVictor Sep 21 at 19:53
  • $\begingroup$ The semantic answer is that it's not a Kan cubical set, i.e., it is not fibered. $\endgroup$ – Andrej Bauer Sep 21 at 20:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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