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 -- | Expression for 'Functor'.
  12 module Language.Symantic.Expr.Functor where
  13
  14 import Data.Proxy (Proxy(..))
  15 import Data.Type.Equality ((:~:)(Refl))
  16 import Prelude hiding (fmap)
  17
  18 import Language.Symantic.Type
  19 import Language.Symantic.Trans.Common
  20 import Language.Symantic.Expr.Common
  21 import Language.Symantic.Expr.Lambda
  22
  23 -- * Class 'Sym_Functor'
  24 -- | Symantic.
  25 class Sym_Functor lam repr where
  26         fmap
  27          :: Functor_with_Lambda f
  28          => repr (Lambda lam a b)
  29          -> repr (f a)
  30          -> repr (f b)
  31
  32         default fmap
  33          :: (Trans t repr, Functor_with_Lambda f)
  34          => t repr (Lambda lam a b)
  35          -> t repr (f a)
  36          -> t repr (f b)
  37         fmap = trans_map2 fmap
  38
  39 -- | Convenient alias.
  40 (<$>) ::
  41  ( Sym_Functor lam repr
  42  , Functor_with_Lambda f )
  43  => repr (Lambda lam a b)
  44  -> repr (f a)
  45  -> repr (f b)
  46 (<$>) = fmap
  47 infixl 4 <$>
  48
  49 -- ** Class 'Functor_with_Lambda'
  50 -- | A class alias to add 'Traversable' to 'Functor'.
  51 --
  52 -- NOTE: 'Traversable' is required by the 'Repr_Host' instance (which uses 'sequence').
  53 -- Imposing this 'Traversable' class to mere 'Functor's is annoying
  54 -- because obviously not all data types have both
  55 -- an instance of 'Functor' and 'Traversable',
  56 -- but I cannot see another way to do when supporting 'val' and 'lazy' 'Lambda's
  57 -- whose @lam@ wrapping has to be extracted from @f (lam a)@ to @lam (f a)@,
  58 -- which is exactly which is done by @sequence :: (Traversable t, Monad m) => t (m a) -> m (t a)@.
  59 class    (Functor f, Traversable f) => Functor_with_Lambda f
  60 instance (Functor f, Traversable f) => Functor_with_Lambda f
  61 instance Constraint_Type1 Functor_with_Lambda (Type_Fun lam  root)
  62 instance Constraint_Type1 Functor_with_Lambda (Type_Bool     root)
  63 instance Constraint_Type1 Functor_with_Lambda (Type_Int      root)
  64 instance Constraint_Type1 Functor_with_Lambda (Type_Ordering root)
  65 instance Constraint_Type1 Functor_with_Lambda (Type_Unit     root)
  66 instance Constraint_Type1 Functor_with_Lambda (Type_Var0     root)
  67 instance Constraint_Type1 Functor_with_Lambda (Type_Var1     root)
  68
  69 -- * Type 'Expr_Functor'
  70 -- | Expression.
  71 data Expr_Functor (lam:: * -> *) (root:: *)
  72 type instance Root_of_Expr      (Expr_Functor lam root)      = root
  73 type instance Type_of_Expr      (Expr_Functor lam root)      = No_Type
  74 type instance Sym_of_Expr       (Expr_Functor lam root) repr = (Sym_Functor lam repr)
  75 type instance Error_of_Expr ast (Expr_Functor lam root)      = No_Error_Expr
  76
  77 -- | Parse 'fmap'.
  78 fmap_from
  79  :: forall root ty lam ast hs ret.
  80  ( ty ~ Type_Root_of_Expr (Expr_Functor lam root)
  81  , String_from_Type ty
  82  , Eq_Type (Type_Root_of_Expr root)
  83  , Expr_from ast root
  84  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
  85  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
  86  , Unlift_Type1 (Type_of_Expr root)
  87  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  88                    (Error_of_Expr ast root)
  89  , Root_of_Expr root ~ root
  90  , Constraint_Type1 Functor_with_Lambda ty
  91  ) => ast -> ast
  92  -> Expr_From ast (Expr_Functor lam root) hs ret
  93 fmap_from ast_g ast_fa ex ast ctx k =
  94  -- NOTE: fmap :: Functor f => (a -> b) -> f a -> f b
  95         expr_from (Proxy::Proxy root) ast_g ctx $
  96          \(ty_g::Type_Root_of_Expr root h_g) (Forall_Repr_with_Context g) ->
  97         expr_from (Proxy::Proxy root) ast_fa ctx $
  98          \(ty_fa::Type_Root_of_Expr root h_fa) (Forall_Repr_with_Context fa) ->
  99         check_type_fun ex ast ty_g $ \(Type_Type2 Proxy ty_g_a ty_g_b
 100          :: Type_Fun lam (Type_Root_of_Expr root) h_g) ->
 101         check_type1 ex ast ty_fa $ \(Type_Type1 f ty_fa_a, Lift_Type1 f_lift) ->
 102         check_constraint1_type ex (Proxy::Proxy Functor_with_Lambda) ast ty_fa $ \Dict ->
 103         check_eq_type ex ast ty_g_a ty_fa_a $ \Refl ->
 104         k (Type_Root $ f_lift $ Type_Type1 f ty_g_b) $ Forall_Repr_with_Context $
 105          \c -> fmap (g c) (fa c)