Add support for nested mutual blocks again

[mortberg]

The PR https://github.com/mortberg/cubicaltt/pull/44 breaks support for nested mutual blocks.

[coquand]

I did not have time to react before, but this might be an issue since we then loose a natural way to have inductive-recursive definitions.

On 29 Jul 2016, at 10:45, Anders Mörtberg notifications@github.com wrote:

The PR #44 https://github.com/mortberg/cubicaltt/pull/44 breaks support for nested mutual blocks.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/mortberg/cubicaltt/issues/48, or mute the thread https://github.com/notifications/unsubscribe-auth/ACrXlKOE13Ol3yXs72IuRPOPdi7Jc_TRks5qacurgaJpZM4JYCZs.

[mortberg]

Do you have an example that requires multiple levels of nested mutual blocks?

The only examples we have so far only required one level and seem to work just fine. Once I have an example I can try to come up with a solution that works.

On Jul 29, 2016 15:40, "coquand" notifications@github.com wrote:

I did not have time to react before, but this might be an issue since we then loose a natural way to have inductive-recursive definitions.

On 29 Jul 2016, at 10:45, Anders Mörtberg notifications@github.com wrote:

The PR #44 https://github.com/mortberg/cubicaltt/pull/44 breaks support for nested mutual blocks.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub < https://github.com/mortberg/cubicaltt/issues/48>, or mute the thread < https://github.com/notifications/unsubscribe-auth/ACrXlKOE13Ol3yXs72IuRPOPdi7Jc_TRks5qacurgaJpZM4JYCZs .

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/mortberg/cubicaltt/issues/48#issuecomment-236182759, or mute the thread https://github.com/notifications/unsubscribe-auth/ABBNfS_lStDW3dTpGD_xxZmhnp1Nbg_Eks5qagKzgaJpZM4JYCZs .

[coquand]

What do you mean by “multiple levels of nested mutual blocks”?

The example I had in mind was something like

mutual

data V = n | pi (x:V) (f:El x -> V)

El : V -> U = split n -> Nat pi x f -> (u:El x) -> El (f x)

Thierry

On 29 Jul 2016, at 14:59, Anders Mörtberg notifications@github.com wrote:

Do you have an example that requires multiple levels of nested mutual blocks?

The only examples we have so far only required one level and seem to work just fine. Once I have an example I can try to come up with a solution that works.

On Jul 29, 2016 15:40, "coquand" notifications@github.com wrote:

I did not have time to react before, but this might be an issue since we then loose a natural way to have inductive-recursive definitions.

On 29 Jul 2016, at 10:45, Anders Mörtberg notifications@github.com wrote:

The PR #44 https://github.com/mortberg/cubicaltt/pull/44 breaks support for nested mutual blocks.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub < https://github.com/mortberg/cubicaltt/issues/48>, or mute the thread < https://github.com/notifications/unsubscribe-auth/ACrXlKOE13Ol3yXs72IuRPOPdi7Jc_TRks5qacurgaJpZM4JYCZs .

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/mortberg/cubicaltt/issues/48#issuecomment-236182759, or mute the thread https://github.com/notifications/unsubscribe-auth/ABBNfS_lStDW3dTpGD_xxZmhnp1Nbg_Eks5qagKzgaJpZM4JYCZs .

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/mortberg/cubicaltt/issues/48#issuecomment-236187684, or mute the thread https://github.com/notifications/unsubscribe-auth/ACrXlBTU_VTH54lxwvAdlCIVUkeuvlVdks5qagdHgaJpZM4JYCZs.

[mortberg]

That works just fine. The problem is when you have nested mutual blocks:

mutual
  mutual
    data V = n | pi (x:V) (f:El x -> V)

    El : V -> U = split
      n -> nat
      pi x f -> (u:El x) -> El (f u)

If you input this the resolver will just crash. I can make it not crash, or if there is some interesting example that needs mutual's inside a mutual I can try to come up with something that works.

[coquand]

Maybe I misunderstood: is this connected to the optimisation suggested by Guillaume or it is a different thing?

On 29 Jul 2016, at 16:00, Anders Mörtberg notifications@github.com wrote:

That works just fine. The problem is when you have nested mutual blocks:

mutual mutual data V = n | pi (x:V) (f:El x -> V)

El : V -> U = split
  n -> nat
  pi x f -> (u:El x) -> El (f u)

If you input this the resolver will just crash. I can make it not crash, or if there is some interesting example that needs mutual's inside a mutual I can try to come up with something that works.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/mortberg/cubicaltt/issues/48#issuecomment-236204311, or mute the thread https://github.com/notifications/unsubscribe-auth/ACrXlHWDk4_uxre8HnyP0bzvOHL1B8DSks5qahWngaJpZM4JYCZs.

[5HT]

I faced a problem of nested mutuals and here is my example which is an extended version of @coquand's example of IR encoding.

-- Mahlo Universes a la Setzer

module ir where

mutual

data V
    = pi_  (x: V) (y: Elv x -> V)
    | uni_ (f: (x: V) -> (Elv x -> V) -> V)
           (g: (x: V) -> (y: Elv x -> V) -> (Elv (f x y) -> V) -> V)

Elv: V -> U = split
    pi_ a b -> (x: Elv a) -> Elv (b x)
    uni_ f g -> Universe f g

mutual

data Universe
    (f: (x: V) -> (Elv x -> V) -> V)
    (g: (x: V) -> (y: Elv x -> V) -> (Elv (f x y) -> V) -> V)
    = fun_ (x: Universe f g) (_: Elt f g x -> Universe f g)
    | f_   (x: Universe f g) (_: Elt f g x -> Universe f g)
    | g_   (x: Universe f g)
           (y: Elt f g x -> Universe f g)
           (z: Elv (f (Elt f g x) (\(a: Elt f g x) -> y a)))

Elt: (f: (x: V) -> (Elv x -> V) -> V) ->
     (g: (x: V) -> (y: Elv x -> V) -> (Elv (f x y) -> V) -> V) ->
     Universe f g -> V = undefined

Here you can see, that in Elv second part of functor should transport to Universe. This code is typechecked with following error:

Parsed "ir.ctt" successfully!
cubical: Resolver.hs:(304,34)-(327,55): Non-exhaustive patterns in case