3 ms·
This feels like something you could do with GADTs in Haskell and OCaml. Here's your example rendered with GADTs: {-# LANGUAGE DataKinds, GADTs, KindSignatu
by tikhonj 11y ago
This feels like something you could do with GADTs in Haskell and OCaml. Here's your example rendered with GADTs:
{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
data IsAdd = IsAdd | NotAdd
data Expr :: IsAdd -> * where
Add :: [Expr 'NotAdd] -> Expr 'IsAdd
Const :: Integer -> Expr 'NotAdd
... -> Expr 'NotAdd
You could also use True and False instead of Add and IsAdd, or even type-level string literals as arbitrary symbols:
data Expr :: Symbol -> * where
Add :: [Expr "NotAdd"] -> Expr "IsAdd"
Const :: Integer -> Expr "NotAdd"