System Fomega

Main.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}

module Main where

-- Integer and Boolean literals
data Lit = LInt Int
         | LBool Bool
  deriving (Show, Eq, Ord)

-- Expressions
data Expr = Lit Lit                              -- Simple literal (integer or boolean)
          | Add { left :: Expr, right :: Expr }  -- Sum of two integers
          | Leq { left :: Expr, right :: Expr }  -- Compare two integers by less or equal
          | And { left :: Expr, right :: Expr }  -- Conjunction of two booleans
  deriving (Show, Eq, Ord)

-- Simplify an expression and compute a simple literal
simplify :: Expr -> Lit
simplify (Lit x) = x
simplify expr    = let x = simplify (left expr)
                       y = simplify (right expr)
                   in  case (x, y) of
                         (LInt i, LInt j) ->
                           case expr of
                             -- We can perform addition and comparision between integers, but not a conjunction
                             Add _ _ -> LInt $ i + j
                             Leq _ _ -> LBool $ i < j
                             _       -> error "This operation cannot be done with non-integer values!"
                         (LBool i, LBool j) ->
                           case expr of
                             -- We can perform conjunction between booleans, but not other operations
                             And _ _ -> LBool $ i && j
                             _       -> error "This operation cannot be done with non-boolean values!"
                         -- We do not have any operations on booleans and integers in the same place
                         _                  -> error "There are no operations with heterogenic parameters!"

expr1 :: Expr -- 42 + 2 < 49 && True
expr1 = And (Leq (Add (Lit (LInt 42))
                      (Lit (LInt 2)))
                 (Lit (LInt 49)))
            (Lit (LBool True))

expr2 :: Expr -- True + 5 < False
expr2 = Leq (Add (Lit (LBool True))
                 (Lit (LInt 5)))
            (Lit (LBool False))

data TLit :: * -> * where
  TLInt  :: Int  -> TLit Int
  TLBool :: Bool -> TLit Bool

deriving instance Show a => Show (TLit a)

data TExpr :: * -> * where
  TLit :: TLit a -> TExpr a
  TAdd :: TExpr Int  -> TExpr Int  -> TExpr Int
  TLeq :: TExpr Int  -> TExpr Int  -> TExpr Bool
  TAnd :: TExpr Bool -> TExpr Bool -> TExpr Bool

deriving instance Show a => Show (TExpr a)

-- Well typed simplification with no runtime errors
tsimplify :: TExpr a -> TLit a
tsimplify (TLit x)   = x
tsimplify (TAdd x y) = let TLInt x' = tsimplify x
                           TLInt y' = tsimplify y
                       in  TLInt $ x' + y'
tsimplify (TLeq x y) = let TLInt x' = tsimplify x
                           TLInt y' = tsimplify y
                       in  TLBool $ x' <= y'
tsimplify (TAnd x y) = let TLBool x' = tsimplify x
                           TLBool y' = tsimplify y
                       in  TLBool $ x' && y'

texpr1 :: TExpr Bool -- 42 + 2 < 49 && True
texpr1 = TAnd (TLeq (TAdd (TLit (TLInt 42))
                          (TLit (TLInt 2)))
                    (TLit (TLInt 49)))
              (TLit (TLBool True))

{-
-- Cannot be typed
texpr2 :: TExpr Bool -- True + 5 < False
texpr2 = TLeq (TAdd (TLit (TLBool True))
                    (TLit (TLInt 5)))
              (TLit (TLBool False))
-}

main :: IO ()
main = do
    print $ simplify expr1
    --print $ simplify expr2   -- Will throw an error
    putStrLn ""
    print $ tsimplify texpr1
    --print $ tsimplify texpr2 -- Cannot be typed