In http://hpaste.org/67172, I've simplified your demonstration to define a function
> uhoh :: forall a b. Dict (a ~ b) Essentially, I had forgot about ~ constraints. The reason I wasn't exporting Skolem was so that if there were a satisfiable constraint (c Skolem), I could infer that the corresponding instances was totally polymorphic in the argument. That's bogus reasoning because of ~ (and hence fundeps, as you used). Thanks again. On Tue, Apr 17, 2012 at 2:14 PM, Nicolas Frisby <nicolas.fri...@gmail.com> wrote: > 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
