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
  31  ( Sym_Applicative repr
  32  , Sym_Applicative_Lam lam repr
  33  ) => Sym_Traversable lam repr where
  34         traverse :: (Traversable t, Applicative f) => repr (Lambda lam a (f b)) -> repr (t a) -> repr (f (t b))
  35         default traverse :: (Trans tr repr, Traversable t, Applicative f)
  36          => tr repr (Lambda lam a (f b)) -> tr repr (t a) -> tr repr (f (t b))
  37         traverse = trans_map2 traverse
  38
  39 -- * Type 'Expr_Traversable'
  40 -- | Expression.
  41 data Expr_Traversable (lam:: * -> *) (root:: *)
  42 type instance Root_of_Expr      (Expr_Traversable lam root)      = root
  43 type instance Type_of_Expr      (Expr_Traversable lam root)      = No_Type
  44 type instance Sym_of_Expr       (Expr_Traversable lam root) repr = (Sym_Traversable lam repr)
  45 type instance Error_of_Expr ast (Expr_Traversable lam root)      = No_Error_Expr
  46 instance Constraint_Type1 Traversable (Type_Type0 px root)
  47 instance Constraint_Type1 Traversable (Type_Var1 root)
  48
  49 traverse_from
  50  :: forall root ty lam ast hs ret.
  51  ( ty ~ Type_Root_of_Expr (Expr_Traversable lam root)
  52  , Eq_Type (Type_Root_of_Expr root)
  53  , Eq_Type1 (Type_Root_of_Expr root)
  54  , Expr_from ast root
  55  , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
  56  , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
  57  , Unlift_Type1 (Type_of_Expr root)
  58  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
  59                    (Error_of_Expr ast root)
  60  , Root_of_Expr root ~ root
  61  , Constraint_Type1 Applicative ty
  62  , Constraint_Type1 Traversable ty
  63  ) => ast -> ast
  64  -> Expr_From ast (Expr_Traversable lam root) hs ret
  65 traverse_from ast_g ast_ta ex ast ctx k =
  66  -- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
  67         expr_from (Proxy::Proxy root) ast_g ctx $
  68          \(ty_g::Type_Root_of_Expr root h_g) (Forall_Repr_with_Context g) ->
  69         expr_from (Proxy::Proxy root) ast_ta ctx $
  70          \ty_ta (Forall_Repr_with_Context ta) ->
  71
  72         check_type_fun ex ast ty_g $ \(Type_Type2 Proxy ty_g_a ty_g_fb
  73          :: Type_Fun lam (Type_Root_of_Expr root) h_g) ->
  74
  75         check_type1 ex ast ty_g_fb $ \(Type_Type1 f ty_g_fb_b, Lift_Type1 ty_f) ->
  76         check_type1 ex ast ty_ta $ \(Type_Type1 t ty_ta_a, Lift_Type1 ty_t) ->
  77
  78         check_constraint_type1 ex (Proxy::Proxy Applicative) ast ty_g_fb $ \Dict ->
  79         check_constraint_type1 ex (Proxy::Proxy Traversable) ast ty_ta $ \Dict ->
  80
  81         check_eq_type ex ast ty_g_a ty_ta_a $ \Refl ->
  82
  83         k (
  84                 Type_Root $ ty_f $ Type_Type1 f $
  85                 Type_Root $ ty_t $ Type_Type1 t ty_g_fb_b
  86          ) $ Forall_Repr_with_Context $
  87          \c -> traverse (g c) (ta c)