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 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fno-warn-orphans #-}
  13 -- | Expression for 'Functor'.
  14 module Language.Symantic.Expr.Functor where
  15
  16 import Control.Monad (liftM2)
  17 import Data.Proxy (Proxy(..))
  18 import Data.Type.Equality ((:~:)(Refl))
  19 import Prelude hiding (fmap)
  20 import qualified Data.Function as Fun
  21 import qualified Data.Functor as Functor
  22
  23 import Language.Symantic.Type
  24 import Language.Symantic.Repr
  25 import Language.Symantic.Expr.Root
  26 import Language.Symantic.Expr.Error
  27 import Language.Symantic.Expr.From
  28 import Language.Symantic.Expr.Lambda
  29 import Language.Symantic.Trans.Common
  30
  31 -- * Class 'Sym_Functor'
  32 -- | Symantic.
  33 class Sym_Lambda repr => Sym_Functor repr where
  34         fmap :: Functor f => repr ((->) a b) -> repr (f a) -> repr (f b)
  35         default fmap
  36          :: (Trans t repr, Functor f)
  37          => t repr ((->) a b)
  38          -> t repr (f a)
  39          -> t repr (f b)
  40         fmap = trans_map2 fmap
  41
  42         (<$) :: Functor f => repr a -> repr (f b) -> repr (f a)
  43         (<$) a = fmap (lam (Fun.const a))
  44 infixl 4 <$
  45 instance Sym_Functor Repr_Host where
  46         fmap = liftM2 (Functor.<$>)
  47 instance Sym_Functor Repr_Text where
  48         fmap = repr_text_app2 "fmap"
  49 instance
  50  ( Sym_Functor r1
  51  , Sym_Functor r2
  52  ) => Sym_Functor (Dup r1 r2) where
  53         fmap (f1 `Dup` f2) (m1 `Dup` m2) =
  54                 fmap f1 m1 `Dup` fmap f2 m2
  55
  56 -- | 'fmap' alias.
  57 (<$>) :: (Sym_Functor repr, Functor f)
  58  => repr ((->) a b) -> repr (f a) -> repr (f b)
  59 (<$>) = fmap
  60 infixl 4 <$>
  61
  62 -- * Type 'Expr_Functor'
  63 -- | Expression.
  64 data Expr_Functor (root:: *)
  65 type instance Root_of_Expr      (Expr_Functor root)      = root
  66 type instance Type_of_Expr      (Expr_Functor root)      = No_Type
  67 type instance Sym_of_Expr       (Expr_Functor root) repr = (Sym_Functor repr)
  68 type instance Error_of_Expr ast (Expr_Functor root)      = No_Error_Expr
  69
  70 -- | Parse 'fmap'.
  71 fmap_from
  72  :: forall root ty ast hs ret.
  73  ( ty ~ Type_Root_of_Expr (Expr_Functor root)
  74  , Eq_Type ty
  75  , Expr_from ast root
  76  , Lift_Type   Type_Fun (Type_of_Expr root)
  77  , Unlift_Type Type_Fun (Type_of_Expr root)
  78  , Unlift_Type1 (Type_of_Expr root)
  79  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  80                    (Error_of_Expr ast root)
  81  , Root_of_Expr root ~ root
  82  , Constraint_Type1 Functor ty
  83  ) => ast -> ast
  84  -> Expr_From ast (Expr_Functor root) hs ret
  85 fmap_from ast_g ast_fa ex ast ctx k =
  86  -- NOTE: fmap :: Functor f => (a -> b) -> f a -> f b
  87         expr_from (Proxy::Proxy root) ast_g ctx $
  88          \(ty_g::ty h_g) (Forall_Repr_with_Context g) ->
  89         expr_from (Proxy::Proxy root) ast_fa ctx $
  90          \(ty_fa::ty h_fa) (Forall_Repr_with_Context fa) ->
  91         check_type_fun ex ast ty_g $ \(Type_Type2 Proxy ty_g_a ty_g_b
  92          :: Type_Fun ty h_g) ->
  93         check_type1 ex ast ty_fa $ \(Type_Type1 f ty_fa_a, Lift_Type1 f_lift) ->
  94         check_constraint_type1 ex (Proxy::Proxy Functor) ast ty_fa $ \Dict ->
  95         check_eq_type ex ast ty_g_a ty_fa_a $ \Refl ->
  96         k (Type_Root $ f_lift $ Type_Type1 f ty_g_b) $ Forall_Repr_with_Context $
  97          \c -> fmap (g c) (fa c)