<div><br></div><br><div class="gmail_quote">On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby <span dir="ltr"><<a href="mailto:nicolas.frisby@gmail.com">nicolas.frisby@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I'm simulating skolem variables in order to fake universal<br>
quantification in constraints via unsafeCoerce.<br>
<br>
<a href="http://hpaste.org/67121" target="_blank">http://hpaste.org/67121</a><br>
<br>
I'm not familiar with various categories of types from the run-time's<br>
perspective, but I'd be surprised if there were NOT a way to use this<br>
code to create run-time errors.<br>
<br>
Is there a way to make it safer? Perhaps by making Skolem act more<br>
like GHC's Any type? Or perhaps like the -> type? I'd like to learn<br>
about the varieties of types from the run-time's perspective.<br></blockquote><div><br></div><div>FWIW- I have a version of this concept packaged up in the constraints package.<div><br></div><div>I had a small example that abused flexible instances and MPTCs to cause the single Skolem version of my code to fail.</div>
<div><br></div><div>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.</div>
<div><br></div><div><a href="http://hackage.haskell.org/packages/archive/constraints/0.3/doc/html/src/Data-Constraint-Forall.html">http://hackage.haskell.org/packages/archive/constraints/0.3/doc/html/src/Data-Constraint-Forall.html</a></div>
<div><br></div></div></div>