RE: faking universal quantification in constraints

2012-04-17 Thread 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

Re: faking universal quantification in constraints

2012-04-17 Thread 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

Re: faking universal quantification in constraints

2012-04-17 Thread 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

Re: faking universal quantification in constraints

2012-04-17 Thread Edward Kmett
On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby nicolas.fri...@gmail.comwrote: 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

Re: faking universal quantification in constraints

2012-04-17 Thread Nicolas Frisby
Great! I'll take a whack at it ;) On Tue, Apr 17, 2012 at 4:07 PM, Edward Kmett ekm...@gmail.com wrote: On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby nicolas.fri...@gmail.com wrote: I'm simulating skolem variables in order to fake universal quantification in constraints via unsafeCoerce.

Re: faking universal quantification in constraints

2012-04-17 Thread 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

Re: faking universal quantification in constraints

2012-04-17 Thread Edward Kmett
On Tue, Apr 17, 2012 at 6:40 PM, Nicolas Frisby nicolas.fri...@gmail.comwrote: 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