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 (Proxy 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 FixityOf Either
  48 instance ClassInstancesFor Either where
  49         proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _l))
  50          | Just HRefl <- proj_ConstKiTy @_ @Either c
  51          = case () of
  52                  _ | Just Refl <- proj_Const @Functor     q -> Just Dict
  53                    | Just Refl <- proj_Const @Applicative q -> Just Dict
  54                    | Just Refl <- proj_Const @Monad       q -> Just Dict
  55                    | Just Refl <- proj_Const @Foldable    q -> Just Dict
  56                    | Just Refl <- proj_Const @Traversable q -> Just Dict
  57                  _ -> Nothing
  58         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c l) r))
  59          | Just HRefl <- proj_ConstKiTy @_ @Either c
  60          = case () of
  61                  _ | Just Refl <- proj_Const @Eq q
  62                    , Just Dict <- proveConstraint (tq `tyApp` l)
  63                    , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
  64                    | Just Refl <- proj_Const @Ord q
  65                    , Just Dict <- proveConstraint (tq `tyApp` l)
  66                    , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
  67                    | Just Refl <- proj_Const @Show q
  68                    , Just Dict <- proveConstraint (tq `tyApp` l)
  69                    , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict
  70                    | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
  71                    | Just Refl <- proj_Const @MT.MonoFunctor  q -> Just Dict
  72                  _ -> Nothing
  73         proveConstraintFor _c _q = Nothing
  74 instance TypeInstancesFor Either where
  75         expandFamFor _c _len f (TyApp _ (TyApp _ c _ty_l) r `TypesS` TypesZ)
  76          | Just HRefl <- proj_ConstKi @_ @Element f
  77          , Just HRefl <- proj_ConstKiTy @_ @Either c
  78          = Just r
  79         expandFamFor _c _len _fam _as = Nothing
  80
  81 -- Compiling
  82 instance Gram_Term_AtomsFor src ss g Either
  83 instance (Source src, Inj_Sym ss Either) => ModuleFor src ss Either where
  84         moduleFor = ["Either"] `moduleWhere`
  85          [ "Left"   := teEither_Left
  86          , "Right"  := teEither_Right
  87          , "either" := teEither_either
  88          ]
  89
  90 -- ** 'Type's
  91 tyEither :: Source src => Type src vs l -> Type src vs r -> Type src vs (Either l r)
  92 tyEither l r = tyConstLen @(K Either) @Either (lenVars l) `tyApp` l `tyApp` r
  93
  94 -- ** 'Term's
  95 teEither_Left :: TermDef Either '[Proxy a, Proxy b] (() #> (a -> Either a b))
  96 teEither_Left = Term noConstraint (a0 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Left
  97 teEither_Right :: TermDef Either '[Proxy a, Proxy b] (() #> (b -> Either a b))
  98 teEither_Right = Term noConstraint (b1 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Right
  99 teEither_either :: TermDef Either '[Proxy a, Proxy b, Proxy c] (() #> ((a -> c) -> (b -> c) -> Either a b -> c))
 100 teEither_either = Term noConstraint ((a0 ~> c2) ~> (b1 ~> c2) ~> tyEither a0 b1 ~> c2) $ teSym @Either $ lam3 either