From f42ef36108725a4daf6132ffae9a747aba17fed5 Mon Sep 17 00:00:00 2001
From: Julien Moutinho <julm+symantic@autogeree.net>
Date: Sun, 16 Oct 2016 17:06:56 +0200
Subject: [PATCH] init

---
 Language/Symantic/AST/Test.hs              | 103 +++++----------------
 Language/Symantic/Expr/Bool.hs             |  49 ++++------
 Language/Symantic/Expr/Bool/Test.hs        |  44 ++++-----
 Language/Symantic/Expr/Common.hs           |  31 ++++++-
 Language/Symantic/Expr/Eq.hs               |  41 +++-----
 Language/Symantic/Expr/Eq/HLint.hs         |   1 +
 Language/Symantic/Expr/Eq/Test.hs          |  26 +++---
 Language/Symantic/Expr/If.hs               |  26 +-----
 Language/Symantic/Expr/If/Test.hs          |  17 ++--
 Language/Symantic/Expr/Int.hs              |  67 +++++++-------
 Language/Symantic/Expr/Int/Test.hs         |  37 ++++----
 Language/Symantic/Expr/Lambda/Test.hs      |  18 ++--
 Language/Symantic/Expr/List.hs             |  15 ++-
 Language/Symantic/Expr/List/HLint.hs       |   1 +
 Language/Symantic/Expr/List/Test.hs        | 101 ++++++++++++++++++++
 Language/Symantic/Expr/Map.hs              |   2 -
 Language/Symantic/Expr/Maybe.hs            |  25 +----
 Language/Symantic/Expr/Maybe/HLint.hs      |   1 +
 Language/Symantic/Expr/Maybe/Test.hs       |  14 +--
 Language/Symantic/Expr/Ord.hs              |  25 +----
 Language/Symantic/Expr/Test.hs             |   2 +
 Language/Symantic/Repr/Host.hs             |  30 +++---
 Language/Symantic/Repr/Host/Test.hs        |  24 ++++-
 Language/Symantic/Repr/Text.hs             |  48 +++++++---
 Language/Symantic/Repr/Text/Test.hs        |  48 +++++-----
 Language/Symantic/Trans/Bool/Const.hs      |  30 +++---
 Language/Symantic/Trans/Bool/Const/Test.hs |   6 +-
 Language/Symantic/Trans/Common.hs          |  14 +--
 Language/Symantic/Type/Bool.hs             |  10 +-
 Language/Symantic/Type/Common.hs           |   3 +
 Language/Symantic/Type/Int.hs              |  19 +---
 Language/Symantic/Type/List.hs             |   3 +-
 Language/Symantic/Type/Map.hs              |  11 ---
 Language/Symantic/Type/Maybe.hs            |  12 +--
 Language/Symantic/Type/Test.hs             |   5 +
 Language/Symantic/Type/Unit.hs             |   3 -
 Language/Symantic/Type/Var.hs              |   4 -
 symantic.cabal                             |   3 +-
 38 files changed, 449 insertions(+), 470 deletions(-)
 create mode 120000 Language/Symantic/Expr/Eq/HLint.hs
 create mode 120000 Language/Symantic/Expr/List/HLint.hs
 create mode 100644 Language/Symantic/Expr/List/Test.hs
 create mode 120000 Language/Symantic/Expr/Maybe/HLint.hs

diff --git a/Language/Symantic/AST/Test.hs b/Language/Symantic/AST/Test.hs
index beac0bd..43021c0 100644
--- a/Language/Symantic/AST/Test.hs
+++ b/Language/Symantic/AST/Test.hs
@@ -17,10 +17,9 @@ import qualified Data.List as List
 import Data.Proxy (Proxy(..))
 import Data.Text (Text)
 import qualified Data.Text as Text
-import Prelude hiding (and, not, or)
 
 import Language.Symantic.Type
-import Language.Symantic.Expr
+import Language.Symantic.Expr as Expr
 
 tests :: TestTree
 tests = testGroup "AST" $
@@ -250,30 +249,24 @@ instance -- Expr_from AST Expr_Bool
  ( Type_from AST (Type_Root_of_Expr root)
  , Expr_from AST root
  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
- , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                               (                   Type_Root_of_Expr root)
-                               AST)
-                   (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
  , Type_Unlift Type_Bool (Type_of_Expr root)
  , Root_of_Expr root ~ root
  , Implicit_HBool (Is_Last_Expr (Expr_Bool root) root)
  ) => Expr_from AST (Expr_Bool root) where
 	expr_from ex ast =
 		case ast of
-		 AST "bool" asts -> lit_from_AST bool type_bool asts ex ast
-		 AST "not"  asts -> op1_from_AST not  type_bool asts ex ast
-		 AST "and"  asts -> op2_from_AST and  type_bool asts ex ast
-		 AST "or"   asts -> op2_from_AST or   type_bool asts ex ast
-		 AST "xor"  asts -> op2_from_AST xor  type_bool asts ex ast
+		 AST "bool" asts -> lit_from_AST bool      type_bool asts ex ast
+		 AST "not"  asts -> op1_from_AST Expr.not  type_bool asts ex ast
+		 AST "&&"   asts -> op2_from_AST (Expr.&&) type_bool asts ex ast
+		 AST "||"   asts -> op2_from_AST (Expr.||) type_bool asts ex ast
+		 AST "xor"  asts -> op2_from_AST Expr.xor  type_bool asts ex ast
 		 _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
 instance -- Expr_from AST Expr_If
  ( Type_from AST (Type_Root_of_Expr root)
  , Expr_from AST root
  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
- , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                               (                   Type_Root_of_Expr root)
-                               AST)
-                   (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
  , Root_of_Expr root ~ root
  , Implicit_HBool (Is_Last_Expr (Expr_If root) root)
  ) => Expr_from AST (Expr_If root) where
@@ -286,10 +279,7 @@ instance -- Expr_from AST Expr_When
  , Expr_from AST root
  , Type_Root_Lift Type_Bool (Type_Root_of_Expr root)
  , Type_Root_Lift Type_Unit (Type_Root_of_Expr root)
- , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                               (                   Type_Root_of_Expr root)
-                               AST)
-                   (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
  , Root_of_Expr root ~ root
  , Implicit_HBool (Is_Last_Expr (Expr_When root) root)
  ) => Expr_from AST (Expr_When root) where
@@ -301,35 +291,27 @@ instance -- Expr_from AST Expr_Int
  ( Type_from AST (Type_Root_of_Expr root)
  , Expr_from AST root
  , Type_Root_Lift Type_Int (Type_Root_of_Expr root)
- , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                               (                   Type_Root_of_Expr root)
-                               AST)
-                   (Error_of_Expr AST root)
- 
+ , Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
  , Type_Unlift Type_Int (Type_of_Expr root)
  , Root_of_Expr root ~ root
  , Implicit_HBool (Is_Last_Expr (Expr_Int root) root)
  ) => Expr_from AST (Expr_Int root) where
 	expr_from ex ast =
 		case ast of
-		 AST "int" asts -> lit_from_AST int type_int asts ex ast
-		 AST "neg" asts -> op1_from_AST neg type_int asts ex ast
-		 AST "add" asts -> op2_from_AST add type_int asts ex ast
+		 AST "int"    asts -> lit_from_AST int         type_int asts ex ast
+		 AST "abs"    asts -> op1_from_AST Expr.abs    type_int asts ex ast
+		 AST "negate" asts -> op1_from_AST Expr.negate type_int asts ex ast
+		 AST "+"      asts -> op2_from_AST (Expr.+)    type_int asts ex ast
+		 AST "-"      asts -> op2_from_AST (Expr.-)    type_int asts ex ast
+		 AST "*"      asts -> op2_from_AST (Expr.*)    type_int asts ex ast
+		 AST "mod"    asts -> op2_from_AST Expr.mod    type_int asts ex ast
 		 _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
 instance -- Expr_from AST Expr_Lambda
  ( Type_from AST (Type_Root_of_Expr root)
  , Expr_from AST root
  , Type_Root_Lift (Type_Fun lam) (Type_Root_of_Expr root)
- , Error_Expr_Lift (Error_Expr_Lambda AST)
-                   (Error_of_Expr AST root)
- , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                               (                   Type_Root_of_Expr root)
-                               AST)
-                   (Error_of_Expr AST root)
- , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                                 (                   Type_Root_of_Expr root)
-                                 AST)
-                   (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr_Lambda AST)       (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
  , Root_of_Expr root ~ root
  , Implicit_HBool (Is_Last_Expr (Expr_Lambda lam root) root)
@@ -373,14 +355,7 @@ instance -- Expr_from AST Expr_Maybe
  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
  , Type_Lift   Type_Maybe     (Type_of_Expr root)
  , Type_Unlift Type_Maybe     (Type_of_Expr root)
- , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                               (                   Type_Root_of_Expr root)
-                               AST)
-                   (Error_of_Expr AST root)
- , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                                 (                   Type_Root_of_Expr root)
-                                 AST)
-                   (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
  , Root_of_Expr root ~ root
  , Implicit_HBool (Is_Last_Expr (Expr_Maybe lam root) root)
  ) => Expr_from AST (Expr_Maybe lam root) where
@@ -395,34 +370,20 @@ instance -- Expr_from AST Expr_Eq
  , Type_Lift Type_Bool (Type_of_Expr root)
  , Type_Constraint Eq (Type_Root_of_Expr root)
  , Expr_from AST root
- , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                               (                   Type_Root_of_Expr root)
-                               AST)
-                   (Error_of_Expr AST root)
- , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                                 (                   Type_Root_of_Expr root)
-                                 AST)
-                   (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
  , Root_of_Expr root ~ root
  , Implicit_HBool (Is_Last_Expr (Expr_Eq root) root)
  ) => Expr_from AST (Expr_Eq root) where
 	expr_from ex ast ctx k =
 		case ast of
-		 AST "eq" asts -> from_ast2 asts eq_from ex ast ctx k
+		 AST "==" asts -> from_ast2 asts eq_from ex ast ctx k
 		 _ -> Left $ error_expr_unsupported ex ast
 instance -- Expr_from AST Expr_Ord
  ( Type_from AST (Type_Root_of_Expr root)
  , Type_Lift Type_Ordering (Type_of_Expr root)
  , Type_Constraint Ord (Type_Root_of_Expr root)
  , Expr_from AST root
- , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                               (                   Type_Root_of_Expr root)
-                               AST)
-                   (Error_of_Expr AST root)
- , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                                 (                   Type_Root_of_Expr root)
-                                 AST)
-                   (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
  , Root_of_Expr root ~ root
  , Implicit_HBool (Is_Last_Expr (Expr_Ord root) root)
  ) => Expr_from AST (Expr_Ord root) where
@@ -438,14 +399,7 @@ instance -- Expr_from AST Expr_List
  , Type_Lift   Type_List      (Type_of_Expr root)
  , Type_Unlift Type_List      (Type_of_Expr root)
  , Type_Lift   Type_Bool      (Type_of_Expr root)
- , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                               (                   Type_Root_of_Expr root)
-                               AST)
-                   (Error_of_Expr AST root)
- , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                                 (                   Type_Root_of_Expr root)
-                                 AST)
-                   (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
  , Root_of_Expr root ~ root
  , Implicit_HBool (Is_Last_Expr (Expr_List lam root) root)
  ) => Expr_from AST (Expr_List lam root) where
