-
Notifications
You must be signed in to change notification settings - Fork 642
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Proof of Void using type constructor injectivity #3687
Comments
Yikes! On the one hand, we can fix this by turning off type constructor injectivity. On the other hand, this would break a lot of other things (mostly involving interfaces). Any ideas? |
So this is leading me down a rabbit hole, which is very interesting. But I suppose there is one question which could lead to at least a temporary fix: even if type constructors aren't injective in general, are there any circumstances under which we can know they are injective? |
Here is the original source for this example:
@edwinb I'm also curious about this question, but I didn't manage to find an answer in the literature. |
@edwinb An option would be to not treat big forced arguments (functions that involve |
@edwinb I'm sorry I threw this up on your day off! I don't know what the fix is, exactly because of the interface issue. I suppose the place to start is to look at how Agda's instance arguments work around the lack of definitional type constructor injectivity. |
Regardless of type constructor injectivity (which is still good to get rid of), I think this exact example is just another instance of #3194: if I change built-in pair type to module ProveVoid
data MPair : (a : Type) -> (P : a -> Type) -> Type where
MkMPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> MPair a P
%default total
data In : (f : Type -> Type) -> Type where
MkIn : In f
-- This step requires definitional type constructor injectivity and is
-- the source of the problem.
injIn : In x = In y -> x = y
injIn Refl = Refl
P : Type -> Type
P x = MPair (Type -> Type) (\a => (In a = x, a x -> Void))
inP : Type
inP = In P
oops : P ProveVoid.inP -> Void
oops (MkMPair a (ha0, ha1)) =
let ohNo : (P (In P) -> Void) = replace {P=\ x => x (In P) -> Void} (injIn ha0) ha1
in ohNo (MkMPair P (Refl, ohNo))
total -- for extra oumph!
ohNo : Void
ohNo =
let foo : P ProveVoid.inP = (MkMPair P (Refl, oops))
in oops foo and of course if I move |
On Sun, Mar 12, 2017 at 6:29 PM, David Christiansen ***@***.***> wrote:
I don't know what the fix is, exactly because of the interface issue.
What complications do interfaces add to the problem?
Cheers,
Miles
…--
Miles Sabin
tel: +44 7813 944 528
skype: milessabin
gtalk: miles@milessabin.com
http://milessabin.com/blog
http://twitter.com/milessabin
|
@milessabin Implementation (type class instace) resolution relies on type constructor injectivity to resolve that e.g. I am not sure how essential it is, i.e., whether there is an acceptable workaround. I believe someone (@yanok ? ) tried to turn it off and it broke a few things, so it is definitely used currently. |
Well, maybe https://lirias.kuleuven.be/bitstream/123456789/582749/1/CW705.pdf could work better, but I don't know how much effort it requires and whether it does avoid issues with type constructor injectivity. |
I hadn't realized that type constructor injectivity caused inconsistency without excluded middle in the past. But @leodemoura pointed me at an example on the Lean issue tracker that proves
Void
without any postulates, relying on type constructor injectivity alone. I ported it to Idris.The following code type checks in master for me:
The text was updated successfully, but these errors were encountered: