faking universal quantification in constraints

[Nicolas Frisby]

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
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

[Dimitrios Vytiniotis-2]

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: [hidden email] [mailto:glasgow-haskell-
> [hidden email]] 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

[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
<[hidden email]> 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: [hidden email] [mailto:glasgow-haskell-
>> [hidden email]] 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
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

[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
<[hidden email]> 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
> <[hidden email]> 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: [hidden email] [mailto:glasgow-haskell-
>>> [hidden email]] 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
>>> [hidden email]
>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

[Edward A Kmett]

On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby <[hidden email]> wrote:

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.

FWIW- I have a version of this concept packaged up in the constraints package.

I had a small example that abused flexible instances and MPTCs to cause the single Skolem version of my code to fail.

However, when I refined it to use two Skolem variables I wasn't able to derive sufficient Oleggery to break it. That said, an absence of a counter-example isn't a proof that it can't exist.

http://hackage.haskell.org/packages/archive/constraints/0.3/doc/html/src/Data-Constraint-Forall.html

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

[Nicolas Frisby]

Great! I'll take a whack at it ;)

On Tue, Apr 17, 2012 at 4:07 PM, Edward Kmett <[hidden email]> wrote:

>
>
> On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby <[hidden email]>
> wrote:
>>
>> 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.
>
>
> FWIW- I have a version of this concept packaged up in the constraints
> package.
>
> I had a small example that abused flexible instances and MPTCs to cause the
> single Skolem version of my code to fail.
>
> However, when I refined it to use two Skolem variables I wasn't able to
> derive sufficient Oleggery to break it. That said, an absence of a
> counter-example isn't a proof that it can't exist.
>
> http://hackage.haskell.org/packages/archive/constraints/0.3/doc/html/src/Data-Constraint-Forall.html
>

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

[Nicolas Frisby]

I built a (really ugly) dictionary for (Int ~ Char) using
Data.Constraints.Forall. I'm fairly confident it could be generalized
to a polymorphic coercion (a ~ b).

  http://hpaste.org/67180

I cheated with overlapping instances, but you left me no choice ;).
Anyone who pulls this kind of stunt is definitely trying to subvert
it; so I vote "trustworthy".

I'm adopting Data.Constraints.Forall for my local experimentation.
Thanks for pointing it out.

On Tue, Apr 17, 2012 at 4:15 PM, Nicolas Frisby
<[hidden email]> wrote:

> Great! I'll take a whack at it ;)
>
> On Tue, Apr 17, 2012 at 4:07 PM, Edward Kmett <[hidden email]> wrote:
>>
>>
>> On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby <[hidden email]>
>> wrote:
>>>
>>> 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.
>>
>>
>> FWIW- I have a version of this concept packaged up in the constraints
>> package.
>>
>> I had a small example that abused flexible instances and MPTCs to cause the
>> single Skolem version of my code to fail.
>>
>> However, when I refined it to use two Skolem variables I wasn't able to
>> derive sufficient Oleggery to break it. That said, an absence of a
>> counter-example isn't a proof that it can't exist.
>>
>> http://hackage.haskell.org/packages/archive/constraints/0.3/doc/html/src/Data-Constraint-Forall.html
>>

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

[Edward A Kmett]

On Tue, Apr 17, 2012 at 6:40 PM, Nicolas Frisby <[hidden email]> wrote:

I built a (really ugly) dictionary for (Int ~ Char) using
Data.Constraints.Forall. I'm fairly confident it could be generalized
to a polymorphic coercion (a ~ b).

 http://hpaste.org/67180

I cheated with overlapping instances, but you left me no choice ;).
Anyone who pulls this kind of stunt is definitely trying to subvert
it; so I vote "trustworthy".

 

I'm adopting Data.Constraints.Forall for my local experimentation.
Thanks for pointing it out.

With overlapping instances you can build any dictionary you want, even without unsafeCoerce, so I'll leave it in. ;)

I should probably avoid using (,) as well, to further stymie such efforts. ;P

-Edward

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users