Language/Symantic/Type/Map.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE PatternSynonyms #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# OPTIONS_GHC -fno-warn-orphans #-}
  10 module Language.Symantic.Type.Map where
  11
  12 import Data.Map.Strict as Map
  13 import qualified Data.MonoTraversable as MT
  14 import Data.Proxy
  15 import Data.Type.Equality ((:~:)(Refl))
  16
  17 import Language.Symantic.Type.Root
  18 import Language.Symantic.Type.Type0
  19 import Language.Symantic.Type.Type1
  20 import Language.Symantic.Type.Type2
  21 import Language.Symantic.Type.Constraint
  22 import Language.Symantic.Type.Family
  23
  24 -- * Type 'Type_Map'
  25 -- | The 'Map' type.
  26 type Type_Map = Type2 (Proxy Map)
  27
  28 pattern Type_Map
  29  :: root k -> root a
  30  -> Type2 (Proxy Map) root (Map k a)
  31 pattern Type_Map k a
  32  = Type2 Proxy k a
  33
  34 instance Type1_Unlift Type_Map where
  35         type1_unlift (Type2 px a b) k =
  36                 k ( Type1 (Proxy::Proxy (Map a)) b
  37                   , Type1_Lift (\(Type1 _ b') -> Type2 px a b')
  38                   )
  39 instance
  40  Type0_Constraint Eq root =>
  41  Type0_Constraint Eq (Type_Map root) where
  42         type0_constraint c (Type2 _ k a)
  43          | Just Dict <- type0_constraint c k
  44          , Just Dict <- type0_constraint c a
  45          = Just Dict
  46         type0_constraint _c _ = Nothing
  47 instance
  48  Type0_Constraint Ord root =>
  49  Type0_Constraint Ord (Type_Map root) where
  50         type0_constraint c (Type2 _ k a)
  51          | Just Dict <- type0_constraint c k
  52          , Just Dict <- type0_constraint c a
  53          = Just Dict
  54         type0_constraint _c _ = Nothing
  55 instance
  56  Type0_Constraint Ord root =>
  57  Type0_Constraint Monoid (Type_Map root) where
  58         type0_constraint _c (Type2 _ k _a)
  59          | Just Dict <- type0_constraint (Proxy::Proxy Ord) k
  60          = Just Dict
  61         type0_constraint _c _ = Nothing
  62 instance Type0_Constraint Num (Type_Map root)
  63 instance Type0_Constraint Integral (Type_Map root)
  64 instance Type0_Constraint MT.MonoFunctor (Type_Map root) where
  65         type0_constraint _c Type2{} = Just Dict
  66 instance Type1_Constraint Functor (Type_Map root) where
  67         type1_constraint _c Type2{} = Just Dict
  68 instance Type1_Constraint Traversable (Type_Map root) where
  69         type1_constraint _c Type2{} = Just Dict
  70 instance Type1_Constraint Foldable (Type_Map root) where
  71         type1_constraint _c Type2{} = Just Dict
  72 instance Type0_Family Type_Family_MonoElement (Type_Map root) where
  73         type0_family _at (Type2 _px _k a) = Just a
  74 instance -- Type0_Eq
  75  Type0_Eq root =>
  76  Type0_Eq (Type_Map root) where
  77         type0_eq (Type2 _px1 k1 a1) (Type2 _px2 k2 a2)
  78          | Just Refl <- k1 `type0_eq` k2
  79          , Just Refl <- a1 `type0_eq` a2
  80          = Just Refl
  81         type0_eq _ _ = Nothing
  82 instance -- Type1_Eq
  83  Type0_Eq root =>
  84  Type1_Eq (Type_Map root) where
  85         type1_eq (Type2 _px1 k1 _a1) (Type2 _px2 k2 _a2)
  86          | Just Refl <- k1 `type0_eq` k2
  87          = Just Refl
  88         type1_eq _ _ = Nothing
  89 instance -- String_from_Type
  90  String_from_Type root =>
  91  String_from_Type (Type_Map root) where
  92         string_from_type (Type2 _ k a) =
  93                 "Map (" ++ string_from_type k ++ ")"
  94                  ++ " (" ++ string_from_type a ++ ")"
  95
  96 -- | Inject 'Type_Map' within a root type.
  97 type_map
  98  :: Type_Root_Lift Type_Map root
  99  => root h_k -> root h_a -> root (Map h_k h_a)
 100 type_map = type2