Language/Symantic/Type/List.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE PatternSynonyms #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# OPTIONS_GHC -fno-warn-orphans #-}
   7 module Language.Symantic.Type.List where
   8
   9 import qualified Data.MonoTraversable as MT
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12
  13 import Language.Symantic.Type.Root
  14 import Language.Symantic.Type.Type0
  15 import Language.Symantic.Type.Type1
  16 import Language.Symantic.Type.Constraint
  17 import Language.Symantic.Type.Family
  18
  19 -- * Type 'Type_List'
  20 -- | The list type.
  21 type Type_List = Type1 (Proxy [])
  22
  23 pattern Type_List :: root a -> Type_List root ([] a)
  24 pattern Type_List a = Type1 Proxy a
  25
  26 instance Type0_Constraint Eq root => Type0_Constraint Eq (Type_List root) where
  27         type0_constraint c (Type1 _ a)
  28          | Just Dict <- type0_constraint c a
  29          = Just Dict
  30         type0_constraint _c _ = Nothing
  31 instance Type0_Constraint Ord root => Type0_Constraint Ord (Type_List root) where
  32         type0_constraint c (Type1 _ a)
  33          | Just Dict <- type0_constraint c a
  34          = Just Dict
  35         type0_constraint _c _ = Nothing
  36 instance Type0_Constraint Monoid (Type_List root) where
  37         type0_constraint _c Type1{} = Just Dict
  38 instance Type0_Constraint Num (Type_List root)
  39 instance Type0_Constraint Integral (Type_List root)
  40 instance Type0_Constraint MT.MonoFunctor (Type_List root) where
  41         type0_constraint _c Type1{} = Just Dict
  42 instance Type1_Constraint Functor (Type_List root) where
  43         type1_constraint _c Type1{} = Just Dict
  44 instance Type1_Constraint Applicative (Type_List root) where
  45         type1_constraint _c Type1{} = Just Dict
  46 instance Type1_Constraint Foldable (Type_List root) where
  47         type1_constraint _c Type1{} = Just Dict
  48 instance Type1_Constraint Traversable (Type_List root) where
  49         type1_constraint _c Type1{} = Just Dict
  50 instance Type1_Constraint Monad (Type_List root) where
  51         type1_constraint _c Type1{} = Just Dict
  52 instance Type0_Family Type_Family_MonoElement (Type_List root) where
  53         type0_family _at (Type1 _px a) = Just a
  54 instance -- Type0_Eq
  55  Type0_Eq root =>
  56  Type0_Eq (Type_List root) where
  57         type0_eq (Type1 _px1 a1) (Type1 _px2 a2)
  58          | Just Refl <- a1 `type0_eq` a2
  59          = Just Refl
  60         type0_eq _ _ = Nothing
  61 instance -- Type1_Eq
  62  Type1_Eq (Type_List root) where
  63         type1_eq Type1{} Type1{}
  64          = Just Refl
  65 instance -- String_from_Type
  66  String_from_Type root =>
  67  String_from_Type (Type_List root) where
  68         string_from_type (Type1 _f a) =
  69                 "[" ++ string_from_type a ++ "]"
  70
  71 -- | Inject 'Type_List' within a root type.
  72 type_list :: Type_Root_Lift Type_List root => root h_a -> root ([] h_a)
  73 type_list = type1