faking universal quantification in constraints
nicolas.frisby at gmail.com
Tue Apr 17 23:15:06 CEST 2012
Great! I'll take a whack at it ;)
On Tue, Apr 17, 2012 at 4:07 PM, Edward Kmett <ekmett at gmail.com> wrote:
> On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby <nicolas.frisby at gmail.com>
>> I'm simulating skolem variables in order to fake universal
>> quantification in constraints via unsafeCoerce.
>> 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.
More information about the Glasgow-haskell-users