Add support for nested mutual blocks again

[mortberg]

The PR #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 [email protected] wrote:

The PR #44 #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 #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" [email protected] 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 [email protected]
wrote:

The PR #44 #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
#48 (comment),
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 [email protected] 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" [email protected] 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 [email protected]
wrote:

The PR #44 #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
#48 (comment),
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 #48 (comment), 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 [email protected] 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 #48 (comment), 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