faking universal quantification in constraints

[Dimitrios Vytiniotis]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: UnsafeMain.hs
Type: application/octet-stream
Size: 1425 bytes
Desc: UnsafeMain.hs
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120417/959d5ee2/attachment.obj>