Skip to content

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information