faking universal quantification in constraints

[Nicolas Frisby]

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.frisby at 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
> <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
>>