faking universal quantification in constraints

Edward Kmett ekmett at gmail.com
Tue Apr 17 23:07:17 CEST 2012

On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby <nicolas.frisby at gmail.com>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

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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120417/9157c74f/attachment-0001.htm>

More information about the Glasgow-haskell-users mailing list