]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Either.hs
factorizing Type1_From ast Type0
[haskell/symantic.git] / 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 qualified Data.MonoTraversable as MT
13
14 import Language.Symantic.Type.Root
15 import Language.Symantic.Type.Type0
16 import Language.Symantic.Type.Type1
17 import Language.Symantic.Type.Type2
18 import Language.Symantic.Type.Constraint
19 import Language.Symantic.Type.Family
20
21 -- * Type 'Type_Either'
22 -- | The 'Either' type.
23 type Type_Either = Type2 (Proxy Either)
24
25 pattern Type_Either
26 :: root l -> root r
27 -> Type_Either root (Either l r)
28 pattern Type_Either l r
29 = Type2 Proxy l r
30
31 instance Type1_Unlift Type_Either where
32 type1_unlift (Type2 px a b) k =
33 k ( Type1 (Proxy::Proxy (Either a)) b
34 , Type1_Lift (\(Type1 _ b') -> Type2 px a b')
35 )
36 instance Type0_Eq root => Type1_Eq (Type_Either root) where
37 type1_eq (Type2 _ a1 _b1) (Type2 _ a2 _b2)
38 | Just Refl <- type0_eq a1 a2
39 = Just Refl
40 type1_eq _ _ = Nothing
41 instance
42 Type0_Constraint Eq root =>
43 Type0_Constraint Eq (Type_Either root) where
44 type0_constraint c (Type2 _ l r)
45 | Just Dict <- type0_constraint c l
46 , Just Dict <- type0_constraint c r
47 = Just Dict
48 type0_constraint _c _ = Nothing
49 instance
50 Type0_Constraint Ord root =>
51 Type0_Constraint Ord (Type_Either root) where
52 type0_constraint c (Type2 _ l r)
53 | Just Dict <- type0_constraint c l
54 , Just Dict <- type0_constraint c r
55 = Just Dict
56 type0_constraint _c _ = Nothing
57 instance Type0_Constraint Num (Type_Either root)
58 instance Type0_Constraint Integral (Type_Either root)
59 instance Type0_Family Type_Family_MonoElement (Type_Either root) where
60 type0_family _at (Type2 _px _l r) = Just r
61 instance Type0_Constraint MT.MonoFunctor (Type_Either root) where
62 type0_constraint _c Type2{} = Just Dict
63 instance Type1_Constraint Functor (Type_Either root) where
64 type1_constraint _c Type2{} = Just Dict
65 instance Type1_Constraint Applicative (Type_Either root) where
66 type1_constraint _c Type2{} = Just Dict
67 instance Type1_Constraint Traversable (Type_Either root) where
68 type1_constraint _c Type2{} = Just Dict
69 instance Type1_Constraint Foldable (Type_Either root) where
70 type1_constraint _c Type2{} = Just Dict
71 instance Type1_Constraint Monad (Type_Either root) where
72 type1_constraint _c Type2{} = Just Dict
73 instance -- Type0_Eq
74 Type0_Eq root =>
75 Type0_Eq (Type_Either root) where
76 type0_eq
77 (Type2 _ l1 r1)
78 (Type2 _ l2 r2)
79 | Just Refl <- l1 `type0_eq` l2
80 , Just Refl <- r1 `type0_eq` r2
81 = Just Refl
82 type0_eq _ _ = Nothing
83 instance -- String_from_Type
84 String_from_Type root =>
85 String_from_Type (Type_Either root) where
86 string_from_type (Type2 _ l r) =
87 "Either"
88 ++ " (" ++ string_from_type l ++ ")"
89 ++ " (" ++ string_from_type r ++ ")"
90
91 -- | Inject 'Type_Either' within a root type.
92 type_either
93 :: Type_Root_Lift Type_Either root
94 => root h_l -> root h_r -> root (Either h_l h_r)
95 type_either = type2