Language/Symantic/Expr/Traversable.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE Rank2Types #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE TypeOperators #-}
  10 {-# LANGUAGE UndecidableInstances #-}
  11 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 -- | Expression for 'Traversable'.
  13 module Language.Symantic.Expr.Traversable where
  14
  15 import Data.Traversable (Traversable)
  16 import Data.Proxy (Proxy(..))
  17 import Data.Type.Equality ((:~:)(Refl))
  18 import Prelude hiding (Traversable(..))
  19
  20 import Language.Symantic.Type
  21 import Language.Symantic.Trans.Common
  22 import Language.Symantic.Expr.Root
  23 import Language.Symantic.Expr.Error
  24 import Language.Symantic.Expr.From
  25 import Language.Symantic.Expr.Lambda
  26 import Language.Symantic.Expr.Applicative
  27
  28 -- * Class 'Sym_Traversable'
  29 -- | Symantic.
  30 class Sym_Applicative repr => Sym_Traversable repr where
  31         traverse :: (Traversable t, Applicative f)
  32          => repr ((->) a (f b)) -> repr (t a) -> repr (f (t b))
  33         default traverse :: (Trans tr repr, Traversable t, Applicative f)
  34          => tr repr ((->) a (f b)) -> tr repr (t a) -> tr repr (f (t b))
  35         traverse = trans_map2 traverse
  36
  37 -- * Type 'Expr_Traversable'
  38 -- | Expression.
  39 data Expr_Traversable (root:: *)
  40 type instance Root_of_Expr      (Expr_Traversable root)      = root
  41 type instance Type_of_Expr      (Expr_Traversable root)      = No_Type
  42 type instance Sym_of_Expr       (Expr_Traversable root) repr = (Sym_Traversable repr)
  43 type instance Error_of_Expr ast (Expr_Traversable root)      = No_Error_Expr
  44
  45 traverse_from
  46  :: forall root ty ast hs ret.
  47  ( ty ~ Type_Root_of_Expr (Expr_Traversable root)
  48  , Eq_Type ty
  49  , Eq_Type1 ty
  50  , Expr_from ast root
  51  , Lift_Type   Type_Fun (Type_of_Expr root)
  52  , Unlift_Type Type_Fun (Type_of_Expr root)
  53  , Unlift_Type1 (Type_of_Expr root)
  54  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  55                    (Error_of_Expr ast root)
  56  , Root_of_Expr root ~ root
  57  , Constraint_Type1 Applicative ty
  58  , Constraint_Type1 Traversable ty
  59  ) => ast -> ast
  60  -> Expr_From ast (Expr_Traversable root) hs ret
  61 traverse_from ast_g ast_ta ex ast ctx k =
  62  -- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
  63         expr_from (Proxy::Proxy root) ast_g ctx $
  64          \(ty_g::ty h_g) (Forall_Repr_with_Context g) ->
  65         expr_from (Proxy::Proxy root) ast_ta ctx $
  66          \ty_ta (Forall_Repr_with_Context ta) ->
  67
  68         check_type_fun ex ast ty_g $ \(Type_Type2 Proxy ty_g_a ty_g_fb
  69          :: Type_Fun ty h_g) ->
  70
  71         check_type1 ex ast ty_g_fb $ \(Type_Type1 f ty_g_fb_b, Lift_Type1 ty_f) ->
  72         check_type1 ex ast ty_ta $ \(Type_Type1 t ty_ta_a, Lift_Type1 ty_t) ->
  73
  74         check_constraint_type1 ex (Proxy::Proxy Applicative) ast ty_g_fb $ \Dict ->
  75         check_constraint_type1 ex (Proxy::Proxy Traversable) ast ty_ta $ \Dict ->
  76
  77         check_eq_type ex ast ty_g_a ty_ta_a $ \Refl ->
  78
  79         k (
  80                 Type_Root $ ty_f $ Type_Type1 f $
  81                 Type_Root $ ty_t $ Type_Type1 t ty_g_fb_b
  82          ) $ Forall_Repr_with_Context $
  83          \c -> traverse (g c) (ta c)