]> Git — Sourcephile - haskell/symantic.git/blob - Language/LOL/Symantic/Type/Bool.hs
init
[haskell/symantic.git] / Language / LOL / Symantic / Type / Bool.hs
1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE MultiParamTypeClasses #-}
4 {-# LANGUAGE OverloadedStrings #-}
5 {-# LANGUAGE TypeFamilies #-}
6 {-# LANGUAGE UndecidableInstances #-}
7 module Language.LOL.Symantic.Type.Bool where
8
9 import Data.Maybe (isJust)
10 import Data.Type.Equality ((:~:)(Refl))
11
12 import Language.LOL.Symantic.Raw
13 import Language.LOL.Symantic.Type.Common
14 import Language.LOL.Symantic.Type.Fun
15
16 -- * Type 'Type_Bool'
17
18 -- | The 'Bool' type.
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 raw (Type_Bool root) = Error_Type_Fun raw
23
24 -- | Convenient alias.
25 type Type_Fun_Bool lam = Type_Root (Type_Cons (Type_Fun lam) Type_Bool)
26
27 -- | Convenient alias to include a 'Type_Bool' within a type.
28 type_bool :: Type_Root_Lift Type_Bool root => root Bool
29 type_bool = type_root_lift Type_Bool
30
31 {-
32 r :: Type_Root_Lift curr root => curr root h -> root h
33 r = type_root_lift
34
35 t0 :: Type_Root Type_Bool Bool
36 t0 = Type_Root $ Type_Bool
37
38 t1 :: Type_Fun_Bool lam (lam Bool -> lam Bool)
39 t1 = r $ Type_Fun (r Type_Bool) (r Type_Bool)
40
41 t2 :: Type_Fun_Bool lam (lam Bool -> lam (lam Bool -> lam Bool))
42 t2 = r $ Type_Fun (r Type_Bool) (r $ Type_Fun (r Type_Bool) (r Type_Bool))
43
44 t3 :: Type_Fun_Bool lam (lam (lam Bool -> lam Bool) -> lam Bool)
45 t3 = r $ Type_Fun (r $ Type_Fun (r Type_Bool) (r Type_Bool)) (r Type_Bool)
46 -}
47
48 instance -- Type_Eq
49 Type_Eq (Type_Bool root) where
50 type_eq Type_Bool Type_Bool = Just Refl
51 instance -- Eq
52 Eq (Type_Bool root h) where
53 x == y = isJust $ type_eq x y
54 instance -- Type_from Raw
55 ( Type_Root_Lift Type_Bool root
56 , Error_Type_Lift (Error_Type_Fun Raw) (Error_of_Type Raw root)
57 -- NOTE: require UndecidableInstances.
58 ) => Type_from Raw (Type_Bool root) where
59 type_from _px_ty raw@(Raw "Bool" raws) k =
60 case raws of
61 [] -> k $ type_root_lift Type_Bool
62 _ -> Left $ Just $ error_type_lift $
63 Error_Type_Fun_Wrong_number_of_arguments 0 raw
64 type_from _px_ty _raw _k = Left Nothing
65 instance -- String_from_Type
66 String_from_Type (Type_Bool root) where
67 string_from_type Type_Bool = "Bool"
68 instance -- Show
69 Show (Type_Bool root h) where
70 show = string_from_type