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 Constraint_Type1 Functor (Type_Either root) where
  32         constraint_type1 _c Type_Type2{} = Just Dict
  33 instance Constraint_Type1 Applicative (Type_Either root) where
  34         constraint_type1 _c Type_Type2{} = Just Dict
  35 instance Constraint_Type1 Traversable (Type_Either root) where
  36         constraint_type1 _c Type_Type2{} = Just Dict
  37 instance Constraint_Type1 Monad (Type_Either root) where
  38         constraint_type1 _c Type_Type2{} = Just Dict
  39
  40 pattern Type_Either
  41  :: root l -> root r
  42  -> Type_Either root (Either l r)
  43 pattern Type_Either l r
  44  = Type_Type2 Proxy l r
  45
  46 instance -- Eq_Type
  47  Eq_Type root =>
  48  Eq_Type (Type_Either root) where
  49         eq_type
  50          (Type_Type2 _ l1 r1)
  51          (Type_Type2 _ l2 r2)
  52          | Just Refl <- l1 `eq_type` l2
  53          , Just Refl <- r1 `eq_type` r2
  54          = Just Refl
  55         eq_type _ _ = Nothing
  56 instance -- String_from_Type
  57  String_from_Type root =>
  58  String_from_Type (Type_Either root) where
  59         string_from_type (Type_Type2 _ l r) =
  60                 "Either"
  61                  ++ " (" ++ string_from_type l ++ ")"
  62                  ++ " (" ++ string_from_type r ++ ")"
  63
  64 -- | Inject 'Type_Either' within a root type.
  65 type_either
  66  :: forall root h_l h_r.
  67  Lift_Type_Root Type_Either root
  68  => root h_l
  69  -> root h_r
  70  -> root (Either h_l h_r)
  71 type_either l r = lift_type_root
  72          (Type_Either l r
  73          ::Type_Either root (Either h_l h_r))