@@ -467,14 +421,7 @@ instance -- Expr_from AST Expr_Map
  , Type_Lift   Type_Tuple2   (Type_of_Expr root)
  , Type_Unlift Type_Tuple2   (Type_of_Expr root)
  , Type_Constraint Ord (Type_Root_of_Expr root)
- , Error_Expr_Lift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                               (                   Type_Root_of_Expr root)
-                               AST)
-                   (Error_of_Expr AST root)
- , Error_Expr_Unlift (Error_Expr (Error_of_Type AST (Type_Root_of_Expr root))
-                                 (                   Type_Root_of_Expr root)
-                                 AST)
-                   (Error_of_Expr AST root)
+ , Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
  , Root_of_Expr root ~ root
  , Implicit_HBool (Is_Last_Expr (Expr_Map lam root) root)
  ) => Expr_from AST (Expr_Map lam root) where
diff --git a/Language/Symantic/Expr/Bool.hs b/Language/Symantic/Expr/Bool.hs
index be293fa..bcdc84a 100644
--- a/Language/Symantic/Expr/Bool.hs
+++ b/Language/Symantic/Expr/Bool.hs
@@ -2,15 +2,14 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 -- | Expression for 'Bool'.
 module Language.Symantic.Expr.Bool where
 
-import Data.Proxy (Proxy(..))
-import Prelude hiding (and, not, or)
+import Prelude hiding ((&&), not, (||))
 
 import Language.Symantic.Type
 import Language.Symantic.Expr.Common
-import Language.Symantic.Expr.Lambda
 import Language.Symantic.Repr.Dup
 import Language.Symantic.Trans.Common
 
@@ -19,29 +18,32 @@ import Language.Symantic.Trans.Common
 class Sym_Bool repr where
 	bool ::      Bool -> repr Bool
 	not  :: repr Bool -> repr Bool
-	and  :: repr Bool -> repr Bool -> repr Bool
-	or   :: repr Bool -> repr Bool -> repr Bool
+	(&&) :: repr Bool -> repr Bool -> repr Bool
+	(||) :: repr Bool -> repr Bool -> repr Bool
 	xor  :: repr Bool -> repr Bool -> repr Bool
-	xor x y = (x `or` y) `and` not (x `and` y)
+	xor x y = (x || y) && not (x && y)
 	
 	default bool :: Trans t repr =>        Bool -> t repr Bool
 	default not  :: Trans t repr => t repr Bool -> t repr Bool
-	default and  :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
-	default or   :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
+	default (&&) :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
+	default (||) :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool
 	bool = trans_lift . bool
 	not  = trans_map1 not
-	and  = trans_map2 and
-	or   = trans_map2 or
+	(&&) = trans_map2 (&&)
+	(||) = trans_map2 (||)
+infixr 2 ||
+infixr 2 `xor`
+infixr 3 &&
 
 instance -- Sym_Bool Dup
  ( Sym_Bool r1
  , Sym_Bool r2
  ) => Sym_Bool (Dup r1 r2) where
 	bool x = bool x `Dup` bool x
-	not (x1 `Dup` x2)               = not x1    `Dup` not x2
-	and (x1 `Dup` x2) (y1 `Dup` y2) = and x1 y1 `Dup` and x2 y2
-	or  (x1 `Dup` x2) (y1 `Dup` y2) = or  x1 y1 `Dup` or  x2 y2
-	xor (x1 `Dup` x2) (y1 `Dup` y2) = xor x1 y1 `Dup` xor x2 y2
+	not  (x1 `Dup` x2)               = not  x1    `Dup` not  x2
+	(&&) (x1 `Dup` x2) (y1 `Dup` y2) = (&&) x1 y1 `Dup` (&&) x2 y2
+	(||) (x1 `Dup` x2) (y1 `Dup` y2) = (||) x1 y1 `Dup` (||) x2 y2
+	xor  (x1 `Dup` x2) (y1 `Dup` y2) = xor  x1 y1 `Dup` xor  x2 y2
 
 -- * Type 'Expr_Bool'
 -- | Expression.
@@ -50,22 +52,3 @@ type instance Root_of_Expr      (Expr_Bool root)      = root
 type instance Type_of_Expr      (Expr_Bool root)      = Type_Bool
 type instance Sym_of_Expr       (Expr_Bool root) repr = Sym_Bool repr
 type instance Error_of_Expr ast (Expr_Bool root)      = No_Error_Expr
-
--- ** Type 'Expr_Lambda_Bool'
--- | Convenient alias.
-type Expr_Lambda_Bool lam = Expr_Root (Expr_Alt (Expr_Lambda lam) Expr_Bool)
-
--- | Convenient alias around 'expr_from'.
-expr_lambda_bool_from
- :: forall lam ast.
- Expr_from ast (Expr_Lambda_Bool lam)
- => Proxy lam
- -> ast
- -> Either (Error_of_Expr ast (Expr_Lambda_Bool lam))
-           (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool lam))
-                                 (Forall_Repr (Expr_Lambda_Bool lam)))
-expr_lambda_bool_from _lam ast =
-	expr_from (Proxy::Proxy (Expr_Lambda_Bool lam)) ast
-	 Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
-		Right $ Exists_Type_and_Repr ty $
-			Forall_Repr $ repr Context_Empty
diff --git a/Language/Symantic/Expr/Bool/Test.hs b/Language/Symantic/Expr/Bool/Test.hs
index d055d20..cbe74ba 100644
--- a/Language/Symantic/Expr/Bool/Test.hs
+++ b/Language/Symantic/Expr/Bool/Test.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
 module Expr.Bool.Test where
 
@@ -15,7 +16,7 @@ import Control.Arrow (left)
 import Data.Proxy (Proxy(..))
 import Data.Text (Text)
 import Data.Type.Equality ((:~:)(Refl))
-import Prelude hiding (and, not, or)
+import Prelude hiding ((&&), not, (||))
 
 import Language.Symantic.Repr
 import Language.Symantic.Expr
@@ -44,41 +45,31 @@ instance -- Trans_Boo_Const
 	z = trans_lift z
 
 -- * Expressions
-e1 = bool True `and` bool False
-e2 = (bool True `and` bool False) `or`  (bool True `and` bool True)
-e3 = (bool True `or`  bool False) `and` (bool True `or`  bool True)
-e4 = bool True `and` not (bool False)
-e5 = bool True `and` not x
+e1 = bool True && bool False
+e2 = (bool True && bool False) ||  (bool True && bool True)
+e3 = (bool True ||  bool False) && (bool True ||  bool True)
+e4 = bool True && not (bool False)
+e5 = bool True && not x
 e6 = x `xor` y
 e7 = (x `xor` y) `xor` z
 e8 = x `xor` (y `xor` bool True)
 
 -- * Tests
-{-
-(==>)
- :: forall h ast root.
- ( Eq h, Eq ast, Show h, Show ast
- , root ~ Expr_Lambda_Bool IO
- , Expr_from ast (Expr_Lambda IO root)
- , Expr_from ast (Expr_Bool      root)
- ) => ast
- -- -> (Type_Fun_Bool IO h, h, String)
- -> Either (Proxy h, Error_of_Expr ast root)
-           (Type_Fun_Bool IO h, h, String)
- -> TestTree
--}
+type Ex lam = Expr_Root (Expr_Lambda lam .|. Expr_Bool)
+ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)
+
 (==>) ast expected =
 	testCase (show ast) $
-	case expr_lambda_bool_from (Proxy::Proxy IO) ast of
+	case ex_from ast of
 	 Left err -> Left err @?= snd `left` expected
 	 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
 		case expected of
 		 Left (_, err) -> Right ("…"::String) @?= Left err
-		 Right (ty_expected::Type_Root_of_Expr (Expr_Lambda_Bool IO) h, _::h, _::Text) ->
+		 Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
 			(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
 			case ty `type_eq` ty_expected of
 			 Nothing -> return $ Left $
-				error_expr (Proxy::Proxy (Expr_Lambda_Bool IO)) $
+				error_expr (Proxy::Proxy (Ex IO)) $
 				Error_Expr_Type_mismatch ast
 				 (Exists_Type ty)
 				 (Exists_Type ty_expected)
@@ -107,7 +98,7 @@ tests = testGroup "Bool" $
 	 ] ==> Right
 	 ( type_bool
 	 , False
-	 , "(True | True) & !(True & True)" )
+	 , "xor True True" )
  , AST "app"
 	 [ AST "val"
 		 [ AST "x" []
@@ -126,7 +117,8 @@ tests = testGroup "Bool" $
 	Error_Expr_Alt_Curr $
 	Error_Expr_Type_mismatch ast
 	 (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
-	 ::Type_Fun_Bool IO (IO Zero -> IO (Succ Zero))))
+	 ::Type_Root (Type_Var :|: Type_Fun IO :|: Type_Bool)
+	             (IO Zero -> IO (Succ Zero))))
 	 (Exists_Type type_bool))
  , AST "app"
 	 [ AST "val"
@@ -141,7 +133,7 @@ tests = testGroup "Bool" $
 	 ] ==> Right
 	 ( type_bool
 	 , False
-	 , "(\\x0 -> (x0 | True) & !(x0 & True)) True" )
+	 , "(\\x0 -> xor x0 True) True" )
  , AST "let_val"
 	 [ AST "x" []
 	 , AST "bool" [AST "True" []]
@@ -152,5 +144,5 @@ tests = testGroup "Bool" $
 	 ] ==> Right
 	 ( type_bool
 	 , False
-	 , "let x0 = True in (x0 | True) & !(x0 & True)" )
+	 , "let x0 = True in xor x0 True" )
  ]
diff --git a/Language/Symantic/Expr/Common.hs b/Language/Symantic/Expr/Common.hs
index 58efd20..57707d6 100644
--- a/Language/Symantic/Expr/Common.hs
+++ b/Language/Symantic/Expr/Common.hs
@@ -29,6 +29,21 @@ import Language.Symantic.Type
 class Expr_from ast (ex:: *) where
 	expr_from :: Expr_From ast ex hs ret
 
+-- | Like 'expr_from' but for a root expression.
+root_expr_from
+ :: forall lam ast root.
+ ( Expr_from ast root
+ , Root_of_Expr root ~ root )
+ => Proxy root -> Proxy lam -> ast
+ -> Either (Error_of_Expr ast root)
+           (Exists_Type_and_Repr (Type_Root_of_Expr root)
+                                 (Forall_Repr root))
+root_expr_from _ex _lam ast =
+	expr_from (Proxy::Proxy root) ast
+	 Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
+		Right $ Exists_Type_and_Repr ty $
+			Forall_Repr $ repr Context_Empty
+
 -- ** Type 'Expr_From'
 type Expr_From ast ex hs ret
  = Proxy ex
@@ -154,7 +169,8 @@ data Forall_Repr_with_Context ex hs h
 data Forall_Repr ex h
  =   Forall_Repr
  { unForall_Repr :: forall repr
-                 .  Sym_of_Expr ex repr
+                 .  ( Sym_of_Expr ex repr
+                    , Sym_of_Expr (Root_of_Expr ex) repr )
                  => repr h }
 
 -- ** Type family 'Root_of_Expr'
