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 qualified Data.MonoTraversable as MT
  11 import Data.Proxy
  12 import Data.Type.Equality ((:~:)(Refl))
  13
  14 import Language.Symantic.Type.Root
  15 import Language.Symantic.Type.Type0
  16 import Language.Symantic.Type.Type1
  17 import Language.Symantic.Type.Type2
  18 import Language.Symantic.Type.Constraint
  19 import Language.Symantic.Type.Family
  20
  21 -- * Type 'Type_Tuple2'
  22 -- | The @(,)@ type.
  23 type Type_Tuple2 = Type2 (Proxy (,))
  24
  25 pattern Type_Tuple2
  26  :: root a -> root b
  27  -> Type_Tuple2 root ((,) a b)
  28 pattern Type_Tuple2 a b
  29  = Type2 Proxy a b
  30
  31 instance Type1_Unlift Type_Tuple2 where
  32         type1_unlift (Type2 px a b) k =
  33                 k ( Type1 (Proxy::Proxy ((,) a)) b
  34                   , Type1_Lift (\(Type1 _ b') -> Type2 px a b')
  35                   )
  36 instance
  37  Type0_Constraint Eq root =>
  38  Type0_Constraint Eq (Type_Tuple2 root) where
  39         type0_constraint c (Type2 _ a b)
  40          | Just Dict <- type0_constraint c a
  41          , Just Dict <- type0_constraint c b
  42          = Just Dict
  43         type0_constraint _c _ = Nothing
  44 instance
  45  Type0_Constraint Ord root =>
  46  Type0_Constraint Ord (Type_Tuple2 root) where
  47         type0_constraint c (Type2 _ a b)
  48          | Just Dict <- type0_constraint c a
  49          , Just Dict <- type0_constraint c b
  50          = Just Dict
  51         type0_constraint _c _ = Nothing
  52 instance
  53  Type0_Constraint Monoid root =>
  54  Type0_Constraint Monoid (Type_Tuple2 root) where
  55         type0_constraint c (Type2 _ a b)
  56          | Just Dict <- type0_constraint c a
  57          , Just Dict <- type0_constraint c b
  58          = Just Dict
  59         type0_constraint _c _ = Nothing
  60 instance Type0_Constraint Num (Type_Tuple2 root)
  61 instance Type0_Constraint Integral (Type_Tuple2 root)
  62 instance Type0_Constraint MT.MonoFunctor (Type_Tuple2 root) where
  63         type0_constraint _c Type2{} = Just Dict
  64 instance Type1_Constraint Functor (Type_Tuple2 root) where
  65         type1_constraint _c Type2{} = Just Dict
  66 instance
  67  Type0_Constraint Monoid root =>
  68  Type1_Constraint Applicative (Type_Tuple2 root) where
  69         type1_constraint _c (Type2 _ a _b)
  70          | Just Dict <- type0_constraint (Proxy::Proxy Monoid) a
  71          = Just Dict
  72         type1_constraint _c _ = Nothing
  73 instance Type1_Constraint Foldable (Type_Tuple2 root) where
  74         type1_constraint _c Type2{} = Just Dict
  75 instance Type1_Constraint Traversable (Type_Tuple2 root) where
  76         type1_constraint _c Type2{} = Just Dict
  77 instance Type0_Family Type_Family_MonoElement (Type_Tuple2 root) where
  78         type0_family _at (Type2 _px _a b) = Just b
  79 instance -- Type0_Eq
  80  Type0_Eq root =>
  81  Type0_Eq (Type_Tuple2 root) where
  82         type0_eq (Type2 _px1 a1 b1) (Type2 _px2 a2 b2)
  83          | Just Refl <- a1 `type0_eq` a2
  84          , Just Refl <- b1 `type0_eq` b2
  85          = Just Refl
  86         type0_eq _ _ = Nothing
  87 instance -- Type1_Eq
  88  Type0_Eq root =>
  89  Type1_Eq (Type_Tuple2 root) where
  90         type1_eq (Type2 _px1 a1 _b1) (Type2 _px2 a2 _b2)
  91          | Just Refl <- a1 `type0_eq` a2
  92          = Just Refl
  93         type1_eq _ _ = Nothing
  94 instance -- String_from_Type
  95  String_from_Type root =>
  96  String_from_Type (Type_Tuple2 root) where
  97         string_from_type (Type2 _ a b) =
  98                 "("  ++ string_from_type a ++
  99                 ", " ++ string_from_type b ++ ")"
 100
 101 -- | Inject 'Type_Tuple2' within a root type.
 102 type_tuple2
 103  :: forall root h_a h_b.
 104  Type_Root_Lift Type_Tuple2 root
 105  => root h_a
 106  -> root h_b
 107  -> root (h_a, h_b)
 108 type_tuple2 = type2