[Haskell-cafe] Type constraint rewrite rules

[rowan goemans]

I haven't used it but something like that exists

https://github.com/gelisam/typelevel-rewrite-rules

Rowan Goemans

On 1/22/23 22:16, Henning Thielemann wrote:
>
> Has anyone thought about rewrite rules for type constraints as 
> light-weight alternative to type-checker plugins?
>
> Rewrite rules could be
>
>   n + 'Zero -> n
>
>   Back (Forth a) -> a
>      for closed type families Back and Forth, where Back is the 
> inverse of Forth
>
>
> Ideally the programmer would also provide a correctness proof for the 
> proposed rewrite, e.g. with a function that generates a
>
> data BackForthProof a = (Back (Forth a) ~ a) => BackForthProof
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.