Thanks! I'll analyze what you've done here. One thing that jumps out at me is that you're using flop twice. I think this violates an invariant that I was trying(/"hoping") to maintain by not exporting Skolem. I'll let you know once I look at it longer.
Thanks for taking the time to do this. On Tue, Apr 17, 2012 at 1:40 PM, Dimitrios Vytiniotis <dimit...@microsoft.com> wrote: > > Hi Nick, I cannot say that I understand very well what you have in your mind, > nor the > signatures of the classes you have in your module, but as you expected your > program > is unsafe (and I've probably attached one of the most obfuscated ways to show > it, many > apologies for this! At least my code can offer a good laugh to people :-)) > > Because I do not understand what you are doing in this module, I also do not > understand > how to make it safer -- I just can safely tell you that using your forall_S > one can create a > Leibniz equality: > > forall a c. c Skolem -> c a > > which (by a free theorem) means that ALL types must be equal to Skolem, and > my code > exploits exactly this to equate Char to Skolem to Int -> Int. The fact that > you can't name > Skolem in the new module because it is not exported is kind of irrelevant ... > > Regarding impredicativity in GHC, we are still unfortunately on the > whiteboard ... > > Hope this helps! > > d- > > > > >> -----Original Message----- >> From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell- >> users-boun...@haskell.org] On Behalf Of Nicolas Frisby >> Sent: Monday, April 16, 2012 11:58 PM >> To: glasgow-haskell-users >> Subject: faking universal quantification in constraints >> >> I'm simulating skolem variables in order to fake universal quantification in >> constraints via unsafeCoerce. >> >> http://hpaste.org/67121 >> >> I'm not familiar with various categories of types from the run-time's >> perspective, but I'd be surprised if there were NOT a way to use this code to >> create run-time errors. >> >> Is there a way to make it safer? Perhaps by making Skolem act more like >> GHC's Any type? Or perhaps like the -> type? I'd like to learn about the >> varieties of types from the run-time's perspective. >> >> I know Dimitrios Vytiniotis is trying to implement these legitimately in GHC, >> but I don't know much about that project's status, nor any documentation >> indicating how to try it out in GHC HEAD (e.g. what's the syntax?). Is there >> a >> page on the GHC wiki or something to check that sort of thing? >> >> I wonder how far this Forall_S trick can take me in the interim towards >> Vytiniotis' objective functionality when paired with a (totally safe) class >> for >> implication. >> >> > class Implies (ante :: Constraint) (conc :: Constraint) where >> > impliesD :: Dict ante -> Dict conc >> >> Thanks, >> Nick >> >> _______________________________________________ >> Glasgow-haskell-users mailing list >> Glasgow-haskell-users@haskell.org >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
