Language/Symantic/Expr/Functor.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE MultiParamTypeClasses #-}
   7 {-# LANGUAGE OverloadedStrings #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 -- | Expression for 'Functor'.
  13 module Language.Symantic.Expr.Functor where
  14
  15 import Control.Monad (liftM2)
  16 import Data.Proxy (Proxy(..))
  17 import Data.Type.Equality ((:~:)(Refl))
  18 import Prelude hiding (fmap, (<$))
  19 import qualified Data.Function as Fun
  20 import qualified Data.Functor as Functor
  21
  22 import Language.Symantic.Type
  23 import Language.Symantic.Repr
  24 import Language.Symantic.Expr.Root
  25 import Language.Symantic.Expr.Error
  26 import Language.Symantic.Expr.From
  27 import Language.Symantic.Expr.Lambda
  28 import Language.Symantic.Trans.Common
  29
  30 -- * Class 'Sym_Functor'
  31 -- | Symantic.
  32 class Sym_Lambda repr => Sym_Functor repr where
  33         fmap :: Functor f => repr (a -> b) -> repr (f a) -> repr (f b)
  34         default fmap
  35          :: (Trans t repr, Functor f)
  36          => t repr (a -> b)
  37          -> t repr (f a)
  38          -> t repr (f b)
  39         fmap = trans_map2 fmap
  40
  41         (<$) :: Functor f => repr a -> repr (f b) -> repr (f a)
  42         (<$) a = fmap (lam (Fun.const a))
  43
  44 infixl 4 <$
  45
  46 instance Sym_Functor Repr_Host where
  47         fmap = liftM2 Functor.fmap
  48         (<$) = liftM2 (Functor.<$)
  49 instance Sym_Functor Repr_Text where
  50         fmap = repr_text_app2 "fmap"
  51         (<$) = repr_text_infix "<$" (Precedence 4)
  52 instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (Repr_Dup r1 r2) where
  53         fmap = repr_dup2 sym_Functor fmap
  54         (<$) = repr_dup2 sym_Functor (<$)
  55
  56 sym_Functor :: Proxy Sym_Functor
  57 sym_Functor = Proxy
  58
  59 -- | 'fmap' alias.
  60 (<$>) :: (Sym_Functor repr, Functor f)
  61  => repr (a -> b) -> repr (f a) -> repr (f b)
  62 (<$>) = fmap
  63 infixl 4 <$>
  64
  65 -- * Type 'Expr_Functor'
  66 -- | Expression.
  67 data Expr_Functor (root:: *)
  68 type instance Root_of_Expr      (Expr_Functor root)      = root
  69 type instance Type_of_Expr      (Expr_Functor root)      = No_Type
  70 type instance Sym_of_Expr       (Expr_Functor root) repr = (Sym_Functor repr)
  71 type instance Error_of_Expr ast (Expr_Functor root)      = No_Error_Expr
  72
  73 -- | Parse 'fmap'.
  74 fmap_from
  75  :: forall root ty ast hs ret.
  76  ( ty ~ Type_Root_of_Expr (Expr_Functor root)
  77  , Expr_From ast root
  78  , Type0_Eq ty
  79  , Type0_Lift   Type_Fun (Type_of_Expr root)
  80  , Type0_Unlift Type_Fun (Type_of_Expr root)
  81  , Type1_Unlift (Type_of_Expr root)
  82  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  83                    (Error_of_Expr ast root)
  84  , Root_of_Expr root ~ root
  85  , Type1_Constraint Functor ty
  86  ) => ast -> ast
  87  -> ExprFrom ast (Expr_Functor root) hs ret
  88 fmap_from ast_g ast_fa ex ast ctx k =
  89  -- fmap :: Functor f => (a -> b) -> f a -> f b
  90         expr_from (Proxy::Proxy root) ast_g ctx $
  91          \(ty_g::ty h_g) (Forall_Repr_with_Context g) ->
  92         expr_from (Proxy::Proxy root) ast_fa ctx $
  93          \(ty_fa::ty h_fa) (Forall_Repr_with_Context fa) ->
  94         check_type_fun ex ast ty_g $ \(Type2 Proxy ty_g_a ty_g_b) ->
  95         check_type1 ex ast ty_fa $ \(Type1 f ty_fa_a, Type1_Lift f_lift) ->
  96         check_type1_constraint ex (Proxy::Proxy Functor) ast ty_fa $ \Dict ->
  97         check_type0_eq ex ast ty_g_a ty_fa_a $ \Refl ->
  98         k (Type_Root $ f_lift $ Type1 f ty_g_b) $ Forall_Repr_with_Context $
  99          \c -> fmap (g c) (fa c)