faking universal quantification in constraints

[Nicolas Frisby]

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
<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!
>
> d-
>
>
>
>
>> -----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.
>>
>>   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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>