symantic-lib/Language/Symantic/Lib/Either.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Either'.
   4 module Language.Symantic.Lib.Either where
   5
   6 import Prelude hiding (either)
   7 import qualified Data.Either as Either
   8 import qualified Data.MonoTraversable as MT
   9
  10 import Language.Symantic
  11 import Language.Symantic.Lib.MonoFunctor (Element)
  12 import Language.Symantic.Lib.Function (a0, b1, c2)
  13
  14 -- * Class 'Sym_Either'
  15 type instance Sym Either = Sym_Either
  16 class Sym_Either term where
  17         _Left  :: term l -> term (Either l r)
  18         _Right :: term r -> term (Either l r)
  19         either :: term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
  20
  21         default _Left  :: Sym_Either (UnT term) => Trans term => term l -> term (Either l r)
  22         default _Right :: Sym_Either (UnT term) => Trans term => term r -> term (Either l r)
  23         default either :: Sym_Either (UnT term) => Trans term => term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
  24
  25         _Left  = trans1 _Left
  26         _Right = trans1 _Right
  27         either = trans3 either
  28
  29 -- Interpreting
  30 instance Sym_Either Eval where
  31         _Right = eval1 Right
  32         _Left  = eval1 Left
  33         either = eval3 Either.either
  34 instance Sym_Either View where
  35         _Right = view1 "Right"
  36         _Left  = view1 "Left"
  37         either = view3 "either"
  38 instance (Sym_Either r1, Sym_Either r2) => Sym_Either (Dup r1 r2) where
  39         _Left  = dup1 @Sym_Either _Left
  40         _Right = dup1 @Sym_Either _Right
  41         either = dup3 @Sym_Either either
  42
  43 -- Transforming
  44 instance (Sym_Either term, Sym_Lambda term) => Sym_Either (BetaT term)
  45
  46 -- Typing
  47 instance NameTyOf Either where
  48         nameTyOf _c = ["Either"] `Mod` "Either"
  49 instance FixityOf Either
  50 instance ClassInstancesFor Either where
  51         proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _l))
  52          | Just HRefl <- proj_ConstKiTy @_ @Either c
  53          = case () of
  54                  _ | Just Refl <- proj_Const @Functor     q -> Just Dict
  55                    | Just Refl <- proj_Const @Applicative q -> Just Dict
  56                    | Just Refl <- proj_Const @Monad       q -> Just Dict
  57                    | Just Refl <- proj_Const @Foldable    q -> Just Dict
  58                    | Just Refl <- proj_Const @Traversable q -> Just Dict
  59                  _ -> Nothing
  60         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c l) r))
  61          | Just HRefl <- proj_ConstKiTy @_ @Either c
  62          = case () of
  63                  _ | Just Refl <- proj_Const @Eq q
  64                    , Just Dict <- proveConstraint (tq `tyApp` l)
  65                    , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
  66                    | Just Refl <- proj_Const @Ord q
  67                    , Just Dict <- proveConstraint (tq `tyApp` l)
  68                    , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
  69                    | Just Refl <- proj_Const @Show q
  70                    , Just Dict <- proveConstraint (tq `tyApp` l)
  71                    , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
  72                    | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
  73                    | Just Refl <- proj_Const @MT.MonoFunctor  q -> Just Dict
  74                  _ -> Nothing
  75         proveConstraintFor _c _q = Nothing
  76 instance TypeInstancesFor Either where
  77         expandFamFor _c _len f (TyApp _ (TyApp _ c _ty_l) r `TypesS` TypesZ)
  78          | Just HRefl <- proj_ConstKi @_ @Element f
  79          , Just HRefl <- proj_ConstKiTy @_ @Either c
  80          = Just r
  81         expandFamFor _c _len _fam _as = Nothing
  82
  83 -- Compiling
  84 instance Gram_Term_AtomsFor src ss g Either
  85 instance (Source src, SymInj ss Either) => ModuleFor src ss Either where
  86         moduleFor = ["Either"] `moduleWhere`
  87          [ "Left"   := teEither_Left
  88          , "Right"  := teEither_Right
  89          , "either" := teEither_either
  90          ]
  91
  92 -- ** 'Type's
  93 tyEither :: Source src => Type src vs l -> Type src vs r -> Type src vs (Either l r)
  94 tyEither l r = tyConstLen @(K Either) @Either (lenVars l) `tyApp` l `tyApp` r
  95
  96 -- ** 'Term's
  97 teEither_Left :: TermDef Either '[Proxy a, Proxy b] (() #> (a -> Either a b))
  98 teEither_Left = Term noConstraint (a0 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Left
  99 teEither_Right :: TermDef Either '[Proxy a, Proxy b] (() #> (b -> Either a b))
 100 teEither_Right = Term noConstraint (b1 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Right
 101 teEither_either :: TermDef Either '[Proxy a, Proxy b, Proxy c] (() #> ((a -> c) -> (b -> c) -> Either a b -> c))
 102 teEither_either = Term noConstraint ((a0 ~> c2) ~> (b1 ~> c2) ~> tyEither a0 b1 ~> c2) $ teSym @Either $ lam3 either