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