Embedding a higher-order domain-specific language (simply-typed lambda-calculus with constants) with a selectable evaluation order: Call-by-value, call-by-name, call-by-need in the same Final Tagless framework
http://okmij.org/ftp/tagless-final/tagless-typed.html#call-by-any
- data IntT
- data a :-> b
- class EDSL exp where
- let_ :: EDSL exp => exp a -> (exp a -> exp b) -> exp b
- t :: EDSL exp => exp IntT
- type family Sem m a :: *
- newtype S l m a = S {}
- data Name
- runName :: S Name m a -> m (Sem m a)
- t1 :: EDSL exp => exp IntT
- t2 :: EDSL exp => exp IntT
- data Value
- vn :: S Value m x -> S Name m x
- nv :: S Name m x -> S Value m x
- runValue :: S Value m a -> m (Sem m a)
- share :: MonadIO m => m a -> m (m a)
- data Lazy
- ln :: S Lazy m x -> S Name m x
- nl :: S Name m x -> S Lazy m x
- runLazy :: S Lazy m a -> m (Sem m a)
Documentation
We could have used Haskell's type Int and the arrow -> constructor.
We would like to emphasize however that EDSL types need not be identical
to the host language types. To give the type system to EDSL, we merely
need labels
-- which is what IntT and :-> are
The (higher-order abstract) syntax of our DSL
type family Sem m a :: *Source
Interpretation of EDSL types as host language types
The type interpretation function Sem is parameterized by m
,
which is assumed to be a Monad.
Interpretation of EDSL expressions as values of the host language (Haskell) An EDSL expression of the type a is interpreted as a Haskell value of the type S l m a, where m is a Monad (the parameter of the interpretation) and l is the label for the evaluation order (one of Name, Value, or Lazy). (S l m) is not quite a monad -- only up to the Sem interpretation
t1 :: EDSL exp => exp IntTSource
Evaluating:
t = (lam $ \x -> let_ (x `add` x) $ \y -> y `add` y) `app` int 10
The addition (x add
x) is performed twice because y is bound
to a computation, and y is evaluated twice
The result of subtraction was not needed, and so it was not performed
| OTH, (int 5 add
int 5) was computed four times