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 {-
  43 instance Constraint_Type1 Functor (Type_Type1 (Proxy ((,) fst)) root) where
  44         constraint_type1 _c Type_Type1{} = Just Dict
  45 instance Constraint_Type1 Functor (Type_Tuple2 root) where
  46 instance Constraint_Type1 Applicative (Type_Type1 (Proxy ((,) fst)) root)
  47 -}
  48
  49 pattern Type_Either
  50  :: root l -> root r
  51  -> Type_Either root (Either l r)
  52 pattern Type_Either l r
  53  = Type_Type2 Proxy l r
  54
  55 instance -- Eq_Type
  56  Eq_Type root =>
  57  Eq_Type (Type_Either root) where
  58         eq_type
  59          (Type_Type2 _ l1 r1)
  60          (Type_Type2 _ l2 r2)
  61          | Just Refl <- l1 `eq_type` l2
  62          , Just Refl <- r1 `eq_type` r2
  63          = Just Refl
  64         eq_type _ _ = Nothing
  65 instance -- String_from_Type
  66  String_from_Type root =>
  67  String_from_Type (Type_Either root) where
  68         string_from_type (Type_Type2 _ l r) =
  69                 "Either"
  70                  ++ " (" ++ string_from_type l ++ ")"
  71                  ++ " (" ++ string_from_type r ++ ")"
  72
  73 -- | Inject 'Type_Either' within a root type.
  74 type_either
  75  :: forall root h_l h_r.
  76  Lift_Type_Root Type_Either root
  77  => root h_l
  78  -> root h_r
  79  -> root (Either h_l h_r)
  80 type_either l r = lift_type_root
  81          (Type_Either l r
  82          ::Type_Either root (Either h_l h_r))