Allow referencing previous constructors in half-positivity check

[shlevy]

Given this code:

data MaybeFoo : Type

data Foo : MaybeFoo -> Type

data MaybeFoo : Type where
  Nothing : MaybeFoo
  Just : (Foo Nothing) -> MaybeFoo

data IsBase : Foo Nothing -> Type

data Foo : MaybeFoo -> Type where
  Base : Foo Nothing
  Good : {auto isBase : IsBase base} -> Foo (Just base)
  Bad : Foo (Just Base)

data IsBase : Foo Nothing -> Type where
  BaseIsBase : IsBase Base

The repl gives:

λΠ> :def Good
Compiled patterns:
[TyDecl: DCon {nt_tag = 1, nt_arity = 2, nt_unique = False} (base : Main.Foo Main.Nothing) -> Main.IsBase base -> Main.Foo (Main.Just base)]

Total
λΠ> Good
Good : Foo (Just Base)
λΠ> :def Bad
Compiled patterns:
[TyDecl: DCon {nt_tag = 2, nt_arity = 0, nt_unique = False} Main.Foo (Main.Just Main.Base)]

not strictly positive
λΠ> Bad
Bad : Foo (Just Base)

Good seems morally equivalent to Bad to me, so if Good is right to pass the positivity checker can we extend it so that Bad does too?

[shlevy]

@edwinb

[ahmadsalim]

Good should be rejected as well.

[shlevy]

Hm, why should it be? Because of non-positivity in the type?

[ahmadsalim]

@shlevy I believe you shouldn't be able to index a type by itself, right?

[shlevy]

It doesn't obviously have the same problems that non-positivity in the constructor arguments, but I have no idea whether it's theoretically sound or not.

[ahmadsalim]

So I can't even get Agda to accept the definition.

[shlevy]

Does Agda support induction-induction?

[ahmadsalim]

@shlevy It should support that yes.

[ahmadsalim]

@shlevy This is the translation that I provided to Agda:

mutual
  data MaybeFoo : Set where
    nothing : MaybeFoo
    just : (Foo nothing) -> MaybeFoo

  data Foo : MaybeFoo -> Set where
    base : Foo nothing
    good : ∀ {b} {{isBase : IsBase b}} -> Foo (just b)
    bad : Foo (just base)

  data IsBase : Foo nothing -> Set where
    base·is·base : IsBase base

[shlevy]

Hmm, I think I must misunderstand induction-induction then. What's an example of a type and a family over that type that needs to be defined mutually that should be accepted?

[ahmadsalim]

@shlevy
From https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/talks/BCTCS_2010/indind_BCTCS.pdf:

mutual
  data Platform : Type where
    Ground : Platform
    Extension : (p : Platform) -> (b : Building p) -> Platform

  data Building : Platform -> Type where
    OnTop : (p : Platform) -> Building p
    HangingUnder : (p : Platform) -> (b : Building p) -> Building (Extension p b)

> HangingUnder (Extension Ground (OnTop Ground)) (OnTop ((Extension Ground (OnTop Ground))))

HangingUnder (Extension Ground (OnTop Ground))
             (OnTop (Extension Ground (OnTop Ground))) : Building (Extension (Extension Ground (OnTop Ground))
                                                                             (OnTop (Extension Ground (OnTop Ground))))

It is usually used for a type theoretic encoding of types depending on contexts I believe (which is referred to in the presentation I linked above)

[shlevy]

So desugaring the mutual, this is basically:

data Platform : Type

data Building : Platform -> Type

data Platform : Type where
  Ground : Platform
  Extension : (p : Platform) -> (b : Building p) -> Platform

data Building : Platform -> Type where
  OnTop : (p : Platform) -> Building p
  HangingUnder : (p : Platform) -> (b : Building p) -> Building (Extension p b)

That doesn't seem to far from mine... Just change Building to have one constructor of type Building Ground. So is the problem that in my case the mutual type is an index, not a parameter (I'm actually not sure if the Platform is actually a parameter to Building given the definition of HangingUnder...)? Or is there something else that makes this definition OK and mine not?

[ahmadsalim]

@shlevy I believe the problem is that yours depend on a data constructor in a type constructor which this does not.

[ahmadsalim]

You might get around it by taking Foo a in IsBase I would guess

[ahmadsalim]

OK, so Agda accepts:

mutual
  data MaybeFoo : Set where
    nothing : MaybeFoo
    just : (Foo nothing) -> MaybeFoo

  data Foo : MaybeFoo -> Set where
    base : Foo nothing
    good : ∀ {b} {{isBase : IsBase b}} -> Foo (just b)
    bad : Foo (just base)

  data IsBase : {A : MaybeFoo} -> Foo A -> Set where
    base·is·base : IsBase base

[shlevy]

Huh, really! So Agda is OK with bad directly? Does the equivalent transformation to my original code (just making IsBase take a MaybeFoo instead of directly using Nothing, right?) work? I don't have a recent Idris on this computer.

[ahmadsalim]

@shlevy Yeah, I am getting confused now on whether it should be accepted or not :). To be honest, I am not a type theory expert, so I wouldn't know. Maybe someone like @david-christiansen could give a hint?

[shlevy]

Any thoughts on this? Still seeing the behavior in 1.2.0

[ahmadsalim]

@shlevy Sorry, still not sure.