Language/Symantic/Type/Tuple.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE PatternSynonyms #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# OPTIONS_GHC -fno-warn-orphans #-}
   8 module Language.Symantic.Type.Tuple where
   9
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Language.Symantic.Type.Root
  13 import Language.Symantic.Type.Type0
  14 import Language.Symantic.Type.Type1
  15 import Language.Symantic.Type.Type2
  16
  17 -- * Type 'Type_Tuple2'
  18 -- | The @(,)@ type.
  19 type Type_Tuple2 = Type_Type2 (Proxy (,))
  20
  21 pattern Type_Tuple2
  22  :: root a -> root b
  23  -> Type_Tuple2 root ((,) a b)
  24 pattern Type_Tuple2 a b
  25  = Type_Type2 Proxy a b
  26
  27 instance Unlift_Type1 Type_Tuple2 where
  28         unlift_type1 (Type_Type2 px a b) k =
  29                 k ( Type_Type1 (Proxy::Proxy ((,) a)) b
  30                   , Lift_Type1 (\(Type_Type1 _ b') -> Type_Type2 px a b')
  31                   )
  32 instance
  33  Constraint_Type Eq root =>
  34  Constraint_Type Eq (Type_Tuple2 root) where
  35         constraint_type c (Type_Type2 _ a b)
  36          | Just Dict <- constraint_type c a
  37          , Just Dict <- constraint_type c b
  38          = Just Dict
  39         constraint_type _c _ = Nothing
  40 instance
  41  Constraint_Type Ord root =>
  42  Constraint_Type Ord (Type_Tuple2 root) where
  43         constraint_type c (Type_Type2 _ a b)
  44          | Just Dict <- constraint_type c a
  45          , Just Dict <- constraint_type c b
  46          = Just Dict
  47         constraint_type _c _ = Nothing
  48 instance
  49  Constraint_Type Monoid root =>
  50  Constraint_Type Monoid (Type_Tuple2 root) where
  51         constraint_type c (Type_Type2 _ a b)
  52          | Just Dict <- constraint_type c a
  53          , Just Dict <- constraint_type c b
  54          = Just Dict
  55         constraint_type _c _ = Nothing
  56 instance Constraint_Type Num (Type_Tuple2 root)
  57 instance Constraint_Type Integral (Type_Tuple2 root)
  58 instance Constraint_Type1 Functor (Type_Tuple2 root) where
  59         constraint_type1 _c Type_Type2{} = Just Dict
  60 instance
  61  Constraint_Type Monoid root =>
  62  Constraint_Type1 Applicative (Type_Tuple2 root) where
  63         constraint_type1 _c (Type_Type2 _ a _b)
  64          | Just Dict <- constraint_type (Proxy::Proxy Monoid) a
  65          = Just Dict
  66         constraint_type1 _c _ = Nothing
  67 instance Constraint_Type1 Foldable (Type_Tuple2 root) where
  68         constraint_type1 _c Type_Type2{} = Just Dict
  69 instance Constraint_Type1 Traversable (Type_Tuple2 root) where
  70         constraint_type1 _c Type_Type2{} = Just Dict
  71 instance -- Eq_Type
  72  Eq_Type root =>
  73  Eq_Type (Type_Tuple2 root) where
  74         eq_type (Type_Type2 _px1 a1 b1) (Type_Type2 _px2 a2 b2)
  75          | Just Refl <- a1 `eq_type` a2
  76          , Just Refl <- b1 `eq_type` b2
  77          = Just Refl
  78         eq_type _ _ = Nothing
  79 instance -- Eq_Type1
  80  Eq_Type root =>
  81  Eq_Type1 (Type_Tuple2 root) where
  82         eq_type1 (Type_Type2 _px1 a1 _b1) (Type_Type2 _px2 a2 _b2)
  83          | Just Refl <- a1 `eq_type` a2
  84          = Just Refl
  85         eq_type1 _ _ = Nothing
  86 instance -- String_from_Type
  87  String_from_Type root =>
  88  String_from_Type (Type_Tuple2 root) where
  89         string_from_type (Type_Type2 _ a b) =
  90                 "("  ++ string_from_type a ++
  91                 ", " ++ string_from_type b ++ ")"
  92
  93 -- | Inject 'Type_Tuple2' within a root type.
  94 type_tuple2
  95  :: forall root h_a h_b.
  96  Lift_Type_Root Type_Tuple2 root
  97  => root h_a
  98  -> root h_b
  99  -> root (h_a, h_b)
 100 type_tuple2 a b = lift_type_root
 101          (Type_Tuple2 a b
 102          ::Type_Tuple2 root (h_a, h_b))