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 ...)
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