@@ -179,7 +195,7 @@ type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *
 -- NOTE: include 'Type_Var' only to use it
 -- within 'Error_Expr_Type_mismatch' so far.
 type Type_Root_of_Expr (ex:: *)
- =   Type_Root (Type_Alt Type_Var (Type_of_Expr (Root_of_Expr ex)))
+ =   Type_Root (Type_Var :|: Type_of_Expr (Root_of_Expr ex))
 
 -- * Type 'Expr_Root'
 -- | The root expression, passing itself as parameter to the given expression.
@@ -220,6 +236,11 @@ instance
 data Expr_Alt curr next (root:: *)
  =   Expr_Alt_Curr (curr root)
  |   Expr_Alt_Next (next root)
+-- | Convenient alias. Requires @TypeOperators@.
+--
+-- TODO: see if using a type-level list is better.
+type (.|.) = Expr_Alt
+infixr 5 .|.
 type instance Root_of_Expr (Expr_Alt curr next root) = root
 type instance Sym_of_Expr (Expr_Alt curr next root) repr
  = ( Sym_of_Expr (curr root) repr
@@ -456,6 +477,12 @@ data Error_Expr err_ty ty ast
  -- the current expression parser component.
  deriving (Eq, Show)
 
+-- | Convenient type alias.
+type Error_Expr_of_Root ast root
+ =   Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
+                (Type_Root_of_Expr root)
+                ast
+
 -- | Convenient wrapper around 'error_expr_lift',
 -- passing the type family boilerplate.
 error_expr
diff --git a/Language/Symantic/Expr/Eq.hs b/Language/Symantic/Expr/Eq.hs
index 18f0675..60e7936 100644
--- a/Language/Symantic/Expr/Eq.hs
+++ b/Language/Symantic/Expr/Eq.hs
@@ -1,30 +1,33 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
 -- | Expression for 'Eq'.
 module Language.Symantic.Expr.Eq where
 
 import Data.Proxy (Proxy(..))
 import Data.Type.Equality ((:~:)(Refl))
+import Prelude hiding ((==))
 
 import Language.Symantic.Repr.Dup
 import Language.Symantic.Trans.Common
 import Language.Symantic.Type
 import Language.Symantic.Expr.Common
-import Language.Symantic.Expr.Lambda
-import Language.Symantic.Expr.Bool
 
 -- * Class 'Sym_Eq'
 -- | Symantic.
 class Sym_Eq repr where
-	eq :: Eq a => repr a -> repr a -> repr Bool
-	default eq :: (Trans t repr, Eq a)
-	           => t repr a -> t repr a -> t repr Bool
-	eq = trans_map2 eq
+	(==) :: Eq a => repr a -> repr a -> repr Bool
+	default (==) :: (Trans t repr, Eq a)
+	             => t repr a -> t repr a -> t repr Bool
+	(==) = trans_map2 (==)
+infix 4 ==
 
 instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (Dup r1 r2) where
-	eq (x1 `Dup` x2) (y1 `Dup` y2) = eq x1 y1 `Dup` eq x2 y2
+	(==) (x1 `Dup` x2) (y1 `Dup` y2) = (==) x1 y1 `Dup` (==) x2 y2
 
 -- * Type 'Expr_Eq'
 -- | Expression.
@@ -54,26 +57,4 @@ eq_from ast_x ast_y ex ast ctx k =
 	check_type_eq ex ast ty_x ty_y $ \Refl ->
 	check_type_constraint ex (Proxy::Proxy Eq) ast ty_x $ \Dict ->
 		k type_bool $ Forall_Repr_with_Context $
-		 \c -> x c `eq` y c
-
--- ** Type 'Expr_Lambda_Bool_Eq'
--- | Convenient alias.
-type Expr_Lambda_Bool_Eq lam
- = Expr_Root (Expr_Alt (Expr_Lambda lam)
-             (Expr_Alt Expr_Bool
-                       Expr_Eq))
-
--- | Convenient alias around 'expr_from'.
-expr_lambda_bool_eq_from
- :: forall lam ast.
- Expr_from ast (Expr_Lambda_Bool_Eq lam)
- => Proxy lam
- -> ast
- -> Either (Error_of_Expr ast (Expr_Lambda_Bool_Eq lam))
-           (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool_Eq lam))
-                                 (Forall_Repr (Expr_Lambda_Bool_Eq lam)))
-expr_lambda_bool_eq_from _lam ast =
-	expr_from (Proxy::Proxy (Expr_Lambda_Bool_Eq lam)) ast
-	 Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
-		Right $ Exists_Type_and_Repr ty $
-			Forall_Repr $ repr Context_Empty
+		 \c -> x c == y c
diff --git a/Language/Symantic/Expr/Eq/HLint.hs b/Language/Symantic/Expr/Eq/HLint.hs
new file mode 120000
index 0000000..ab18269
--- /dev/null
+++ b/Language/Symantic/Expr/Eq/HLint.hs
@@ -0,0 +1 @@
+../HLint.hs
\ No newline at end of file
diff --git a/Language/Symantic/Expr/Eq/Test.hs b/Language/Symantic/Expr/Eq/Test.hs
index f07758f..d2f9a78 100644
--- a/Language/Symantic/Expr/Eq/Test.hs
+++ b/Language/Symantic/Expr/Eq/Test.hs
@@ -1,7 +1,8 @@
-{-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
 
 module Expr.Eq.Test where
@@ -13,7 +14,7 @@ import Control.Arrow (left)
 import Data.Proxy (Proxy(..))
 import Data.Text (Text)
 import Data.Type.Equality ((:~:)(Refl))
-import Prelude hiding (and, not, or)
+import Prelude hiding ((&&), not, (||), (==))
 
 import Language.Symantic.Type
 import Language.Symantic.Expr
@@ -24,23 +25,26 @@ import AST.Test
 -- * Expressions
 t = bool True
 f = bool False
-e1 = if_ ((t `and` t) `eq` (t `or` f)) t f
-e2 = if_ (((t `and` t) `or` f) `eq` (t `and` (t `or` f))) t f
-e3 = if_ (not (t `eq` f) `eq` (t `eq` t)) t f
+e1 = if_ ((t && t) == (t || f)) t f
+e2 = if_ (((t && t) || f) == (t && (t || f))) t f
+e3 = if_ (not (t == f) == (t == t)) t f
 
 -- * Tests
+type Ex lam = Expr_Root (Expr_Lambda lam .|. Expr_Bool .|. Expr_Eq)
+ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)
+
 (==>) ast expected =
 	testCase (show ast) $
-	case expr_lambda_bool_eq_from (Proxy::Proxy IO) ast of
+	case ex_from ast of
 	 Left err -> Left err @?= snd `left` expected
 	 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
 		case expected of
 		 Left (_, err) -> Right ("…"::String) @?= Left err
