How would we convert this:
import Data.Leibniz (type (~))
data Expr a
= Add (Expr Int) (Expr Int) (a ~ Int)
| Eq (Expr Int) (Expr Int) (a ~ Boolean)
| Not (Expr Boolean) (a ~ Boolean)
| Val Int (a ~ Int)
to using Type.Equality
? The goal would be to approximate GADTs such as explained here https://hgiasac.github.io/posts/2018-12-18-PureScript-GADTs-Alternatives---Recap.html (which uses Leibniz).
To get something like eval :: forall a. Expr a -> a
that works. Is this even possible? I’m trying to wrap my head around this and tried a bunch of things none of which worked. This doesn’t seem to be a great idea:
data Expr a
= Add (TypeEquality a Int => Expr a) (TypeEquality a Int => Expr a)
| Eq (TypeEquality a Boolean => Expr a) (TypeEquality a Boolean => Expr a)
| Not (TypeEquality a Boolean => Expr a)
| Val (TypeEquality a Int => a)
And other similar forma all fail. Thanks