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