Safe Haskell | None |
---|---|
Language | Haskell2010 |
This module lets you evaluate Bricks expressions. First expression'to'term
s
converts the abstract syntax tree (Expression
) into an enriched version of the
lambda calculus (Term
). Then we perform graph reduction, repeatedly applying
simplifications until we arrive at an irreducible term.
When we substitute an argument into a lambda body to perform beta-conversion, we
do so by substituting a Pointer
of the argument rather than the term itself.
This gives rise to sharing, thus turning the tree into a general graph, and
helps avoid reducing the same expression more than once.
The Implementation of Functional Programming Languages
The design of Bricks evaluation is in large part based on Simon Peyton Jones's 1987 book The Implementation of Functional Programming Languages. In attempt to keep the Bricks API documentation mostly self-contained, we avoid making frequent references to this work throughout. Instead, here we give a list of some important connections to the book:
- The rationale for immediately converting the AST into another data structure rather than performing any transformations directly on the AST comes from page 38.
- A Bricks function defined using a dict pattern turns into a "pattern-matching lambda abstraction"; this term is introduced on page 61.
- Page 185 introduces the style of drawing ASTs to which the
/@\
operator alludes. - Pointer substitution is described on page 208.
- The implementation of
term'substitute
closely follows the description of Instantiate, page 210. - Page 20 introduces the name capture problem. Pages 199 and 210 discuss how we avoid it by only reducing the top-level redex, which has no free variables.
- On page 233 starts the discussion of how letrec expressions are instantiated as cyclic graphcs.
- newtype Eval a = Eval {}
- does'termPattern'bind :: Text -> TermPattern -> Bool
- instantiate'one :: forall m. MonadEval m => Text -> Term -> Term -> m Term
- instantiate'many :: forall m. MonadEval m => Map Text Term -> Term -> m Term
- reduce'to'type :: Typeable a => Type a -> Term -> IO (Either Bottom a)
- reduce'to'type'or'throw :: (HasCallStack, Typeable a) => Type a -> Term -> IO a
Documentation
does'termPattern'bind :: Text -> TermPattern -> Bool Source #
:: MonadEval m | |
=> Text |
|
-> Term |
|
-> Term |
|
-> m Term |
instantiate var value body
produces a copy of the term body
,
substituting value
for free occurrences of var
.
reduce'to'type'or'throw :: (HasCallStack, Typeable a) => Type a -> Term -> IO a Source #