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 Data.Proxy
  14 import Data.Type.Equality ((:~:)(Refl))
  15
  16 import Language.Symantic.Type.Root
  17 import Language.Symantic.Type.Type0
  18 import Language.Symantic.Type.Type1
  19 import Language.Symantic.Type.Type2
  20
  21 -- * Type 'Type_Map'
  22 -- | The 'Map' type.
  23 type Type_Map = Type_Type2 (Proxy Map)
  24
  25 pattern Type_Map
  26  :: root k -> root a
  27  -> Type_Type2 (Proxy Map) root (Map k a)
  28 pattern Type_Map k a
  29  = Type_Type2 Proxy k a
  30
  31 instance Unlift_Type1 Type_Map where
  32         unlift_type1 (Type_Type2 px a b) k =
  33                 k ( Type_Type1 (Proxy::Proxy (Map a)) b
  34                   , Lift_Type1 (\(Type_Type1 _ b') -> Type_Type2 px a b')
  35                   )
  36 instance
  37  Constraint_Type Eq root =>
  38  Constraint_Type Eq (Type_Map root) where
  39         constraint_type c (Type_Type2 _ k a)
  40          | Just Dict <- constraint_type c k
  41          , Just Dict <- constraint_type c a
  42          = Just Dict
  43         constraint_type _c _ = Nothing
  44 instance
  45  Constraint_Type Ord root =>
  46  Constraint_Type Ord (Type_Map root) where
  47         constraint_type c (Type_Type2 _ k a)
  48          | Just Dict <- constraint_type c k
  49          , Just Dict <- constraint_type c a
  50          = Just Dict
  51         constraint_type _c _ = Nothing
  52 instance
  53  Constraint_Type Ord root =>
  54  Constraint_Type Monoid (Type_Map root) where
  55         constraint_type _c (Type_Type2 _ k _a)
  56          | Just Dict <- constraint_type (Proxy::Proxy Ord) k
  57          = Just Dict
  58         constraint_type _c _ = Nothing
  59 instance Constraint_Type1 Functor (Type_Map root) where
  60         constraint_type1 _c Type_Type2{} = Just Dict
  61 instance Constraint_Type1 Traversable (Type_Map root) where
  62         constraint_type1 _c Type_Type2{} = Just Dict
  63 instance Constraint_Type1 Foldable (Type_Map root) where
  64         constraint_type1 _c Type_Type2{} = Just Dict
  65 instance -- Eq_Type
  66  Eq_Type root =>
  67  Eq_Type (Type_Map root) where
  68         eq_type (Type_Type2 _px1 k1 a1) (Type_Type2 _px2 k2 a2)
  69          | Just Refl <- k1 `eq_type` k2
  70          , Just Refl <- a1 `eq_type` a2
  71          = Just Refl
  72         eq_type _ _ = Nothing
  73 instance -- Eq_Type1
  74  Eq_Type root =>
  75  Eq_Type1 (Type_Map root) where
  76         eq_type1 (Type_Type2 _px1 k1 _a1) (Type_Type2 _px2 k2 _a2)
  77          | Just Refl <- k1 `eq_type` k2
  78          = Just Refl
  79         eq_type1 _ _ = Nothing
  80 instance -- String_from_Type
  81  String_from_Type root =>
  82  String_from_Type (Type_Map root) where
  83         string_from_type (Type_Type2 _ k a) =
  84                 "Map (" ++ string_from_type k ++ ")"
  85                  ++ " (" ++ string_from_type a ++ ")"
  86
  87 -- | Inject 'Type_Map' within a root type.
  88 type_map
  89  :: forall root h_k h_a.
  90  (Lift_Type_Root Type_Map root)
  91  => root h_k -> root h_a
  92  -> root (Map h_k h_a)
  93 type_map k a = lift_type_root (Type_Type2 Proxy k a
  94          ::Type_Map root (Map h_k h_a))