-		 Right (ty_expected::Type_Root_of_Expr (Expr_Lambda_Bool_Eq IO) h, _::h, _::Text) ->
+		 Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
 			(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
 			case ty `type_eq` ty_expected of
 			 Nothing -> return $ Left $
-				error_expr (Proxy::Proxy (Expr_Lambda_Bool_Eq IO)) $
+				error_expr (Proxy::Proxy (Ex IO)) $
 				Error_Expr_Type_mismatch ast
 				 (Exists_Type ty)
 				 (Exists_Type ty_expected)
@@ -56,7 +60,7 @@ e3 = if_ (not (t `eq` f) `eq` (t `eq` t)) t f
 
 tests :: TestTree
 tests = testGroup "Eq"
- [ AST "eq" [ AST "bool" [AST "True" []]
+ [ AST "==" [ AST "bool" [AST "True" []]
 	          , AST "bool" [AST "True" []]
 	          ] ==> Right
 	 ( type_bool
@@ -66,7 +70,7 @@ tests = testGroup "Eq"
 	 [ AST "val"
 		 [ AST "x" []
 		 , AST "Bool" []
-		 , AST "eq" [ AST "var" [AST "x" []]
+		 , AST "==" [ AST "var" [AST "x" []]
 		            , AST "not" [AST "var" [AST "x" []]] ]
 		 ]
 	 , AST "bool" [AST "True" []]
diff --git a/Language/Symantic/Expr/If.hs b/Language/Symantic/Expr/If.hs
index b985748..72edeb3 100644
--- a/Language/Symantic/Expr/If.hs
+++ b/Language/Symantic/Expr/If.hs
@@ -2,14 +2,13 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 -- | Expression for @if@.
 module Language.Symantic.Expr.If where
 
 import Data.Proxy (Proxy(..))
 import Data.Type.Equality ((:~:)(Refl))
-import Language.Symantic.Expr.Bool
 import Language.Symantic.Expr.Common
-import Language.Symantic.Expr.Lambda
 import Language.Symantic.Repr.Dup
 import Language.Symantic.Trans.Common
 import Language.Symantic.Type
@@ -101,26 +100,3 @@ when_from ast_cond ast_ok ex ast ctx k =
 	check_type_eq ex ast type_unit ty_ok $ \Refl ->
 		k ty_ok $ Forall_Repr_with_Context $
 		 \c -> when (cond c) (ok c)
-
--- ** Type 'Expr_Lambda_Bool_If'
--- | Convenient alias.
-type Expr_Lambda_If_Bool lam
- =   Expr_Root (Expr_Alt (Expr_Lambda lam)
-                         (Expr_Alt Expr_If
-                                   Expr_Bool))
-
--- | Convenient alias around 'expr_from'.
-expr_lambda_if_bool_from
- :: forall lam ast root.
- ( Expr_from ast (Expr_Lambda_If_Bool lam)
- , root ~ Expr_Lambda_If_Bool lam
- ) => Proxy lam
- -> ast
- -> Either (Error_of_Expr ast root)
-           (Exists_Type_and_Repr (Type_Root_of_Expr root)
-                                 (Forall_Repr root))
-expr_lambda_if_bool_from _lam ast =
-	expr_from (Proxy::Proxy root) ast
-	 Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
-		Right $ Exists_Type_and_Repr ty $
-			Forall_Repr $ repr Context_Empty
diff --git a/Language/Symantic/Expr/If/Test.hs b/Language/Symantic/Expr/If/Test.hs
index 36fdccb..5622107 100644
--- a/Language/Symantic/Expr/If/Test.hs
+++ b/Language/Symantic/Expr/If/Test.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
 module Expr.If.Test where
 
@@ -13,7 +14,7 @@ import Control.Arrow (left)
 import Data.Proxy (Proxy(..))
 import Data.Text (Text)
 import Data.Type.Equality ((:~:)(Refl))
-import Prelude hiding (maybe, not)
+import Prelude hiding (maybe, not, (&&))
 
 import Language.Symantic.Repr
 import Language.Symantic.Expr
@@ -22,23 +23,25 @@ import Language.Symantic.Type
 import AST.Test
 
 -- * Expressions
-e1 = if_ (bool True)
-         (bool False)
-         (bool True)
+e1 = if_ (bool True) (bool False) (bool True)
+e2 = if_ (bool True && bool True) (bool False) (bool True)
 
 -- * Tests
+type Ex lam = Expr_Root (Expr_Lambda lam .|. Expr_If .|. Expr_Bool)
+ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)
+
 (==>) ast expected =
 	testCase (show ast) $
-	case expr_lambda_if_bool_from (Proxy::Proxy IO) ast of
+	case ex_from ast of
 	 Left err -> Left err @?= snd `left` expected
 	 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
 		case expected of
 		 Left (_, err) -> Right ("…"::String) @?= Left err
-		 Right (ty_expected::Type_Root_of_Expr (Expr_Lambda_If_Bool IO) h, _::h, _::Text) ->
+		 Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
 			(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
 			case ty `type_eq` ty_expected of
 			 Nothing -> return $ Left $
-				error_expr (Proxy::Proxy (Expr_Lambda_If_Bool IO)) $
+				error_expr (Proxy::Proxy (Ex IO)) $
 				Error_Expr_Type_mismatch ast
 				 (Exists_Type ty)
 				 (Exists_Type ty_expected)
diff --git a/Language/Symantic/Expr/Int.hs b/Language/Symantic/Expr/Int.hs
index d432c26..e1f6309 100644
--- a/Language/Symantic/Expr/Int.hs
+++ b/Language/Symantic/Expr/Int.hs
@@ -2,38 +2,58 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 -- | Expression for 'Int'.
 module Language.Symantic.Expr.Int where
 
-import Data.Proxy (Proxy(..))
+import Prelude hiding ((+), (-), (*), abs, mod, negate)
 
 import Language.Symantic.Type
 import Language.Symantic.Expr.Common
-import Language.Symantic.Expr.Lambda
 import Language.Symantic.Repr.Dup
 import Language.Symantic.Trans.Common
 
 -- * Class 'Sym_Int'
 -- | Symantic.
 class Sym_Int repr where
-	int ::      Int -> repr Int
-	neg :: repr Int -> repr Int
-	add :: repr Int -> repr Int -> repr Int
+	int    ::      Int -> repr Int
+	abs    :: repr Int -> repr Int
+	negate :: repr Int -> repr Int
+	(+)    :: repr Int -> repr Int -> repr Int
+	(-)    :: repr Int -> repr Int -> repr Int
+	(*)    :: repr Int -> repr Int -> repr Int
+	mod    :: repr Int -> repr Int -> repr Int
 	
-	default int :: Trans t repr =>        Int -> t repr Int
-	default neg :: Trans t repr => t repr Int -> t repr Int
-	default add :: Trans t repr => t repr Int -> t repr Int -> t repr Int
-	int = trans_lift . int
-	neg = trans_map1 neg
-	add = trans_map2 add
+	default int    :: Trans t repr =>        Int -> t repr Int
+	default abs    :: Trans t repr => t repr Int -> t repr Int
+	default negate :: Trans t repr => t repr Int -> t repr Int
+	default (+)    :: Trans t repr => t repr Int -> t repr Int -> t repr Int
+	default (-)    :: Trans t repr => t repr Int -> t repr Int -> t repr Int
+	default (*)    :: Trans t repr => t repr Int -> t repr Int -> t repr Int
+	default mod    :: Trans t repr => t repr Int -> t repr Int -> t repr Int
+	int    = trans_lift . int
+	abs    = trans_map1 abs
+	negate = trans_map1 negate
+	(+)    = trans_map2 (+)
+	(-)    = trans_map2 (-)
+	(*)    = trans_map2 (*)
+	mod    = trans_map2 mod
+infixl 6 +
+infixl 6 -
+infixl 7 *
+infixl 7 `mod`
 
 instance -- Sym_Int Dup
  ( Sym_Int r1
  , Sym_Int r2
  ) => Sym_Int (Dup r1 r2) where
-	int x = int x `Dup` int x
-	neg (x1 `Dup` x2) = neg x1 `Dup` neg x2
-	add (x1 `Dup` x2) (y1 `Dup` y2) = add x1 y1 `Dup` add x2 y2
+	int     x                          = int x     `Dup` int x
+	abs    (x1 `Dup` x2)               = abs x1    `Dup` abs x2
+	negate (x1 `Dup` x2)               = negate x1 `Dup` negate x2
+	(+)    (x1 `Dup` x2) (y1 `Dup` y2) = (+) x1 y1 `Dup` (+) x2 y2
+	(-)    (x1 `Dup` x2) (y1 `Dup` y2) = (-) x1 y1 `Dup` (-) x2 y2
+	(*)    (x1 `Dup` x2) (y1 `Dup` y2) = (*) x1 y1 `Dup` (*) x2 y2
+	mod    (x1 `Dup` x2) (y1 `Dup` y2) = mod x1 y1 `Dup` mod x2 y2
 
 -- * Type 'Expr_Int'
 -- | Expression.
@@ -42,22 +62,3 @@ type instance Root_of_Expr      (Expr_Int root)      = root
 type instance Type_of_Expr      (Expr_Int root)      = Type_Int
 type instance Sym_of_Expr       (Expr_Int root) repr = Sym_Int repr
 type instance Error_of_Expr ast (Expr_Int root)      = No_Error_Expr
-
--- ** Type 'Expr_Lambda_Int'
--- | Convenient alias.
-type Expr_Lambda_Int lam = Expr_Root (Expr_Alt (Expr_Lambda lam) Expr_Int)
-
--- | Convenient alias around 'expr_from'.
-expr_lambda_int_from
- :: forall lam ast.
- Expr_from ast (Expr_Lambda_Int lam)
- => Proxy lam
- -> ast
- -> Either (Error_of_Expr ast (Expr_Lambda_Int lam))
-           (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Int lam))
-                                 (Forall_Repr (Expr_Lambda_Int lam)))
-expr_lambda_int_from _lam ast =
-	expr_from (Proxy::Proxy (Expr_Lambda_Int lam)) ast
-	 Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
-		Right $ Exists_Type_and_Repr ty $
-			Forall_Repr $ repr Context_Empty
diff --git a/Language/Symantic/Expr/Int/Test.hs b/Language/Symantic/Expr/Int/Test.hs
index e319dbf..b1df17f 100644
--- a/Language/Symantic/Expr/Int/Test.hs
+++ b/Language/Symantic/Expr/Int/Test.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
 module Expr.Int.Test where
 
@@ -15,7 +16,7 @@ import Control.Arrow (left)
 import Data.Proxy (Proxy(..))
 import Data.Text (Text)
 import Data.Type.Equality ((:~:)(Refl))
-import Prelude hiding (and, not, or)
+import Prelude hiding ((&&), not, (||), (+), negate)
 
 import Language.Symantic.Repr
 import Language.Symantic.Expr
@@ -37,28 +38,31 @@ instance Sym_Int_Vars (Repr_Text fun) where
 	z = Repr_Text $ \_p _v -> "z"
 
 -- * Expressions
-e1 = int 1 `add` int 0
-e2 = (int 1 `add` int 0) `add` neg (int 1 `add` int 1)
-e3 = (int 1 `add` neg (int 0)) `add` (int 1 `add` neg (int 1))
-e4 = int 0 `add` neg (int 1)
-e5 = int 1 `add` neg x
-e6 = x `add` y
-e7 = (x `add` y) `add` z
-e8 = x `add` (y `add` int 1)
+e1 = int 1 + int 0
+e2 = (int 1 + int 0) + negate (int 1 + int 1)
+e3 = (int 1 + negate (int 0)) + (int 1 + negate (int 1))
+e4 = int 0 + negate (int 1)
+e5 = int 1 + negate x
+e6 = x + y
+e7 = (x + y) + z
+e8 = x + (y + int 1)
 
 -- * Tests
+type Ex lam = Expr_Root (Expr_Lambda lam .|. Expr_Int)
+ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)
+
 (==>) ast expected =
 	testCase (show ast) $
-	case expr_lambda_int_from (Proxy::Proxy IO) ast of
+	case ex_from ast of
 	 Left err -> Left err @?= snd `left` expected
 	 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
 		case expected of
 		 Left (_, err) -> Right ("…"::String) @?= Left err
-		 Right (ty_expected::Type_Root_of_Expr (Expr_Lambda_Int IO) h, _::h, _::Text) ->
+		 Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
 			(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
 			case ty `type_eq` ty_expected of
 			 Nothing -> return $ Left $
-				error_expr (Proxy::Proxy (Expr_Lambda_Int IO)) $
+				error_expr (Proxy::Proxy (Ex IO)) $
 				Error_Expr_Type_mismatch ast
 				 (Exists_Type ty)
 				 (Exists_Type ty_expected)
@@ -81,7 +85,7 @@ tests = testGroup "Int" $
  , AST "bool" [AST "True" []] ==> Left (Proxy::Proxy Bool,
 	Error_Expr_Alt_Curr $
 	Error_Expr_Unsupported $ AST "bool" [AST "True" []])
- , AST "add"
+ , AST "+"
 	 [ AST "int" [AST "1" []]
 	 , AST "int" [AST "1" []]
 	 ] ==> Right
@@ -95,7 +99,8 @@ tests = testGroup "Int" $
 	Error_Expr_Alt_Curr $
 	Error_Expr_Type_mismatch ast
 	 (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
-	 ::Type_Fun_Int IO (IO Zero -> IO (Succ Zero))))
+	 ::Type_Root (Type_Var :|: Type_Fun IO :|: Type_Int)
+	             (IO Zero -> IO (Succ Zero))))
 	 (Exists_Type type_int))
  , AST "app"
 	 [ AST "val"
@@ -112,7 +117,7 @@ tests = testGroup "Int" $
 	 [ AST "val"
 		 [ AST "x" []
 		 , AST "Int" []
-		 , AST "add"
+		 , AST "+"
 			 [ AST "var" [AST "x" []]
 			 , AST "int" [AST "1" []]
 			 ]
@@ -125,7 +130,7 @@ tests = testGroup "Int" $
  , AST "let_val"
 	 [ AST "x" []
 	 , AST "int" [AST "1" []]
-	 , AST "add"
+	 , AST "+"
 		 [ AST "var" [AST "x" []]
 		 , AST "int" [AST "1" []]
 		 ]
diff --git a/Language/Symantic/Expr/Lambda/Test.hs b/Language/Symantic/Expr/Lambda/Test.hs
index 26e1e8d..f23226d 100644
--- a/Language/Symantic/Expr/Lambda/Test.hs
+++ b/Language/Symantic/Expr/Lambda/Test.hs
@@ -6,20 +6,20 @@ module Expr.Lambda.Test where
 
 import Test.Tasty
 
-import Prelude hiding (and, not, or)
+import Prelude hiding ((&&), not, (||), (==))
 
 import Language.Symantic.Expr.Lambda
 import Language.Symantic.Expr.Bool
 
 -- * Expressions
-e1 = val $ \x -> val $ \y -> (x `or` y) `and` not (x `and` y)
-e2 = val $ \x -> val $ \y -> (x `and` not y) `or` (not x `and` y)
-e3 = let_val (bool True) $ \x -> x `and` x
-e4 = let_val (val $ \x -> x `and` x) $ \f -> f `app` bool True
-e5 = val $ \x0 -> val $ \x1 -> x0 `and` x1
-e6 = let_val (bool True) id `and` bool False
-e7 = val $ \f -> (f `app` bool True) `and` bool True
-e8 = val $ \f -> f `app` (bool True `and` bool True)
+e1 = val $ \x -> val $ \y -> (x || y) && not (x && y)
+e2 = val $ \x -> val $ \y -> (x && not y) || (not x && y)
+e3 = let_val (bool True) $ \x -> x && x
+e4 = let_val (val $ \x -> x && x) $ \f -> f `app` bool True
+e5 = val $ \x0 -> val $ \x1 -> x0 && x1
+e6 = let_val (bool True) id && bool False
+e7 = val $ \f -> (f `app` bool True) && bool True
+e8 = val $ \f -> f `app` (bool True && bool True)
 
 tests :: TestTree
 tests =
diff --git a/Language/Symantic/Expr/List.hs b/Language/Symantic/Expr/List.hs
index 2409648..656bc36 100644
--- a/Language/Symantic/Expr/List.hs
+++ b/Language/Symantic/Expr/List.hs
@@ -4,13 +4,12 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 -- | Expression for 'List'.
 module Language.Symantic.Expr.List where
 
--- import qualified Data.List as List
 import Data.Proxy (Proxy(..))
 import Data.Type.Equality ((:~:)(Refl))
-import Prelude hiding (maybe)
 
 import Language.Symantic.Type
 import Language.Symantic.Repr.Dup
@@ -24,11 +23,14 @@ import Language.Symantic.Expr.Bool
 class Sym_List repr where
 	list_empty :: repr [a]
 	list_cons  :: repr a -> repr [a] -> repr [a]
+	list       :: [repr a] -> repr [a]
 	
 	default list_empty :: Trans t repr => t repr [a]
 	default list_cons  :: Trans t repr => t repr a -> t repr [a] -> t repr [a]
+	default list       :: Trans t repr => [t repr a] -> t repr [a]
 	list_empty = trans_lift list_empty
 	list_cons  = trans_map2 list_cons
+	list l     = trans_lift $ list (trans_apply <$> l)
 -- | Symantic requiring a 'Lambda'.
 class Sym_List_Lam lam repr where
 	list_filter
@@ -49,6 +51,11 @@ instance -- Sym_List Dup
  ) => Sym_List (Dup r1 r2) where
 	list_empty = list_empty `Dup` list_empty
 	list_cons (a1 `Dup` a2) (l1 `Dup` l2) = list_cons a1 l1 `Dup` list_cons a2 l2
+	list l =
+		let (l1, l2) =
+			foldr (\(x1 `Dup` x2) (xs1, xs2) ->
+				(x1:xs1, x2:xs2)) ([], []) l in
+		list l1 `Dup` list l2
 instance -- Sym_List_Lam Dup
  ( Sym_List_Lam lam r1
  , Sym_List_Lam lam r2
@@ -164,9 +171,7 @@ list_filter_from ast_f ast_l ex ast ctx k =
 -- ** Type 'Expr_Lambda_List_Bool'
 -- | Convenient alias.
 type Expr_Lambda_List_Bool lam
- =   Expr_Root (Expr_Alt (Expr_Lambda lam)
-                         (Expr_Alt (Expr_List lam)
-                                    Expr_Bool))
+ =   Expr_Root (Expr_Lambda lam .|. Expr_List lam .|. Expr_Bool)
 
 -- | Convenient alias around 'expr_from'.
 expr_lambda_list_bool_from
diff --git a/Language/Symantic/Expr/List/HLint.hs b/Language/Symantic/Expr/List/HLint.hs
new file mode 120000
index 0000000..ab18269
--- /dev/null
+++ b/Language/Symantic/Expr/List/HLint.hs
@@ -0,0 +1 @@
+../HLint.hs
\ No newline at end of file
diff --git a/Language/Symantic/Expr/List/Test.hs b/Language/Symantic/Expr/List/Test.hs
new file mode 100644
index 0000000..d7b1e31
--- /dev/null
+++ b/Language/Symantic/Expr/List/Test.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module Expr.List.Test where
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Control.Arrow (left)
+import Data.Proxy (Proxy(..))
+import Data.Text (Text)
+import Data.Type.Equality ((:~:)(Refl))
+import Prelude hiding (mod, (==))
+
+import Language.Symantic.Repr
+import Language.Symantic.Expr
+import Language.Symantic.Type
+
+import AST.Test
+
+-- * Expressions
+t = bool True
+f = bool False
+e1 = list_filter (inline $ \x -> if_ (x `mod` int 2 == int 0) t f)
+                 (list $ int <$> [1..5])
+
+{-
+-- * Tests
+(==>) ast expected =
+	testCase (show ast) $
+	case expr_lambda_maybe_bool_from (Proxy::Proxy IO) ast of
+	 Left err -> Left err @?= snd `left` expected
+	 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
+		case expected of
+		 Left (_, err) -> Right ("…"::String) @?= Left err
+		 Right (ty_expected::Type_Root_of_Expr (Expr_Lambda_List_Bool IO) h, _::h, _::Text) ->
+			(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
+			case ty `type_eq` ty_expected of
+			 Nothing -> return $ Left $
+				error_expr (Proxy::Proxy (Expr_Lambda_List_Bool IO)) $
+				Error_Expr_Type_mismatch ast
+				 (Exists_Type ty)
+				 (Exists_Type ty_expected)
+			 Just Refl -> do
+				h <- host_from_expr r
+				return $
+					Right
+					 ( ty
+					 , h
+					 , text_from_expr r
+					 -- , (text_from_expr :: Repr_String IO h -> Text) r
+					 )
+-}
+tests :: TestTree
+tests = testGroup "List"
+ [{- AST "just" [AST "bool" [AST "True" []]] ==> Right
+	 ( type_maybe type_bool
+	 , Just True
+	 , "just True" )
+ , AST "just"
+	 [ AST "let_val"
+		 [ AST "x" []
+		 , AST "bool" [AST "True" []]
+		 , AST "var" [AST "x" []]
+		 ]
+	 ] ==> Right
+	 ( type_maybe type_bool
+	 , Just True
+	 , "just (let x0 = True in x0)" )
+ , AST "maybe"
+	 [ AST "bool" [AST "True" []]
+	 , AST "val"
+		 [ AST "x" []
+		 , AST "Bool" []
+		 , AST "not" [AST "var" [AST "x" []]]
+		 ]
+	 , AST "nothing"
+		 [ AST "Bool" []
+		 ]
+	 ] ==> Right
+	 ( type_bool
+	 , True
+	 , "maybe True (\\x0 -> !x0) nothing" )
+ , AST "maybe"
+	 [ AST "bool" [AST "False" []]
+	 , AST "val"
+		 [ AST "x" []
+		 , AST "Bool" []
+		 , AST "not" [AST "var" [AST "x" []]]
+		 ]
+	 , AST "just"
+		 [ AST "bool" [AST "True" []]
+		 ]
+	 ] ==> Right
+	 ( type_bool
+	 , False
+	 , "maybe False (\\x0 -> !x0) (just True)" )
+ -}]
diff --git a/Language/Symantic/Expr/Map.hs b/Language/Symantic/Expr/Map.hs
index f488dae..d2d1e33 100644
--- a/Language/Symantic/Expr/Map.hs
+++ b/Language/Symantic/Expr/Map.hs
@@ -141,5 +141,3 @@ type instance Root_of_Expr      (Expr_Map lam root)      = root
 type instance Type_of_Expr      (Expr_Map lam root)      = Type_Map
 type instance Sym_of_Expr       (Expr_Map lam root) repr = (Sym_Map repr, Sym_Map_Lam lam repr)
 type instance Error_of_Expr ast (Expr_Map lam root)      = No_Error_Expr
-
-
diff --git a/Language/Symantic/Expr/Maybe.hs b/Language/Symantic/Expr/Maybe.hs
index 28ada56..2764b72 100644
--- a/Language/Symantic/Expr/Maybe.hs
+++ b/Language/Symantic/Expr/Maybe.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 -- | Expression for 'Maybe'.
 module Language.Symantic.Expr.Maybe where
 
@@ -16,7 +17,6 @@ import Language.Symantic.Repr.Dup
 import Language.Symantic.Trans.Common
 import Language.Symantic.Expr.Common
 import Language.Symantic.Expr.Lambda
-import Language.Symantic.Expr.Bool
 
 -- * Class 'Sym_Maybe_Lam'
 -- | Symantic.
@@ -154,26 +154,3 @@ just_from ast_a _ex _ast ctx k =
 	 \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
 		k (type_maybe ty_a) $ Forall_Repr_with_Context $
 			\c -> just (a c)
-
--- ** Type 'Expr_Lambda_Maybe_Bool'
--- | Convenient alias.
-type Expr_Lambda_Maybe_Bool lam
- =   Expr_Root (Expr_Alt (Expr_Lambda lam)
-                         (Expr_Alt (Expr_Maybe lam)
-                                    Expr_Bool))
-
--- | Convenient alias around 'expr_from'.
-expr_lambda_maybe_bool_from
- :: forall lam ast root.
- ( Expr_from ast (Expr_Lambda_Maybe_Bool lam)
- , root ~ Expr_Lambda_Maybe_Bool lam
- ) => Proxy lam
- -> ast
- -> Either (Error_of_Expr ast root)
-           (Exists_Type_and_Repr (Type_Root_of_Expr root)
-                                 (Forall_Repr root))
-expr_lambda_maybe_bool_from _lam ast =
-	expr_from (Proxy::Proxy root) ast
-	 Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
-		Right $ Exists_Type_and_Repr ty $
-			Forall_Repr $ repr Context_Empty
diff --git a/Language/Symantic/Expr/Maybe/HLint.hs b/Language/Symantic/Expr/Maybe/HLint.hs
new file mode 120000
index 0000000..ab18269
--- /dev/null
+++ b/Language/Symantic/Expr/Maybe/HLint.hs
@@ -0,0 +1 @@
+../HLint.hs
\ No newline at end of file
diff --git a/Language/Symantic/Expr/Maybe/Test.hs b/Language/Symantic/Expr/Maybe/Test.hs
index ca6c701..4fe7a8c 100644
--- a/Language/Symantic/Expr/Maybe/Test.hs
+++ b/Language/Symantic/Expr/Maybe/Test.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
 module Expr.Maybe.Test where
 
@@ -22,23 +23,24 @@ import Language.Symantic.Type
 import AST.Test
 
 -- * Expressions
-e1 = maybe (bool True)
-           (val not)
-           (just $ bool True)
+e1 = maybe (bool True) (val not) (just $ bool True)
 
 -- * Tests
+type Ex lam = Expr_Root (Expr_Lambda lam .|. Expr_Maybe lam .|. Expr_Bool)
+ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)
+
 (==>) ast expected =
 	testCase (show ast) $
-	case expr_lambda_maybe_bool_from (Proxy::Proxy IO) ast of
+	case ex_from ast of
 	 Left err -> Left err @?= snd `left` expected
 	 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
 		case expected of
 		 Left (_, err) -> Right ("…"::String) @?= Left err
-		 Right (ty_expected::Type_Root_of_Expr (Expr_Lambda_Maybe_Bool IO) h, _::h, _::Text) ->
+		 Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
 			(>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
 			case ty `type_eq` ty_expected of
 			 Nothing -> return $ Left $
-				error_expr (Proxy::Proxy (Expr_Lambda_Maybe_Bool IO)) $
+				error_expr (Proxy::Proxy (Ex IO)) $
 				Error_Expr_Type_mismatch ast
 				 (Exists_Type ty)
 				 (Exists_Type ty_expected)
diff --git a/Language/Symantic/Expr/Ord.hs b/Language/Symantic/Expr/Ord.hs
index d13708e..e774fe8 100644
--- a/Language/Symantic/Expr/Ord.hs
+++ b/Language/Symantic/Expr/Ord.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 -- | Expression for 'Ord'.
 module Language.Symantic.Expr.Ord where
 
@@ -13,8 +14,6 @@ import Language.Symantic.Repr.Dup
 import Language.Symantic.Trans.Common
 import Language.Symantic.Type
 import Language.Symantic.Expr.Common
-import Language.Symantic.Expr.Lambda
-import Language.Symantic.Expr.Bool
 import Language.Symantic.Expr.Eq
 
 -- * Class 'Sym_Ord'
@@ -59,25 +58,3 @@ compare_from ast_x ast_y ex ast ctx k =
 	check_type_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict ->
 		k type_ordering $ Forall_Repr_with_Context $
 		 \c -> x c `compare` y c
-
--- ** Type 'Expr_Lambda_Bool_Ord'
--- | Convenient alias.
-type Expr_Lambda_Bool_Ord lam
- = Expr_Root (Expr_Alt (Expr_Lambda lam)
-             (Expr_Alt Expr_Bool
-                       Expr_Ord))
-
--- | Convenient alias around 'expr_from'.
-expr_lambda_bool_ord_from
- :: forall lam ast.
- Expr_from ast (Expr_Lambda_Bool_Ord lam)
- => Proxy lam
- -> ast
- -> Either (Error_of_Expr ast (Expr_Lambda_Bool_Ord lam))
-           (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Bool_Ord lam))
-                                 (Forall_Repr (Expr_Lambda_Bool_Ord lam)))
-expr_lambda_bool_ord_from _lam ast =
-	expr_from (Proxy::Proxy (Expr_Lambda_Bool_Ord lam)) ast
-	 Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
-		Right $ Exists_Type_and_Repr ty $
-			Forall_Repr $ repr Context_Empty
diff --git a/Language/Symantic/Expr/Test.hs b/Language/Symantic/Expr/Test.hs
index b7256ec..1a41adc 100644
--- a/Language/Symantic/Expr/Test.hs
+++ b/Language/Symantic/Expr/Test.hs
@@ -8,6 +8,7 @@ import qualified Expr.Int.Test as Int
 import qualified Expr.Maybe.Test as Maybe
 import qualified Expr.If.Test as If
 import qualified Expr.Eq.Test as Eq
+import qualified Expr.List.Test as List
 
 tests :: TestTree
 tests =
@@ -18,4 +19,5 @@ tests =
 	 , Maybe.tests
 	 , If.tests
 	 , Eq.tests
+	 , List.tests
 	 ]
diff --git a/Language/Symantic/Repr/Host.hs b/Language/Symantic/Repr/Host.hs
index 49d55bc..28b5670 100644
--- a/Language/Symantic/Repr/Host.hs
+++ b/Language/Symantic/Repr/Host.hs
@@ -10,10 +10,7 @@ import Control.Monad.IO.Class (MonadIO(..))
 import Data.IORef
 import qualified Data.Bool as Bool
 import qualified Data.Maybe as Maybe
--- import qualified Data.List as List
-import qualified Data.Ord as Ord
 import qualified Data.Map.Strict as Map
-import Prelude hiding (and, not, or, compare)
 
 import Language.Symantic.Lib.Control.Monad
 import Language.Symantic.Expr
@@ -35,19 +32,23 @@ host_from_expr = unRepr_Host
 
 instance MonadIO lam => Sym_Lambda lam (Repr_Host lam) where
 	type Lambda_from_Repr (Repr_Host lam) = lam
-	app = liftM2Join $ \f a -> Repr_Host $ f $ return a
+	app      = liftM2Join $ \f a -> Repr_Host $ f $ return a
 	inline f = return $       unRepr_Host . f . Repr_Host
 	val    f = return $  (>>= unRepr_Host . f . Repr_Host  . return)
-	lazy   f = return $ ((>>= unRepr_Host . f . Repr_Host) . expr_lambda_lazy_share)
+	lazy   f = return $ ((>>= unRepr_Host . f . Repr_Host) . lazy_share)
 instance Monad lam => Sym_Bool (Repr_Host lam) where
 	bool = return
 	not  = fmap Bool.not
-	and  = liftM2 (&&)
-	or   = liftM2 (||)
+	(&&) = liftM2 (Prelude.&&)
+	(||) = liftM2 (Prelude.||)
 instance Monad lam => Sym_Int (Repr_Host lam) where
-	int = return
-	neg = fmap negate
-	add = liftM2 (+)
+	int    = return
+	abs    = fmap Prelude.abs
+	negate = fmap Prelude.negate
+	(+)    = liftM2 (Prelude.+)
+	(-)    = liftM2 (Prelude.-)
+	(*)    = liftM2 (Prelude.*)
+	mod    = liftM2 Prelude.mod
 instance Monad lam => Sym_Maybe (Repr_Host lam) where
 	nothing = return Nothing
 	just    = liftMJoin $ return . Just
@@ -64,12 +65,13 @@ instance Monad lam => Sym_When (Repr_Host lam) where
 		m' <- m
 		Monad.when m' ok
 instance Monad lam => Sym_Eq (Repr_Host lam) where
-	eq = liftM2 (==)
+	(==) = liftM2 (Prelude.==)
 instance Monad lam => Sym_Ord (Repr_Host lam) where
-	compare = liftM2 Ord.compare
+	compare = liftM2 Prelude.compare
 instance Monad lam => Sym_List (Repr_Host lam) where
 	list_empty = return []
 	list_cons  = liftM2 (:)
+	list       = sequence
 instance MonadIO lam => Sym_List_Lam lam (Repr_Host lam) where
 	list_filter f = liftMJoin go
 		where
@@ -86,8 +88,8 @@ instance MonadIO lam => Sym_Map_Lam lam (Repr_Host lam) where
 	map_map f = liftMJoin $ sequence . ((\a -> f `app` return a) <$>)
 
 -- | Helper to store arguments of 'lazy' into an 'IORef'.
-expr_lambda_lazy_share :: MonadIO m => m a -> m (m a)
-expr_lambda_lazy_share m = do
+lazy_share :: MonadIO m => m a -> m (m a)
+lazy_share m = do
 	r <- liftIO $ newIORef (False, m)
 	return $ do
 		(already_evaluated, m') <- liftIO $ readIORef r
diff --git a/Language/Symantic/Repr/Host/Test.hs b/Language/Symantic/Repr/Host/Test.hs
index 34706c4..67d70f7 100644
--- a/Language/Symantic/Repr/Host/Test.hs
+++ b/Language/Symantic/Repr/Host/Test.hs
@@ -1,8 +1,9 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
 
 module Repr.Host.Test where
 
@@ -21,11 +22,12 @@ import qualified Expr.Lambda.Test as Lambda.Test
 import qualified Expr.Bool.Test as Bool.Test
 import qualified Expr.Maybe.Test as Maybe.Test
 import qualified Expr.If.Test as If.Test
+import qualified Expr.List.Test as List.Test
 
 tests :: TestTree
 tests = testGroup "Host" $
  [ testGroup "Bool" $
-	let (==>) (expr::forall repr. Sym_of_Expr (Expr_Lambda_Bool IO) repr => repr h) expected =
+	let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root (Expr_Lambda IO .|. Expr_Bool)) repr => repr h) expected =
 		testCase (Text.unpack $ (text_from_expr :: Repr_Text IO _h -> Text) $ expr) $
 		(>>= (@?= expected)) $
 		host_from_expr expr in
@@ -35,7 +37,7 @@ tests = testGroup "Host" $
 	 , Bool.Test.e4 ==> True
 	 ]
  , testGroup "Lambda" $
-	let (==>) (expr::forall repr. Sym_of_Expr (Expr_Lambda_Bool IO) repr => repr h) expected =
+	let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root (Expr_Lambda IO .|. Expr_Bool)) repr => repr h) expected =
 		testCase (Text.unpack $ (text_from_expr :: Repr_Text IO _h -> Text) $ expr) $
 		(>>= (@?= expected)) $
 		host_from_expr expr in
