Is this A-normal shape a realistic linear in size AST?
The essence of compilation with sequels Flanagan et.al. describe a linear time algorithm for converting a term to A-normal form . In short, A-normal form has all applications that only accept trivial arguments (like variables), and all non-trivial members must be concatenated.
Here's a (stupid) example of A-normal form:
let x0 = x0 in
let x2 = \ x1 -> x1 in
let x3 = 1 in
x2 x3
created from this non-normal member of the form:
let y = y in
(\ x0 -> x0) 1
I translated the schema code at the end of the article (page 11) into a lower Haskell module. However, I introduced monads to give me a source of fresh names and keep the display of renamed variables. My question is, does using monads destroy O (n) execution time of an algorithm in a document? I'm particularly worried about nesting >>=
, which for some monads results in O (n ^ 2) behavior.
-- Based on http://slang.soe.ucsc.edu/cormac/papers/pldi93.pdf
import Control.Applicative
import Control.Monad.State.Strict
import Control.Monad.Reader
import qualified Data.Map.Strict as M
type Name = String
data Term = Var Name
| Lam Name Term
| App Term Term
| Let Name Term Term
| Lit Int
deriving Show
type NameSupply a = ReaderT (M.Map Name Name) (State [Name]) a
fresh :: NameSupply String
fresh = do
(name:rest) <- get
put rest
return name
normalizeTerm :: Term -> NameSupply Term
normalizeTerm m = normalize m return
normalize :: Term -> (Term -> NameSupply Term) -> NameSupply Term
normalize m k = case m of
Var x -> do
mx' <- asks (M.lookup x)
case mx' of
Just x' -> k (Var x')
Nothing -> error $ "var not found: " ++ x
Lam x body -> do
x' <- fresh
k =<< (Lam x' <$> local (M.insert x x') (normalizeTerm body))
Let x m1 m2 -> do
x' <- fresh
local (M.insert x x') $ normalize m1 (\ n1 -> Let x' n1 <$> (normalize m2 k))
App m1 m2 -> normalizeName m1 (\ n1 -> normalizeName m2 (k . App n1))
(Lit _) -> k m
normalizeName :: Term -> (Term -> NameSupply Term) -> NameSupply Term
normalizeName m k = normalize m $ \ n -> do
x <- fresh
Let x n <$> k (Var x)
run :: Term -> Term
run = flip evalState names . flip runReaderT M.empty . normalizeTerm
where names = (map (("x" ++) . show) [0..])
example :: Term
example = Let "y" (Var "y") (App (Lam "x0" (Var "x0")) (Lit 1))
source to share
Your monad is simple ReaderT ... (State ...)
and both ReaderT
and State
are passing single values around, so there is no reason to wait for linear time (>>=)
or for an O (n) chain to take O (n ^ 2) time.
You can get left-nested quadratic blow-ups when the monad uses lists or sets or similar.
source to share