Re: [Haskell-cafe] Type constraint rewrite rules
... rewrite rules for type constraints ...
That's what FunDeps are, with the advantage you can stipulate multiple/multi-directional rewrites. (With a bit of effort you can support three FunDeps for `Nat` Plus.) The more I think about it, the more it seems type-land 'solving' is not the same job as term-land 'evaluating'; and Type Families are the wrong tool for the job. AntC
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.
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@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.
participants (2)
-
Anthony Clayden -
Henning Thielemann