Useless(?) hComp’s with empty systems when using higher inductive types

[guillaumebrunerie]

In the code below, the normal form of the term p is

<!0> hComp SuspS1 (merid {SuspS1} (hComp S1 base []) @ !0) [].

It seems strange that we get hComp S1 base [] instead of just base, and it gives us terms full of seemingly useless hComp’s with empty systems.

module bug where

data S1 = base
        | loop <i> [(i = 0) -> base, (i = 1) -> base]

data SuspS1 = north
            | south
            | merid (a : S1) <i> [(i = 0) -> north, (i = 1) -> south]

p : PathP (<_> SuspS1) (comp (<_> SuspS1) north []) (comp (<_> SuspS1) south [])
 = <i> comp (<_> SuspS1) (merid{SuspS1} base @ i) []

[mortberg]

I noticed the same thing when I tried a very simple example related to propositional truncation a few weeks ago, see my comment on: #62

I don't understand if all of these hComp's with empty systems are really needed or if there is a way to do things so that we don't get them (or at least not this many of them)...

[coquand]

For this example they should not be needed since the type S1 is a constant type and so one can use the identity function for “forward”. But it is not clear how to implement this optimisation (to recognise when one can use identity function for “forward”) in a satisfactory way.

…

On 8 Jun 2017, at 21:23, Anders Mörtberg ***@***.***> wrote: I noticed the same thing when I tried a very simple example related to propositional truncation a few weeks ago, see my comment on: #62 <#62> I don't understand if all of these hComp's with empty systems are really needed or if there is a way to do things so that we don't get them (or at least not this many of them)... — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#67 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACrXlP5eVWAwnm-WvC6pUy-8uZU6feIjks5sCEoegaJpZM4N0c0Q>.

[mortberg]

Could it make sense to have a computation rule so that hComp with the empty system disappears for point constructors? This way I think HITs would compute like normal inductive types for point constructors.

[coquand]

Semantically this is not justified since e.g. if we define g : S1 -> A from a : A and l : Path A a a by g base = a g (loop r) = l r g (hcomp^i [psi -> u] u0) = comp^i A [psi -> g u] (g u0) we have g (hcomp^i [psi -> u] u0) = comp^i A [psi -> g u] (g u0) for psi <> 0, and by substitution if psi = 0, we should have g (hcomp^i [] u0) = comp^i A [] (g u0) which may be different from g u0 if A is not “regular” Syntactically this will result in a non Church-Rosser computation system. (And the fact that we have non “regular” types in this approach is motivated geometrically by the fact that the geometric composition is not regular, and by Dan Licata’s analysis of non regularity of the universe.)

…

On 9 Jun 2017, at 12:47, Anders Mörtberg ***@***.***> wrote: Could it make sense to have a computation rule so that hComp with the empty system disappears for point constructors? This way I think HITs would compute like normal inductive types for point constructors. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#67 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACrXlGDh2nHcN0Y6wjv8WGeCNeFQGuy1ks5sCSKvgaJpZM4N0c0Q>.

[mortberg]

Ah right, I see. Thanks for reminding me of this! So I guess the only hope is to do what you suggest and make forward smarter so that it behaves like the identity function when appropriate...

[jonsterling]

@coquand Thank you for the very helpful comments. I have a question about this failure of confluence...

My understanding of the operational interpretation (as in Simon's paper) of cubicaltt is that the computability predicates are required to be compatible with evaluating and substituting in any order.

So, if we were to adopt this computation rule for empty compositions in constant types (like S1), I'm not so sure that the equation g (hcomp^i [psi -> u] u0) = comp^i A [psi -> g u] (g u0) would even hold / be induced by the computability predicate for A, since this identification is not stable under substitutions: as you say, if a substitution renders the system empty, then the application would reduce to g u0.

Naïvely, it seems like adopting the computation rule for empty compositions in constant types would not break confluence, but rather it would mean that we could not directly commute compositions with functions in the style of the equations you give for g at the top.

I wonder if it would be interesting to consider a version of cubicaltt where you cannot define such a function g: the version of g that could be defined in such a language would be one where the third equation has some side condition, such as that the system is not empty, or maybe that the composition is not a redex. I believe that the Angiuli/Harper type theory behaves this way, for instance.

[coquand]

On 9 Jun 2017, at 17:57, Jonathan Sterling ***@***.***> wrote: @coquand <https://github.com/coquand> Thank you for the very helpful comments. I have a question about this failure of confluence... My understanding of the operational interpretation (as in Simon's paper) of cubicaltt is that the computability predicates are required to be compatible with evaluating and substituting in any order. So, if we were to adopt this computation rule for empty compositions in constant types (like S1), I'm not so sure that the equation g (hcomp^i [psi -> u] u0) = comp^i A [psi -> g u] (g u0) would even hold / be induced by the computability predicate for A, since this identification is not stable under substitutions: as you say, if a substitution renders the system empty, then the application would reduce to g u0. Naïvely, it seems like adopting the computation rule for empty compositions in constant types would not break confluence, but rather it would mean that we could not directly commute compositions with functions in the style of the equations you give for g at the top. I wonder if it would be interesting to consider a version of cubicaltt where you cannot define such a function g: the version of g that could be defined in such a language would be one where the third equation has some side condition, such as that the system is not empty, or maybe that the composition is not a redex. I believe that the Angiuli/Harper type theory behaves this way, for instance

What would be the operational semantics of S1 elimination along these lines?

[jonsterling]

@coquand The operational semantics of S1 elimination would proceed as usual when its principal argument is a value—the only difference is that under the discussed circumstances, hcomp S1 base [] would not be a value, so there would not need to be any case for it in the operational semantics of S1 elimination...

Whilst I think the operational semantics can be made sense of, I am less certain that this makes semantic sense overall. After discussing with Carlo Angiuli, we are a little worried that such a rule (which computes the empty composition away at the circle) would be destructive for other reasons; I cannot say precisely what is the problem, but I am concerned that such a computation rule for the circle might, in conjunction with the elimination rule for the circle, lead to a collapse of empty compositions in other types (such as the universe).

[mortberg]

I had a look at this with @guillaumebrunerie today and we noticed that on the hcomptrans branch the comp with the empty system for S1 seems to have disappeared for this example:

> :n p
NORMEVAL: <i0> hcomp SuspS1 (merid {SuspS1} base @ i0) []

So it seems like the new algorithm for comp for HITs computes a bit better, at least for S1.

[jonsterling]

@mortberg heh! That's good news.