Hi Alexis,
I'm not aware of any work in this direction. It's an interesting idea to think
about. A few such disconnected thoughts:
- You could refactor the type family equation to be `F a b = a ~ b`. Then your
program would be accepted. And -- assuming the more sophisticated example is
also of
Hi Richard,
Thanks for the pointer to constrained type families—that’s helpful to clarify
some of my thoughts about this, and it is indeed relevant! One example I had in
my real code seems difficult to express even with constrained type families,
however; here is a stripped-down version of it:
> On Dec 30, 2019, at 11:16 AM, Alexis King wrote:
>
> I don’t know if there is a way to encode those using the constraint language
> available in source Haskell today.
I gave it a good try, but failed. The trick I was hoping to leverage was
*partial improvement*. Here is an example of parti
> On Jan 4, 2020, at 20:38, Richard Eisenberg wrote:
>
> I thought that, maybe, we could use partial improvement to give you what you
> want
I think that improvement alone cannot possibly be enough here, as improvement
by its nature does not provide evidence. Improvement allows us to take a se
You're absolutely right that improvement doesn't solve your problem. But what I
didn't say is that there is no real reason (I think) that we can't improve
improvement to produce givens. This would likely require a change to the
coercion language in Core (and thus not to be taken lightly), but if
I've read this thread, superficially so far. But I'm puzzled about the goal.
| type family F a b :: Constraint where
| F a a = ()
|
| eq :: F a b => a :~: b
| eq = Refl
This is rejected, and it's not in the least bit puzzling! You have evidence
for (F a b) and you need to pro
> On Jan 6, 2020, at 2:52 PM, Simon Peyton Jones via ghc-devs
> wrote:
>
> | type family F a b :: Constraint where
> | F a a = ()
> |
> | eq :: F a b => a :~: b
> | eq = Refl
>
> This is rejected, and it's not in the least bit puzzling! You have evidence
> for (F a b) and
> On Jan 6, 2020, at 08:52, Simon Peyton Jones wrote:
>
> This is rejected, and it's not in the least bit puzzling! You have evidence
> for (F a b) and you need to prove (a~b) -- for any a and b. Obviously you
> can't. And in Core you could write (eq @Int @Bool (error "urk")) and you
> joll
> On Jan 6, 2020, at 12:05, Alexis King wrote:
>
>type family F a b where
> F a b = () -- regular (), not (() :: Constraint)
(Err, sorry, this should be `F a a = ()`. But I think you can understand what
I’m getting at.)
___
ghc-devs mailing l
> On Jan 6, 2020, at 05:29, Richard Eisenberg wrote:
>
> You're absolutely right that improvement doesn't solve your problem. But
> what I didn't say is that there is no real reason (I think) that we can't
> improve improvement to produce givens. This would likely require a change to
> the co
ones
| Cc: ghc-devs
| Subject: Re: Superclasses of type families returning constraints?
|
| > On Jan 6, 2020, at 08:52, Simon Peyton Jones
| wrote:
| >
| > This is rejected, and it's not in the least bit puzzling! You have
| evidence for (F a b) and you need to prove (a~b) -- for
> On Jan 6, 2020, at 15:41, Simon Peyton Jones wrote:
>
> Ah, I see a bit better now. So you want a way to get from evidence that
> co1 :: F a b ~# ()
> to evidence that
> co2 :: a ~# b
>
> So you'd need some coercion form like
> co2 = runBackwards co1
>
> or something, where
12 matches
Mail list logo