@@ -62,17 +64,29 @@ tests = testGroup "Host" $
 	 , (Lambda.Test.e7 `app` val not) ==> False
 	 ]
  , testGroup "Maybe" $
-	let (==>) (expr::forall repr. Sym_of_Expr (Expr_Lambda_Maybe_Bool IO) repr => repr h) expected =
+	let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root (Expr_Lambda IO .|. Expr_Maybe IO .|. Expr_Bool)) repr => repr h) expected =
 		testCase (Text.unpack $ (text_from_expr :: Repr_Text IO _h -> Text) $ expr) $
 		(>>= (@?= expected)) $
 		host_from_expr expr in
 	 [ Maybe.Test.e1 ==> False
 	 ]
  , testGroup "If" $
-	let (==>) (expr::forall repr. Sym_of_Expr (Expr_Lambda_If_Bool IO) repr => repr h) expected =
+	let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root (Expr_Lambda IO .|. Expr_If .|. Expr_Bool)) repr => repr h) expected =
 		testCase (Text.unpack $ (text_from_expr :: Repr_Text IO _h -> Text) $ expr) $
 		(>>= (@?= expected)) $
 		host_from_expr expr in
 	 [ If.Test.e1 ==> False
 	 ]
+ , testGroup "List" $
+	let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root (  Expr_Lambda IO
+	                                                    .|. Expr_List IO
+	                                                    .|. Expr_Bool
+	                                                    .|. Expr_Int
+	                                                    .|. Expr_If
+	                                                    .|. Expr_Eq )) repr => repr h) expected =
+		testCase (Text.unpack $ (text_from_expr :: Repr_Text IO _h -> Text) $ expr) $
+		(>>= (@?= expected)) $
+		host_from_expr expr in
+	 [ List.Test.e1 ==> [2::Int,4]
+	 ]
  ]
