Language/Symantic/Compiling/Functor.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE NoMonomorphismRestriction #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 {-# OPTIONS_GHC -fno-warn-orphans #-}
  14 -- | Symantic for 'Functor'.
  15 module Language.Symantic.Compiling.Functor where
  16
  17 import Control.Monad (liftM2)
  18 import qualified Data.Function as Fun
  19 import Data.Functor (Functor)
  20 import qualified Data.Functor as Functor
  21 import Data.Proxy (Proxy(..))
  22 import Data.String (IsString)
  23 import Data.Text (Text)
  24 import Data.Type.Equality
  25 import Prelude hiding (Functor(..))
  26
  27 import Language.Symantic.Typing
  28 import Language.Symantic.Compiling.Term
  29 import Language.Symantic.Interpreting
  30 import Language.Symantic.Transforming.Trans
  31
  32 -- * Class 'Sym_Functor'
  33 class Sym_Lambda term => Sym_Functor term where
  34         fmap :: Functor f => term (a -> b) -> term (f a) -> term (f b)
  35         default fmap
  36          :: (Trans t term, Functor f)
  37          => t term (a -> b)
  38          -> t term (f a)
  39          -> t term (f b)
  40         fmap = trans_map2 fmap
  41
  42         (<$) :: Functor f => term a -> term (f b) -> term (f a)
  43         (<$) a = fmap (lam (Fun.const a))
  44
  45 infixl 4 <$
  46
  47 type instance Sym_of_Iface (Proxy Functor) = Sym_Functor
  48 type instance Consts_of_Iface (Proxy Functor) = Proxy Functor ': Consts_imported_by Functor
  49 type instance Consts_imported_by Functor = '[]
  50
  51 instance Sym_Functor HostI where
  52         fmap = liftM2 Functor.fmap
  53         (<$) = liftM2 (Functor.<$)
  54 instance Sym_Functor TextI where
  55         fmap = textI_app2 "fmap"
  56         (<$) = textI_infix "<$" (Precedence 4)
  57 instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (DupI r1 r2) where
  58         fmap = dupI2 sym_Functor fmap
  59         (<$) = dupI2 sym_Functor (<$)
  60
  61 -- | 'fmap' alias.
  62 (<$>) :: (Sym_Functor term, Functor f)
  63  => term (a -> b) -> term (f a) -> term (f b)
  64 (<$>) = fmap
  65 infixl 4 <$>
  66
  67 instance Const_from Text cs => Const_from Text (Proxy Functor ': cs) where
  68         const_from "Functor" k = k (ConstZ kind)
  69         const_from s k = const_from s $ k . ConstS
  70 instance Show_Const cs => Show_Const (Proxy Functor ': cs) where
  71         show_const ConstZ{} = "Functor"
  72         show_const (ConstS c) = show_const c
  73
  74 instance -- Proj_ConC
  75  Proj_ConC cs (Proxy Functor)
  76 instance -- Term_fromI
  77  ( AST ast
  78  , Lexem ast ~ LamVarName
  79  , Inj_Const  (Consts_of_Ifaces is) Functor
  80  , Inj_Const  (Consts_of_Ifaces is) (->)
  81  , Proj_Con   (Consts_of_Ifaces is)
  82  , Term_from is ast
  83  ) => Term_fromI is (Proxy Functor) ast where
  84         term_fromI ast ctx k =
  85                 case ast_lexem ast of
  86                  "fmap" -> fmap_from
  87                  "<$>"  -> fmap_from
  88                  "<$"   -> ltdollar_from
  89                  _ -> Left $ Error_Term_unsupported
  90                 where
  91                 fmap_from =
  92                  -- fmap :: Functor f => (a -> b) -> f a -> f b
  93                         from_ast2 ast $ \ast_a2b ast_fa as ->
  94                         term_from ast_a2b ctx $ \ty_a2b (TermLC a2b) ->
  95                         term_from ast_fa  ctx $ \ty_fa  (TermLC fa) ->
  96                         check_type2 tyFun ast_a2b ty_a2b $ \Refl ty_a2b_a ty_a2b_b ->
  97                         check_constraint1 tyFunctor ast_fa ty_fa $ \Refl Con ty_fa_f ty_fa_a ->
  98                         check_type (At (Just ast_a2b) ty_a2b_a) (At (Just ast_fa) ty_fa_a) $ \Refl ->
  99                         k as (ty_fa_f :$ ty_a2b_b) $ TermLC $
 100                          \c -> fmap (a2b c) (fa c)
 101                 ltdollar_from =
 102                  -- (<$) :: Functor f => a -> f b -> f a
 103                         from_ast2 ast $ \ast_a ast_fb as ->
 104                         term_from ast_a  ctx $ \ty_a  (TermLC a) ->
 105                         term_from ast_fb ctx $ \ty_fb (TermLC fb) ->
 106                         check_constraint1 tyFunctor ast_fb ty_fb $ \Refl Con ty_fb_f _ty_fb_b ->
 107                         k as (ty_fb_f :$ ty_a) $ TermLC $
 108                          \c -> (<$) (a c) (fb c)
 109
 110 -- | The 'Functor' 'Type'
 111 tyFunctor :: Inj_Const cs Functor => Type cs Functor
 112 tyFunctor = TyConst inj_const
 113
 114 sym_Functor :: Proxy Sym_Functor
 115 sym_Functor = Proxy
 116
 117 syFunctor :: IsString a => [Syntax a] -> Syntax a
 118 syFunctor = Syntax "Functor"