Open shlevy opened 8 years ago
@edwinb
Good
should be rejected as well.
Hm, why should it be? Because of non-positivity in the type?
@shlevy I believe you shouldn't be able to index a type by itself, right?
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.
So I can't even get Agda to accept the definition.
Does Agda support induction-induction?
@shlevy It should support that yes.
@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
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?
@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)
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?
@shlevy I believe the problem is that yours depend on a data constructor in a type constructor which this does not.
You might get around it by taking Foo a
in IsBase
I would guess
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
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.
@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?
Any thoughts on this? Still seeing the behavior in 1.2.0
@shlevy Sorry, still not sure.
Given this code:
The repl gives:
Good
seems morally equivalent toBad
to me, so ifGood
is right to pass the positivity checker can we extend it so thatBad
does too?