diff --git a/Language/Symantic/Repr/Text.hs b/Language/Symantic/Repr/Text.hs
index 45abf99..172db02 100644
--- a/Language/Symantic/Repr/Text.hs
+++ b/Language/Symantic/Repr/Text.hs
@@ -78,30 +78,45 @@ instance Sym_Bool (Repr_Text lam) where
 		Repr_Text $ \p v ->
 			let p' = precedence_Not in
 			paren p p' $ "!" <> x p' v
-	and (Repr_Text x) (Repr_Text y) =
+	(&&) (Repr_Text x) (Repr_Text y) =
 		Repr_Text $ \p v ->
 			let p' = precedence_And in
-			paren p p' $ x p' v <> " & " <> y p' v
-	or (Repr_Text x) (Repr_Text y) =
+			paren p p' $ x p' v <> " && " <> y p' v
+	(||) (Repr_Text x) (Repr_Text y) =
 		Repr_Text $ \p v ->
 			let p' = precedence_Or in
-			paren p p'  $ x p' v <> " | " <> y p' v
-	{-xor (Repr_Text x) (Repr_Text y) =
+			paren p p'  $ x p' v <> " || " <> y p' v
+	xor (Repr_Text x) (Repr_Text y) =
 		Repr_Text $ \p v ->
 			let p' = precedence_Xor in
-			paren p p'  $ x p' v <> " * " <> y p' v
-	-}
+			paren p p'  $ "xor " <> x p' v <> " " <> y p' v
 instance Sym_Int (Repr_Text lam) where
 	int a = Repr_Text $ \_p _v ->
 		Text.pack (show a)
