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.Repr.Dup
  20 import Language.Symantic.Trans.Common
  21 import Language.Symantic.Expr.Common
  22 import Language.Symantic.Expr.Lambda
  23
  24 -- | A class alias to add 'Traversable' to 'Functor'.
  25 --
  26 -- NOTE: 'Traversable' is required by the 'Repr_Host' instance (which uses 'sequence').
  27 -- Imposing this 'Traversable' class to mere 'Functor's is annoying
  28 -- because obviously not all data types have both
  29 -- an instance of 'Functor' and 'Traversable',
  30 -- but I cannot see another way to do when supporting 'val' and 'lazy' 'Lambda's
  31 -- whose @lam@ wrapping has to be extracted from @f (lam a)@ to @lam (f a)@,
  32 -- which is exactly which is done by @sequence :: (Traversable t, Monad m) => t (m a) -> m (t a)@.
  33 class    (Functor f, Traversable f) => Functor_with_Lambda f
  34 instance (Functor f, Traversable f) => Functor_with_Lambda f
  35 instance Constraint1_Type Functor_with_Lambda (Type_Fun lam root)
  36 instance Constraint1_Type Functor_with_Lambda (Type_Bool root)
  37 instance Constraint1_Type Functor_with_Lambda (Type_Int  root)
  38 instance Constraint1_Type Functor_with_Lambda (Type_Var  root)
  39
  40 class Sym_Functor lam repr where
  41         fmap
  42          :: Functor_with_Lambda f
  43          => repr (Lambda lam a b)
  44          -> repr (f a)
  45          -> repr (f b)
  46
  47         default fmap
  48          :: (Trans t repr, Functor_with_Lambda f)
  49          => t repr (Lambda lam a b)
  50          -> t repr (f a)
  51          -> t repr (f b)
  52         fmap = trans_map2 fmap
  53
  54 -- * Type 'Expr_Functor'
  55 -- | Expression.
  56 data Expr_Functor (lam:: * -> *) (root:: *)
  57 type instance Root_of_Expr      (Expr_Functor lam root)      = root
  58 type instance Type_of_Expr      (Expr_Functor lam root)      = No_Type
  59 type instance Sym_of_Expr       (Expr_Functor lam root) repr = (Sym_Functor lam repr)
  60 type instance Error_of_Expr ast (Expr_Functor lam root)      = No_Error_Expr
  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  , Type_Lift   (Type_Fun lam) (Type_of_Expr root)
  69  , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
  70  , Type_Unlift1 (Type_of_Expr root)
  71  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  72                    (Error_of_Expr ast root)
  73  , Root_of_Expr root ~ root
  74  , Constraint1_Type Functor_with_Lambda 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 $ \(ty_g_a `Type_Fun` 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, Type_Lift1 f_lift) ->
  86         check_constraint1_type ex (Proxy::Proxy Functor_with_Lambda) 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)