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