module TCDef where

data Expr
  = Lit Integer
  | Var String
  | Expr :+: Expr
  | Lambda String Type Expr
  | Expr :@: Expr
  deriving (Eq, Show)
infixl 6 :+:
infixl 9 :@:

{-
:+: is a data constructor name that enjoys infix syntax. It means I could have
written Add Expr Expr, but it would not look nice.

:@: is similar.

The rule for infix data constructor names: they are symbols and the first
character is colon. One more example is :-> below in Type.
-}

data Type = Int | Type :-> Type
    deriving (Eq, Show)
infixr 5 :->

data Result a = OK a | Throw Error
    deriving (Eq, Show)

data Error = VarNotFound | Mismatch
    deriving (Eq, Show)

(&&>) :: Result a -> (a -> Result b) -> Result b
Throw e &&> _ = Throw e
OK t &&> k = k t

infixl 1 &&>