faking universal quantification in constraints
nicolas.frisby at gmail.com
Tue Apr 17 21:14:27 CEST 2012
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
Thanks for taking the time to do this.
On Tue, Apr 17, 2012 at 1:40 PM, Dimitrios Vytiniotis
<dimitris at 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!
>> -----Original Message-----
>> From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-
>> users-bounces at 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.
>> 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
>> > class Implies (ante :: Constraint) (conc :: Constraint) where
>> > impliesD :: Dict ante -> Dict conc
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users at haskell.org
More information about the Glasgow-haskell-users