Alternative GADT syntax
An alternative syntax for GADTs
Instead of
data Term x where
K :: Term (a -> b -> a)
S :: Term ((a -> b -> c) -> (a -> b) -> a -> c)
Const :: a -> Term a
(:@) :: Term (a -> b) -> (Term a) -> Term b
You can write
data Term x = K :: Term (a -> b -> a)
| S :: Term ((a -> b -> c) -> (a -> b) -> a -> c)
| Const a :: Term a
| (:@) (Term (a -> b)) (Term a) :: Term b
Edited by Simon Peyton Jones