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 import Language.Symantic.Type.Root
  14 import Language.Symantic.Type.Type0
  15 import Language.Symantic.Type.Type1
  16 import Language.Symantic.Type.Type2
  17
  18 -- * Type 'Type_Either'
  19 -- | The 'Either' type.
  20 type Type_Either = Type_Type2 (Proxy Either)
  21
  22 instance Unlift_Type1 Type_Either where
  23         unlift_type1 (Type_Type2 px a b) k =
  24                 k ( Type_Type1 (Proxy::Proxy (Either a)) b
  25                   , Lift_Type1 (\(Type_Type1 _ b') -> Type_Type2 px a b')
  26                   )
  27 instance Eq_Type root => Eq_Type1 (Type_Either root) where
  28         eq_type1 (Type_Type2 _ a1 _b1) (Type_Type2 _ a2 _b2)
  29          | Just Refl <- eq_type a1 a2
  30          = Just Refl
  31         eq_type1 _ _ = Nothing
  32 instance
  33  Constraint_Type Eq root =>
  34  Constraint_Type Eq (Type_Either root) where
  35         constraint_type c (Type_Type2 _ l r)
  36          | Just Dict <- constraint_type c l
  37          , Just Dict <- constraint_type c r
  38          = Just Dict
  39         constraint_type _c _ = Nothing
  40 instance
  41  Constraint_Type Ord root =>
  42  Constraint_Type Ord (Type_Either root) where
  43         constraint_type c (Type_Type2 _ l r)
  44          | Just Dict <- constraint_type c l
  45          , Just Dict <- constraint_type c r
  46          = Just Dict
  47         constraint_type _c _ = Nothing
  48 instance Constraint_Type Num (Type_Either root)
  49 instance Constraint_Type Integral (Type_Either root)
  50 instance Constraint_Type MT.MonoFunctor (Type_Either root) where
  51         constraint_type _c Type_Type2{} = Just Dict
  52 instance Constraint_Type1 Functor (Type_Either root) where
  53         constraint_type1 _c Type_Type2{} = Just Dict
  54 instance Constraint_Type1 Applicative (Type_Either root) where
  55         constraint_type1 _c Type_Type2{} = Just Dict
  56 instance Constraint_Type1 Traversable (Type_Either root) where
  57         constraint_type1 _c Type_Type2{} = Just Dict
  58 instance Constraint_Type1 Monad (Type_Either root) where
  59         constraint_type1 _c Type_Type2{} = Just Dict
  60
  61 pattern Type_Either
  62  :: root l -> root r
  63  -> Type_Either root (Either l r)
  64 pattern Type_Either l r
  65  = Type_Type2 Proxy l r
  66
  67 instance -- Eq_Type
  68  Eq_Type root =>
  69  Eq_Type (Type_Either root) where
  70         eq_type
  71          (Type_Type2 _ l1 r1)
  72          (Type_Type2 _ l2 r2)
  73          | Just Refl <- l1 `eq_type` l2
  74          , Just Refl <- r1 `eq_type` r2
  75          = Just Refl
  76         eq_type _ _ = Nothing
  77 instance -- String_from_Type
  78  String_from_Type root =>
  79  String_from_Type (Type_Either root) where
  80         string_from_type (Type_Type2 _ l r) =
  81                 "Either"
  82                  ++ " (" ++ string_from_type l ++ ")"
  83                  ++ " (" ++ string_from_type r ++ ")"
  84
  85 -- | Inject 'Type_Either' within a root type.
  86 type_either
  87  :: forall root h_l h_r.
  88  Lift_Type_Root Type_Either root
  89  => root h_l
  90  -> root h_r
  91  -> root (Either h_l h_r)
  92 type_either = type_type2