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