Language/Symantic/Type/Either.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE PatternSynonyms #-}
   4 {-# LANGUAGE ScopedTypeVariables #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# OPTIONS_GHC -fno-warn-orphans #-}
   7 module Language.Symantic.Type.Either where
   8
   9 import Data.Proxy
  10 import Language.Symantic.Type.Root
  11 import Language.Symantic.Type.Type0
  12 import Language.Symantic.Type.Type2
  13
  14 -- * Type 'Type_Either'
  15 -- | The 'Either' type.
  16 type Type_Either = Type_Type2 (Proxy Either)
  17
  18 type instance Constraint2_of (Proxy Either)
  19  = Constraint2_Empty
  20
  21 pattern Type_Either
  22  :: root a -> root b
  23  -> Type_Either root (Either a b)
  24 pattern Type_Either a b
  25  = Type_Type2 Proxy a b
  26
  27 instance -- String_from_Type
  28  String_from_Type root =>
  29  String_from_Type (Type_Either root) where
  30         string_from_type (Type_Type2 _ a b) =
  31                 "Either"
  32                  ++ " (" ++ string_from_type a ++ ")"
  33                  ++ " (" ++ string_from_type b ++ ")"
  34
  35 -- | Inject 'Type_Either' within a root type.
  36 type_either
  37  :: forall root h_a h_b.
  38  Lift_Type_Root Type_Either root
  39  => root h_a
  40  -> root h_b
  41  -> root (Either h_a h_b)
  42 type_either a b = lift_type_root
  43          (Type_Either a b
  44          ::Type_Either root (Either h_a h_b))