TFHOE/Expr/Fun.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 -- {-# LANGUAGE FunctionalDependencies #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE NoImplicitPrelude #-}
   7 {-# LANGUAGE OverloadedStrings #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 module TFHOE.Expr.Fun where
  13
  14 import Data.Either (Either(..))
  15 import Data.Eq (Eq(..))
  16 import Data.Function (($))
  17 -- import Data.Functor.Identity (Identity)
  18 import Data.Maybe (Maybe(..))
  19 -- import Data.Monoid ((<>))
  20 import Data.Proxy (Proxy(..))
  21 -- import Data.Proxy (Proxy(..))
  22 -- import Data.String (String)
  23 import Data.Type.Equality ((:~:)(Refl))
  24 -- import Data.Type.Equality ((:~:)(Refl))
  25 -- import Text.Show (Show(..))
  26
  27 import TFHOE.Raw
  28 import TFHOE.Type
  29 import TFHOE.Expr.Common
  30 import TFHOE.Repr.Dup
  31
  32 -- * Class 'Expr_Fun'
  33
  34 -- | /Tagless-final symantics/ for /lambda abstraction/
  35 -- in /higher-order abstract syntax/ (HOAS),
  36 -- and with argument @arg@ and result @res@ of 'Fun'
  37 -- wrapped inside 'fun': to control the calling
  38 -- in the 'Repr_Host' instance.
  39 class (fun ~ Fun_from_Repr repr) => Expr_Fun fun repr where
  40         -- | This type constructor is used like
  41         -- the functional dependency: @repr -> fun@
  42         -- (ie. knowing @repr@ one can determine @fun@)
  43         -- in order to avoid to introduce a 'Proxy' @fun@
  44         -- in 'let_inline', 'let_val' and 'let_lazy'.
  45         --
  46         -- Distinguishing between @fun@ and @repr@ is used to maintain
  47         -- the universal polymorphism of @repr@ in 'Expr_from',
  48         -- the downside with this however is that
  49         -- to be an instance of 'Expr_Fun' for all @fun@,
  50         -- the @repr@ type of an interpreter
  51         -- has to be parameterized by @fun@,
  52         -- even though it does not actually need @fun@ to do its work.
  53         --
  54         -- Basically this means having sometimes to add a type annotation
  55         -- to the interpreter call to specify @fun@.
  56         type Fun_from_Repr repr :: {-fun-}(* -> *)
  57
  58         -- | Lambda application.
  59         app :: repr (Fun fun arg res) -> repr arg -> repr res
  60
  61         -- | /Call-by-name/ lambda.
  62         inline :: (repr arg -> repr res) -> repr (Fun fun arg res)
  63         -- | /Call-by-value/ lambda.
  64         val    :: (repr arg -> repr res) -> repr (Fun fun arg res)
  65         -- | /Call-by-need/ lambda (aka. /lazyness/): lazy shares its argument, no matter what.
  66         lazy   :: (repr arg -> repr res) -> repr (Fun fun arg res)
  67
  68         -- | Convenient 'inline' wrapper.
  69         let_inline
  70          :: Expr_Fun fun repr
  71          => repr arg -> (repr arg -> repr res) -> repr res
  72         let_inline x y = inline y `app` x
  73         -- | Convenient 'val' wrapper.
  74         let_val
  75          :: Expr_Fun fun repr
  76          => repr arg -> (repr arg -> repr res) -> repr res
  77         let_val x y = val y `app` x
  78         -- | Convenient 'lazy' wrapper.
  79         let_lazy
  80          :: Expr_Fun fun repr
  81          => repr arg -> (repr arg -> repr res) -> repr res
  82         let_lazy x y = lazy y `app` x
  83
  84 infixl 5 `app`
  85
  86 type instance Expr_from_Type (Type_Fun fun next) repr
  87  = ( Expr_Fun fun repr
  88    , Expr_from_Type next repr )
  89
  90 instance -- Expr_Fun Dup
  91  ( Expr_Fun fun r1
  92  , Expr_Fun fun r2
  93  ) => Expr_Fun fun (Dup r1 r2) where
  94         type Fun_from_Repr (Dup r1 r2) = Fun_from_Repr r1
  95         app (f1 `Dup` f2) (x1 `Dup` x2) = app f1 x1 `Dup` app f2 x2
  96         inline f = dup1 (inline f) `Dup` dup2 (inline f)
  97         val    f = dup1 (val f)    `Dup` dup2 (val f)
  98         lazy   f = dup1 (lazy f)   `Dup` dup2 (lazy f)
  99 instance -- Expr_from Raw Type_Fun Type_Fun
 100  ( Type_from Raw next
 101  , Expr_from Raw next (Type_Fun fun next)
 102  ) => Expr_from Raw (Type_Fun fun next) (Type_Fun fun next) where
 103         expr_from _px_ty _px_ty_end ctx (Raw "var" [Raw name []]) k =
 104                 go ctx k
 105                 where
 106                 go :: forall hs ret.
 107                  Context (Var (Type_Fun fun next)) hs
 108                  -> (forall h. Type_Fun fun next h
 109                   -> Forall_Repr_with_Context (Type_Fun fun next) hs h
 110                   -> Either Error_Type ret)
 111                  -> Either Error_Type ret
 112                 go c k' =
 113                         case c of
 114                          Context_Empty -> Left "Error: var: unbound variable"
 115                          Var n ty `Context_Next` _ | n == name ->
 116                                 k' ty $ Forall_Repr_with_Context $
 117                                  \(repr `Context_Next` _) -> repr
 118                          _ `Context_Next` ctx' ->
 119                                 go ctx' $ \ty (Forall_Repr_with_Context repr) ->
 120                                         k' ty $ Forall_Repr_with_Context $
 121                                          \(_ `Context_Next` c') -> repr c'
 122         expr_from _px_ty px_ty_end ctx (Raw "app" [raw_lam, raw_val]) k =
 123                 expr_from px_ty_end px_ty_end ctx raw_lam $ \ty_lam (Forall_Repr_with_Context lam) ->
 124                 expr_from px_ty_end px_ty_end ctx raw_val $ \ty_val (Forall_Repr_with_Context val_) ->
 125                         case ty_lam of
 126                          ty_arg `Type_Fun` ty_res
 127                           | Just Refl <- ty_arg `type_eq` ty_val ->
 128                                 k ty_res $ Forall_Repr_with_Context $
 129                                  \c -> lam c `app` val_ c
 130                          _ -> Left "Error: app: bad lambda application"
 131         expr_from _px_ty px_ty_end ctx (Raw "inline" [Raw name [], raw_ty_arg, raw_body]) k =
 132                 type_from raw_ty_arg $ \ty_arg ->
 133                         expr_from px_ty_end px_ty_end (Var name ty_arg `Context_Next` ctx) raw_body $
 134                          \ty_res (Forall_Repr_with_Context res) ->
 135                                 k (ty_arg `Type_Fun` ty_res) $ Forall_Repr_with_Context $
 136                                  \c -> inline $ \arg -> res (arg `Context_Next` c)
 137         expr_from _px_ty px_ty_end ctx (Raw "val" [Raw name [], raw_ty_arg, raw_body]) k =
 138                 type_from raw_ty_arg $ \ty_arg ->
 139                         expr_from px_ty_end px_ty_end (Var name ty_arg `Context_Next` ctx) raw_body $
 140                          \ty_res (Forall_Repr_with_Context res) ->
 141                                 k (ty_arg `Type_Fun` ty_res) $ Forall_Repr_with_Context $
 142                                  \c -> val $ \arg -> res (arg `Context_Next` c)
 143         expr_from _px_ty px_ty_end ctx (Raw "lazy" [Raw name [], raw_ty_arg, raw_body]) k =
 144                 type_from raw_ty_arg $ \ty_arg ->
 145                         expr_from px_ty_end px_ty_end (Var name ty_arg `Context_Next` ctx) raw_body $
 146                          \ty_res (Forall_Repr_with_Context res) ->
 147                                 k (ty_arg `Type_Fun` ty_res) $ Forall_Repr_with_Context $
 148                                  \c -> lazy $ \arg -> res (arg `Context_Next` c)
 149         expr_from _px_ty px_ty_end ctx raw k =
 150                 expr_from (Proxy::Proxy next) px_ty_end ctx raw k