Language/Symantic/Type/Either.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.Either where
   9
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import qualified Data.MonoTraversable as MT
  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_Either'
  22 -- | The 'Either' type.
  23 type Type_Either = Type2 (Proxy Either)
  24
  25 pattern Type_Either
  26  :: root l -> root r
  27  -> Type_Either root (Either l r)
  28 pattern Type_Either l r
  29  = Type2 Proxy l r
  30
  31 instance Type1_Unlift Type_Either where
  32         type1_unlift (Type2 px a b) k =
  33                 k ( Type1 (Proxy::Proxy (Either a)) b
  34                   , Type1_Lift (\(Type1 _ b') -> Type2 px a b')
  35                   )
  36 instance Type0_Eq root => Type1_Eq (Type_Either root) where
  37         type1_eq (Type2 _ a1 _b1) (Type2 _ a2 _b2)
  38          | Just Refl <- type0_eq a1 a2
  39          = Just Refl
  40         type1_eq _ _ = Nothing
  41 instance
  42  Type0_Constraint Eq root =>
  43  Type0_Constraint Eq (Type_Either root) where
  44         type0_constraint c (Type2 _ l r)
  45          | Just Dict <- type0_constraint c l
  46          , Just Dict <- type0_constraint c r
  47          = Just Dict
  48         type0_constraint _c _ = Nothing
  49 instance
  50  Type0_Constraint Ord root =>
  51  Type0_Constraint Ord (Type_Either root) where
  52         type0_constraint c (Type2 _ l r)
  53          | Just Dict <- type0_constraint c l
  54          , Just Dict <- type0_constraint c r
  55          = Just Dict
  56         type0_constraint _c _ = Nothing
  57 instance Type0_Constraint Num (Type_Either root)
  58 instance Type0_Constraint Integral (Type_Either root)
  59 instance Type0_Family Type_Family_MonoElement (Type_Either root) where
  60         type0_family _at (Type2 _px _l r) = Just r
  61 instance Type0_Constraint MT.MonoFunctor (Type_Either root) where
  62         type0_constraint _c Type2{} = Just Dict
  63 instance Type1_Constraint Functor (Type_Either root) where
  64         type1_constraint _c Type2{} = Just Dict
  65 instance Type1_Constraint Applicative (Type_Either root) where
  66         type1_constraint _c Type2{} = Just Dict
  67 instance Type1_Constraint Traversable (Type_Either root) where
  68         type1_constraint _c Type2{} = Just Dict
  69 instance Type1_Constraint Foldable (Type_Either root) where
  70         type1_constraint _c Type2{} = Just Dict
  71 instance Type1_Constraint Monad (Type_Either root) where
  72         type1_constraint _c Type2{} = Just Dict
  73 instance -- Type0_Eq
  74  Type0_Eq root =>
  75  Type0_Eq (Type_Either root) where
  76         type0_eq
  77          (Type2 _ l1 r1)
  78          (Type2 _ l2 r2)
  79          | Just Refl <- l1 `type0_eq` l2
  80          , Just Refl <- r1 `type0_eq` r2
  81          = Just Refl
  82         type0_eq _ _ = Nothing
  83 instance -- String_from_Type
  84  String_from_Type root =>
  85  String_from_Type (Type_Either root) where
  86         string_from_type (Type2 _ l r) =
  87                 "Either"
  88                  ++ " (" ++ string_from_type l ++ ")"
  89                  ++ " (" ++ string_from_type r ++ ")"
  90
  91 -- | Inject 'Type_Either' within a root type.
  92 type_either
  93  :: Type_Root_Lift Type_Either root
  94  => root h_l -> root h_r -> root (Either h_l h_r)
  95 type_either = type2