-	neg (Repr_Text x) =
+	abs (Repr_Text x) =
+		Repr_Text $ \p v ->
+			let p' = precedence_App in
+			paren p p' $ "abs " <> x p' v
+	negate (Repr_Text x) =
 		Repr_Text $ \p v ->
 			let p' = precedence_Neg in
 			paren p p' $ "-" <> x p' v
-	add (Repr_Text x) (Repr_Text y) =
+	(+) (Repr_Text x) (Repr_Text y) =
 		Repr_Text $ \p v ->
 			let p' = precedence_Add in
 			paren p p' $ x p' v <> " + " <> y p' v
+	(-) (Repr_Text x) (Repr_Text y) =
+		Repr_Text $ \p v ->
+			let p' = precedence_Sub in
+			paren p p' $ x p' v <> " - " <> y p' v
+	(*) (Repr_Text x) (Repr_Text y) =
+		Repr_Text $ \p v ->
+			let p' = precedence_Mul in
+			paren p p' $ x p' v <> " * " <> y p' v
+	mod (Repr_Text x) (Repr_Text y) =
+		Repr_Text $ \p v ->
+			let p' = precedence_Mod in
+			paren p p' $ x p' v <> " % " <> y p' v
 instance Sym_Maybe (Repr_Text lam) where
 	nothing =
 		Repr_Text $ \_p _v ->
@@ -135,7 +150,7 @@ instance Sym_When (Repr_Text lam) where
 			"when " <> cond p' v <>
 			" " <> ok p' v
 instance Sym_Eq (Repr_Text lam) where
-	eq (Repr_Text x) (Repr_Text y) =
+	(==) (Repr_Text x) (Repr_Text y) =
 		Repr_Text $ \p v ->
 			let p' = precedence_Eq in
 			paren p p' $
@@ -154,6 +169,9 @@ instance Sym_List (Repr_Text lam) where
 			let p' = precedence_App in
 			paren p p' $
 			x p' v <> ":" <> xs p' v
