Language/Symantic/Expr/Traversable.hs

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