]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Functor.hs
init
[haskell/symantic.git] / 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 -- * Class 'Sym_Functor'
25 -- | Symantic.
26 class Sym_Functor lam repr where
27 fmap
28 :: Functor_with_Lambda f
29 => repr (Lambda lam a b)
30 -> repr (f a)
31 -> repr (f b)
32
33 default fmap
34 :: (Trans t repr, Functor_with_Lambda f)
35 => t repr (Lambda lam a b)
36 -> t repr (f a)
37 -> t repr (f b)
38 fmap = trans_map2 fmap
39
40 -- | Convenient alias.
41 (<$>) ::
42 ( Sym_Functor lam repr
43 , Functor_with_Lambda f )
44 => repr (Lambda lam a b)
45 -> repr (f a)
46 -> repr (f b)
47 (<$>) = fmap
48 infixl 4 <$>
49
50 -- ** Class 'Functor_with_Lambda'
51 -- | A class alias to add 'Traversable' to 'Functor'.
52 --
53 -- NOTE: 'Traversable' is required by the 'Repr_Host' instance (which uses 'sequence').
54 -- Imposing this 'Traversable' class to mere 'Functor's is annoying
55 -- because obviously not all data types have both
56 -- an instance of 'Functor' and 'Traversable',
57 -- but I cannot see another way to do when supporting 'val' and 'lazy' 'Lambda's
58 -- whose @lam@ wrapping has to be extracted from @f (lam a)@ to @lam (f a)@,
59 -- which is exactly which is done by @sequence :: (Traversable t, Monad m) => t (m a) -> m (t a)@.
60 class (Functor f, Traversable f) => Functor_with_Lambda f
61 instance (Functor f, Traversable f) => Functor_with_Lambda f
62 instance Constraint1_Type Functor_with_Lambda (Type_Fun lam root)
63 instance Constraint1_Type Functor_with_Lambda (Type_Bool root)
64 instance Constraint1_Type Functor_with_Lambda (Type_Int root)
65 instance Constraint1_Type Functor_with_Lambda (Type_Ordering root)
66 instance Constraint1_Type Functor_with_Lambda (Type_Unit root)
67 instance Constraint1_Type Functor_with_Lambda (Type_Var 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 , Type_Lift (Type_Fun lam) (Type_of_Expr root)
85 , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
86 , Unlift_Type1 (Type_of_Expr root)
87 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
88 (Error_of_Expr ast root)
89 , Root_of_Expr root ~ root
90 , Constraint1_Type 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 $ \(ty_g_a `Type_Fun` 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, Type_Lift1 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)