+	list l = Repr_Text $ \_p v ->
+		let p' = precedence_Toplevel in
+		"[" <> Text.intercalate ", " ((\(Repr_Text a) -> a p' v) <$> l) <> "]"
 instance Sym_List_Lam lam (Repr_Text lam) where
 	list_filter (Repr_Text f) (Repr_Text l) =
 		Repr_Text $ \p v ->
@@ -203,11 +221,17 @@ precedence_Eq         = Precedence 4
 precedence_Or        :: Precedence
 precedence_Or         = Precedence 5
 precedence_Xor       :: Precedence
-precedence_Xor        = Precedence 6
+precedence_Xor        = precedence_Or
 precedence_And       :: Precedence
-precedence_And        = Precedence 7
+precedence_And        = Precedence 6
 precedence_Add       :: Precedence
 precedence_Add        = precedence_And
+precedence_Sub       :: Precedence
+precedence_Sub        = precedence_Add
+precedence_Mul       :: Precedence
+precedence_Mul        = Precedence 7
+precedence_Mod       :: Precedence
+precedence_Mod        = precedence_Mul
 precedence_App       :: Precedence
 precedence_App        = Precedence 8
 precedence_Not       :: Precedence
diff --git a/Language/Symantic/Repr/Text/Test.hs b/Language/Symantic/Repr/Text/Test.hs
index 0fba191..19d96cf 100644
--- a/Language/Symantic/Repr/Text/Test.hs
+++ b/Language/Symantic/Repr/Text/Test.hs
@@ -1,4 +1,3 @@
-
 module Repr.Text.Test where
 
 import Test.Tasty
@@ -11,43 +10,44 @@ import qualified Expr.Lambda.Test as Lambda.Test
 import qualified Expr.Bool.Test as Bool.Test
 import qualified Expr.Maybe.Test as Maybe.Test
 import qualified Expr.Eq.Test as Eq.Test
+import qualified Expr.If.Test as If.Test
 
 tests :: TestTree
-tests = testGroup "String" $
+tests = testGroup "Text" $
  let (==>) expr expected =
 	testCase (Text.unpack expected) $
 	(@?= expected) $
 	text_from_expr expr in
  [ testGroup "Bool"
-	 [ Bool.Test.e1 ==> "True & False"
-	 , Bool.Test.e2 ==> "True & False | True & True"
-	 , Bool.Test.e3 ==> "(True | False) & (True | True)"
-	 , Bool.Test.e4 ==> "True & !False"
-	 , Bool.Test.e5 ==> "True & !x"
-	 , Bool.Test.e6 ==> "(x | y) & !(x & y)"
-	 , Bool.Test.e7 ==> "((x | y) & !(x & y) | z) & !(((x | y) & !(x & y)) & z)"
-	 , Bool.Test.e8 ==> "(x | (y | True) & !(y & True)) & !(x & ((y | True) & !(y & True)))"
+	 [ Bool.Test.e1 ==> "True && False"
+	 , Bool.Test.e2 ==> "True && False || True && True"
+	 , Bool.Test.e3 ==> "(True || False) && (True || True)"
+	 , Bool.Test.e4 ==> "True && !False"
+	 , Bool.Test.e5 ==> "True && !x"
+	 , Bool.Test.e6 ==> "xor x y"
+	 , Bool.Test.e7 ==> "xor (xor x y) z"
+	 , Bool.Test.e8 ==> "xor x (xor y True)"
 	 ]
  , testGroup "Lambda"
-	 [ Lambda.Test.e1 ==> "\\x0 -> (\\x1 -> (x0 | x1) & !(x0 & x1))"
-	 , Lambda.Test.e2 ==> "\\x0 -> (\\x1 -> x0 & !x1 | !x0 & x1)"
-	 , Lambda.Test.e3 ==> "let x0 = True in x0 & x0"
-	 , Lambda.Test.e4 ==> "let x0 = \\x1 -> x1 & x1 in x0 True"
-	 , Lambda.Test.e5 ==> "\\x0 -> (\\x1 -> x0 & x1)"
-	 , Lambda.Test.e6 ==> "(let x0 = True in x0) & False"
-	 , Lambda.Test.e7 ==> "\\x0 -> x0 True & True"
-	 , Lambda.Test.e8 ==> "\\x0 -> x0 (True & True)"
+	 [ Lambda.Test.e1 ==> "\\x0 -> (\\x1 -> (x0 || x1) && !(x0 && x1))"
+	 , Lambda.Test.e2 ==> "\\x0 -> (\\x1 -> x0 && !x1 || !x0 && x1)"
+	 , Lambda.Test.e3 ==> "let x0 = True in x0 && x0"
+	 , Lambda.Test.e4 ==> "let x0 = \\x1 -> x1 && x1 in x0 True"
+	 , Lambda.Test.e5 ==> "\\x0 -> (\\x1 -> x0 && x1)"
+	 , Lambda.Test.e6 ==> "(let x0 = True in x0) && False"
+	 , Lambda.Test.e7 ==> "\\x0 -> x0 True && True"
+	 , Lambda.Test.e8 ==> "\\x0 -> x0 (True && True)"
 	 ]
  , testGroup "Maybe"
 	 [ Maybe.Test.e1 ==> "maybe True (\\x0 -> !x0) (just True)"
 	 ]
  , testGroup "Eq"
-	 [ Eq.Test.e1 ==> "if True & True == True | False then True else False"
-	 , Eq.Test.e2 ==> "if True & True | False == True & (True | False) then True else False"
+	 [ Eq.Test.e1 ==> "if True && True == True || False then True else False"
+	 , Eq.Test.e2 ==> "if True && True || False == True && (True || False) then True else False"
 	 , Eq.Test.e3 ==> "if !(True == False) == (True == True) then True else False"
 	 ]
- {-, testGroup "If"
-	 [ If.e1 ==> "if True then False else True"
-	 , If.e2 ==> "if True & True then False else True"
+ , testGroup "If"
+	 [ If.Test.e1 ==> "if True then False else True"
+	 , If.Test.e2 ==> "if True && True then False else True"
 	 ]
- -}]
+ ]
diff --git a/Language/Symantic/Trans/Bool/Const.hs b/Language/Symantic/Trans/Bool/Const.hs
index d434d71..b3a61b1 100644
--- a/Language/Symantic/Trans/Bool/Const.hs
+++ b/Language/Symantic/Trans/Bool/Const.hs
@@ -6,7 +6,7 @@
 module Language.Symantic.Trans.Bool.Const where
 
 import qualified Data.Bool as Bool
-import Prelude hiding (and, not, or)
+import Prelude hiding ((&&), not, (||))
 
 import Language.Symantic.Trans.Common
 import Language.Symantic.Expr.Bool
@@ -33,21 +33,21 @@ instance
 	not (Trans_Bool_Const_Unknown e) = Trans_Bool_Const_Unknown $ not e
 	not (Trans_Bool_Const_Known   x) = Trans_Bool_Const_Known $ Bool.not x
 	
-	and (Trans_Bool_Const_Known True) y   = y
-	and (Trans_Bool_Const_Known False) _y = Trans_Bool_Const_Known False
-	and x  (Trans_Bool_Const_Known True)  = x
-	and _x (Trans_Bool_Const_Known False) = Trans_Bool_Const_Known False
-	and (Trans_Bool_Const_Unknown x)
-	    (Trans_Bool_Const_Unknown y)
-	 =   Trans_Bool_Const_Unknown $ and x y
+	(&&) (Trans_Bool_Const_Known True) y   = y
+	(&&) (Trans_Bool_Const_Known False) _y = Trans_Bool_Const_Known False
+	(&&) x  (Trans_Bool_Const_Known True)  = x
+	(&&) _x (Trans_Bool_Const_Known False) = Trans_Bool_Const_Known False
+	(&&) (Trans_Bool_Const_Unknown x)
+	     (Trans_Bool_Const_Unknown y)
+	 =   Trans_Bool_Const_Unknown $ (&&) x y
 	
-	or (Trans_Bool_Const_Known False) y = y
-	or (Trans_Bool_Const_Known True) _y = Trans_Bool_Const_Known True
-	or x (Trans_Bool_Const_Known False) = x
-	or _x (Trans_Bool_Const_Known True) = Trans_Bool_Const_Known True
-	or (Trans_Bool_Const_Unknown x)
-	   (Trans_Bool_Const_Unknown y)
-	 =  Trans_Bool_Const_Unknown $ or x y
+	(||) (Trans_Bool_Const_Known False) y = y
+	(||) (Trans_Bool_Const_Known True) _y = Trans_Bool_Const_Known True
+	(||) x (Trans_Bool_Const_Known False) = x
+	(||) _x (Trans_Bool_Const_Known True) = Trans_Bool_Const_Known True
+	(||) (Trans_Bool_Const_Unknown x)
+	     (Trans_Bool_Const_Unknown y)
+	 =  Trans_Bool_Const_Unknown $ (||) x y
 
 -- | Transformer.
 trans_bool_const
diff --git a/Language/Symantic/Trans/Bool/Const/Test.hs b/Language/Symantic/Trans/Bool/Const/Test.hs
index 094c558..d321aae 100644
--- a/Language/Symantic/Trans/Bool/Const/Test.hs
+++ b/Language/Symantic/Trans/Bool/Const/Test.hs
@@ -24,8 +24,8 @@ tests = testGroup "Const" $
  , Bool.e3 ==> "True"
  , Bool.e4 ==> "True"
  , Bool.e5 ==> "!x"
- , Bool.e6 ==> "(x | y) & !(x & y)"
- , Bool.e7 ==> "((x | y) & !(x & y) | z) & !(((x | y) & !(x & y)) & z)"
- , Bool.e8 ==> "(x | !y) & !(x & !y)"
+ , Bool.e6 ==> "(x || y) && !(x && y)"
+ , Bool.e7 ==> "((x || y) && !(x && y) || z) && !(((x || y) && !(x && y)) && z)"
+ , Bool.e8 ==> "(x || !y) && !(x && !y)"
  ]
 
diff --git a/Language/Symantic/Trans/Common.hs b/Language/Symantic/Trans/Common.hs
index c08685f..4d523d3 100644
--- a/Language/Symantic/Trans/Common.hs
+++ b/Language/Symantic/Trans/Common.hs
@@ -9,29 +9,29 @@ module Language.Symantic.Trans.Common where
 --
 -- NOTE: @DefaultSignatures@ can be used
 -- when declaring a symantic type class
--- to provide default definition of the methods
+-- to provide default definition of the methods:
 -- implementing their identity transformation
 -- in order to avoid boilerplate code
 -- when writting 'Trans' instances which
 -- do not need to alterate those methods.
-class Trans trans repr where
+class Trans t repr where
 	-- | Lift an interpreter to the transformer's.
-	trans_lift  :: repr a -> trans repr a
+	trans_lift  :: repr a -> t repr a
 	-- | Unlift an interpreter from the transformer's.
-	trans_apply :: trans repr a -> repr a
+	trans_apply :: t repr a -> repr a
 	
 	-- | Convenient method to define the identity transformation for a unary symantic method.
-	trans_map1 :: (repr a -> repr b) -> (trans repr a -> trans repr b)
+	trans_map1 :: (repr a -> repr b) -> (t repr a -> t repr b)
 	trans_map1 f = trans_lift . f . trans_apply
 	
 	-- | Convenient method to define the identity transformation for a binary symantic method.
 	trans_map2
 	 :: (repr a -> repr b -> repr c)
-	 -> (trans repr a -> trans repr b -> trans repr c)
+	 -> (t repr a -> t repr b -> t repr c)
 	trans_map2 f e1 e2 = trans_lift (trans_apply e1 `f` trans_apply e2)
 	
 	-- | Convenient method to define the identity transformation for a terary symantic method.
 	trans_map3
 	 :: (repr a -> repr b -> repr c -> repr d)
-	 -> (trans repr a -> trans repr b -> trans repr c -> trans repr d)
+	 -> (t repr a -> t repr b -> t repr c -> t repr d)
 	trans_map3 f e1 e2 e3 = trans_lift $ f (trans_apply e1) (trans_apply e2) (trans_apply e3)
diff --git a/Language/Symantic/Type/Bool.hs b/Language/Symantic/Type/Bool.hs
index 79d457e..49aa832 100644
--- a/Language/Symantic/Type/Bool.hs
+++ b/Language/Symantic/Type/Bool.hs
@@ -4,14 +4,13 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 module Language.Symantic.Type.Bool where
 
 import Data.Maybe (isJust)
 import Data.Type.Equality ((:~:)(Refl))
 
 import Language.Symantic.Type.Common
-import Language.Symantic.Type.Fun
-import Language.Symantic.Type.Var
 
 -- * Type 'Type_Bool'
 -- | The 'Bool' type.
@@ -40,10 +39,3 @@ instance Type_Constraint Ord (Type_Bool root) where
 -- | Convenient alias to include a 'Type_Bool' within a type.
 type_bool :: Type_Root_Lift Type_Bool root => root Bool
 type_bool = type_root_lift Type_Bool
-
--- * Type 'Type_Fun_Bool'
--- | Convenient alias.
-type Type_Fun_Bool lam
- = Type_Root (Type_Alt  Type_Var
-             (Type_Alt (Type_Fun lam)
-                        Type_Bool))
diff --git a/Language/Symantic/Type/Common.hs b/Language/Symantic/Type/Common.hs
index 01c538f..df43a30 100644
--- a/Language/Symantic/Type/Common.hs
+++ b/Language/Symantic/Type/Common.hs
@@ -121,6 +121,9 @@ instance
 data Type_Alt curr next (root:: * -> *) h
  =   Type_Alt_Curr (curr root h)
  |   Type_Alt_Next (next root h)
+-- | Convenient alias. Requires @TypeOperators@.
+type (:|:) = Type_Alt
+infixr 5 :|:
 type instance Root_of_Type (Type_Alt curr next root) = root
 type instance Error_of_Type ast (Type_Alt curr next root)
  = Error_of_Type_Alt ast (Error_of_Type ast (curr root))
diff --git a/Language/Symantic/Type/Int.hs b/Language/Symantic/Type/Int.hs
index e152adc..9ac7b73 100644
--- a/Language/Symantic/Type/Int.hs
+++ b/Language/Symantic/Type/Int.hs
@@ -4,15 +4,13 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 module Language.Symantic.Type.Int where
 
 import Data.Maybe (isJust)
 import Data.Type.Equality ((:~:)(Refl))
 
 import Language.Symantic.Type.Common
-import Language.Symantic.Type.Fun
-import Language.Symantic.Type.Bool
-import Language.Symantic.Type.Var
 
 -- * Type 'Type_Int'
 -- | The 'Int' type.
@@ -41,18 +39,3 @@ instance Type_Constraint Ord (Type_Int root) where
 -- | Convenient alias to include a 'Type_Int' within a type.
 type_int :: Type_Root_Lift Type_Int root => root Int
 type_int = type_root_lift Type_Int
-
--- * Type 'Type_Fun_Int'
--- | Convenient alias.
-type Type_Fun_Int lam
- = Type_Root (Type_Alt  Type_Var
-             (Type_Alt (Type_Fun lam)
-                        Type_Int))
-
--- * Type 'Type_Fun_Bool_Int'
--- | Convenient alias.
-type Type_Fun_Bool_Int lam
- = Type_Root (Type_Alt  Type_Var
-             (Type_Alt (Type_Fun lam)
-             (Type_Alt  Type_Bool
-                        Type_Int)))
diff --git a/Language/Symantic/Type/List.hs b/Language/Symantic/Type/List.hs
index 86b1626..f2d6e4c 100644
--- a/Language/Symantic/Type/List.hs
+++ b/Language/Symantic/Type/List.hs
@@ -47,8 +47,7 @@ instance -- Show
 -- | Convenient alias to include a 'Type_List' within a type.
 type_list
  :: Type_Root_Lift Type_List root
- => root h_a
- -> root [h_a]
+ => root h_a -> root [h_a]
 type_list a = type_root_lift (Type_List a)
 
 -- * Type 'Type_Fun_Bool_List'
diff --git a/Language/Symantic/Type/Map.hs b/Language/Symantic/Type/Map.hs
index 59cdb1d..a8882c3 100644
--- a/Language/Symantic/Type/Map.hs
+++ b/Language/Symantic/Type/Map.hs
@@ -11,9 +11,6 @@ import Data.Maybe (isJust)
 import Data.Type.Equality ((:~:)(Refl))
 
 import Language.Symantic.Type.Common
-import Language.Symantic.Type.Fun
-import Language.Symantic.Type.Bool
-import Language.Symantic.Type.Var
 
 -- * Type 'Type_Map'
 -- | The 'Map' type.
@@ -56,11 +53,3 @@ type_map
  -> root h_a
  -> root (Map h_k h_a)
 type_map k a = type_root_lift (Type_Map k a)
-
--- * Type 'Type_Fun_Bool_Map'
--- | Convenient alias.
-type Type_Fun_Bool_Map lam
- = Type_Root (Type_Alt Type_Var
-             (Type_Alt (Type_Fun lam)
-             (Type_Alt Type_Bool
-                       Type_Map)))
diff --git a/Language/Symantic/Type/Maybe.hs b/Language/Symantic/Type/Maybe.hs
index acb7267..70a6b82 100644
--- a/Language/Symantic/Type/Maybe.hs
+++ b/Language/Symantic/Type/Maybe.hs
@@ -4,15 +4,13 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 module Language.Symantic.Type.Maybe where
 
 import Data.Maybe (isJust)
 import Data.Type.Equality ((:~:)(Refl))
 
 import Language.Symantic.Type.Common
-import Language.Symantic.Type.Fun
-import Language.Symantic.Type.Bool
-import Language.Symantic.Type.Var
 
 -- * Type 'Type_Maybe'
 -- | The 'Maybe' type.
@@ -50,11 +48,3 @@ type_maybe
  => root h_a
  -> root (Maybe h_a)
 type_maybe a = type_root_lift (Type_Maybe a)
-
--- * Type 'Type_Fun_Bool_Maybe'
--- | Convenient alias.
-type Type_Fun_Bool_Maybe lam
- = Type_Root (Type_Alt Type_Var
-             (Type_Alt (Type_Fun lam)
-             (Type_Alt Type_Bool
-                       Type_Maybe)))
diff --git a/Language/Symantic/Type/Test.hs b/Language/Symantic/Type/Test.hs
index e5d2c39..3ca187d 100644
--- a/Language/Symantic/Type/Test.hs
+++ b/Language/Symantic/Type/Test.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeOperators #-}
 module Type.Test where
 
 import Test.Tasty
@@ -9,6 +10,10 @@ import Language.Symantic.Type
 
 import AST.Test
 
+type Type_Fun_Bool     lam = Type_Root (Type_Fun lam :|: Type_Bool)
+type Type_Fun_Bool_Int lam = Type_Root (Type_Fun lam :|: Type_Bool :|: Type_Int)
+type Type_Fun_Int      lam = Type_Root (Type_Fun lam :|: Type_Int)
+
 tests :: TestTree
 tests = testGroup "Type" $
 	let (==>) ast expected p =
diff --git a/Language/Symantic/Type/Unit.hs b/Language/Symantic/Type/Unit.hs
index 74008e5..8631b2a 100644
--- a/Language/Symantic/Type/Unit.hs
+++ b/Language/Symantic/Type/Unit.hs
@@ -1,10 +1,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE UndecidableInstances #-}
 module Language.Symantic.Type.Unit where
 
 import Data.Maybe (isJust)
diff --git a/Language/Symantic/Type/Var.hs b/Language/Symantic/Type/Var.hs
index 5b7f66a..65c7da2 100644
--- a/Language/Symantic/Type/Var.hs
+++ b/Language/Symantic/Type/Var.hs
@@ -1,11 +1,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
 -- | Type variable.
 module Language.Symantic.Type.Var
  ( module Language.Symantic.Type.Var
diff --git a/symantic.cabal b/symantic.cabal
index d0cc870..87d7172 100644
--- a/symantic.cabal
+++ b/symantic.cabal
@@ -132,7 +132,7 @@ Library
     base >= 4.6 && < 5
     , containers
     , ghc-prim
-    , monad-classes >= 0.3.1.1
+    -- , monad-classes >= 0.3.1.1
     , transformers
     , text
 
@@ -152,6 +152,7 @@ Test-Suite symantic-test
     Expr.If.Test
     Expr.Int.Test
     Expr.Lambda.Test
+    Expr.List.Test
     Expr.Maybe.Test
     Expr.Test
     Repr.Host.Test
-- 
2.47.2