[Haskell-cafe] Type constraint rewrite rules

Anthony Clayden anthony.d.clayden at gmail.com
Fri Jan 27 06:45:22 UTC 2023


Thanks Henning, and apologies for the delay in replying.

I more had in mind your `n + 'Zero -> n` example. With cunning overlaps you
can also achieve `'Zero + n -> n`; and even from result 'Zero improve both
arguments to 'Zero.

With class ForthBack, a FunDep right-to-left would (maybe) expand  `a` to
`Forth (Back a)` -- which hardly seems helpful and is anyway not true:
`Forth (Forth (Back (Back a)))` would be just as legit.

That kind of recursion-depth-sensitive normalisation is possible with
FunDeps and overlaps. But I'd need to recharge my Oleg batteries.

On Mon, 23 Jan 2023 at 21:23, Henning Thielemann <
lemming at henning-thielemann.de> wrote:

>
> On Mon, 23 Jan 2023, Anthony Clayden wrote:
>
> > > ... rewrite rules for type constraints ...
>
> > That's what FunDeps are, with the advantage you can stipulate
> > multiple/multi-directional rewrites.
>
> How would you simplify Forth (Back a) to 'a' automatically with FunDeps?
>
> I could define
>
>    class ForthBack a b | a -> b, b -> a where
>
> but then I would have constraint ForthBack a b and it does not go away.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20230127/dd5d7e4d/attachment.html>


More information about the Haskell-Cafe mailing list