1 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE MultiParamTypeClasses #-}
4 {-# LANGUAGE OverloadedStrings #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeFamilies #-}
7 module Language.Symantic.Type.List where
9 import Data.Maybe (isJust)
10 import Data.Type.Equality ((:~:)(Refl))
12 import Language.Symantic.Type.Common
13 import Language.Symantic.Type.Fun
14 import Language.Symantic.Type.Bool
15 import Language.Symantic.Type.Var
19 data Type_List root h where
21 -> Type_List root [h_a]
23 type instance Root_of_Type (Type_List root) = root
24 type instance Error_of_Type ast (Type_List root) = No_Error_Type
28 Eq_Type (Type_List root) where
29 eq_type (Type_List a1) (Type_List a2)
30 | Just Refl <- a1 `eq_type` a2
35 Eq (Type_List root h) where
36 x == y = isJust $ eq_type x y
37 instance -- String_from_Type
38 String_from_Type root =>
39 String_from_Type (Type_List root) where
40 string_from_type (Type_List a) =
41 "List (" ++ string_from_type a ++ ")"
43 String_from_Type root =>
44 Show (Type_List root h) where
45 show = string_from_type
47 -- | Convenient alias to include a 'Type_List' within a type.
49 :: Type_Root_Lift Type_List root
50 => root h_a -> root [h_a]
51 type_list a = type_root_lift (Type_List a)
53 -- * Type 'Type_Fun_Bool_List'
54 -- | Convenient alias.
55 type Type_Fun_Bool_List lam
56 = Type_Root (Type_Alt Type_Var
57 (Type_Alt (Type_Fun lam)