1 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE MultiParamTypeClasses #-}
4 {-# LANGUAGE OverloadedStrings #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeFamilies #-}
7 {-# LANGUAGE UndecidableInstances #-}
8 module Language.LOL.Symantic.Type.Bool where
10 import Data.Maybe (isJust)
11 import Data.Type.Equality ((:~:)(Refl))
13 import Language.LOL.Symantic.Type.Common
14 import Language.LOL.Symantic.Type.Fun
15 import Language.LOL.Symantic.Type.Var
19 data Type_Bool (root:: * -> *) h where
20 Type_Bool :: Type_Bool root Bool
21 type instance Root_of_Type (Type_Bool root) = root
22 type instance Error_of_Type ast (Type_Bool root) = ()
25 Type_Eq (Type_Bool root) where
26 type_eq Type_Bool Type_Bool = Just Refl
28 Eq (Type_Bool root h) where
29 x == y = isJust $ x `type_eq` y
30 instance -- String_from_Type
31 String_from_Type (Type_Bool root) where
32 string_from_type Type_Bool = "Bool"
34 Show (Type_Bool root h) where
35 show = string_from_type
37 -- | Convenient alias to include a 'Type_Bool' within a type.
38 type_bool :: Type_Root_Lift Type_Bool root => root Bool
39 type_bool = type_root_lift Type_Bool
41 -- * Type 'Type_Fun_Bool'
42 -- | Convenient alias.
43 type Type_Fun_Bool lam
44 = Type_Root (Type_Alt Type_Var
45 (Type_Alt (Type_Fun lam)