diff --git a/.gitignore b/.gitignore
index e2f8c00..0a2bec4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,3 +7,4 @@ node_modules/
 bower_components/
 tmp/
 output/
+.psc-ide-port
diff --git a/bower.json b/bower.json
index 3674de7..7b2d73d 100644
--- a/bower.json
+++ b/bower.json
@@ -18,6 +18,7 @@
     "purescript-integers": "^3.0.0",
     "purescript-generics": "^4.0.0",
     "purescript-console": "^3.0.0",
-    "purescript-exceptions": "^3.0.0"
+    "purescript-exceptions": "^3.0.0",
+    "purescript-quickcheck-laws": "^3.0.1"
   }
 }
diff --git a/package.json b/package.json
index 331664e..b7768e8 100644
--- a/package.json
+++ b/package.json
@@ -1,14 +1,13 @@
 {
-  "name": "purescript-freeap",
-  "version": "3.0.1",
   "private": true,
-  "license": "MIT",
   "scripts": {
-    "psc": "PATH=$PURESCRIPT_0_11_PATH:$PATH psc 'src/**/*.purs' 'test/**/*.purs' 'bower_components/purescript-*/src/**/*.purs' 2>&1",
-    "pscid": "PATH=$PURESCRIPT_0_11_PATH:$PATH pscid",
-    "test": "node -e 'require(\"./output/Test.Main\").main()'"
+    "clean": "rimraf output && rimraf .pulp-cache && rimraf bench/output && rimraf bench/.pulp-cache",
+    "test": "pulp test",
+    "build": "pulp build -- --censor-lib --strict"
   },
   "devDependencies": {
-    "pscid": "^1.12.1"
+    "pulp": "^11.0.0",
+    "purescript-psa": "^0.5.1",
+    "rimraf": "^2.6.1"
   }
 }
diff --git a/src/Control/Applicative/Free.purs b/src/Control/Applicative/Free.purs
index cb92d69..2b6c0cd 100644
--- a/src/Control/Applicative/Free.purs
+++ b/src/Control/Applicative/Free.purs
@@ -7,55 +7,134 @@ module Control.Applicative.Free
   , analyzeFreeAp
   ) where
 
-import Prelude hiding (ap)
-
+import Prelude
 import Data.Const (Const(..))
-import Data.Exists (Exists, mkExists, runExists)
+import Data.Either (Either(..))
+import Data.List (List(..))
+import Data.List.NonEmpty as NEL
 import Data.Monoid (class Monoid)
 import Data.Newtype (unwrap)
+import Data.NonEmpty ((:|))
+import Data.Tuple (Tuple(..))
+import Unsafe.Coerce (unsafeCoerce)
 
 -- | The free applicative functor for a type constructor `f`.
-data FreeAp f a = Pure a | Ap (Exists (ApF f a))
-
-data ApF f a i = ApF (Unit -> f i) (Unit -> FreeAp f (i -> a))
+data FreeAp f a
+  = Pure a
+  | Lift (f a)
+  | Ap (FreeAp f (Val -> a)) (FreeAp f Val)
 
-ap :: forall f a i. (Unit -> f i) -> (Unit -> FreeAp f (i -> a)) -> FreeAp f a
-ap v k = Ap (mkExists (ApF v k))
+data Val
 
 -- | Lift a value described by the type constructor `f` into
 -- | the free applicative functor.
 liftFreeAp :: forall f a. f a -> FreeAp f a
-liftFreeAp a = ap (\_ -> a) (\_ -> Pure id)
+liftFreeAp = Lift
 
--- | Run a free applicative functor using the applicative instance for
--- | the type constructor `f`.
-retractFreeAp :: forall f a. Applicative f => FreeAp f a -> f a
-retractFreeAp (Pure a) = pure a
-retractFreeAp (Ap x) = runExists (\(ApF v k') -> apply (retractFreeAp (k' unit)) (v unit)) x
+type ApFunc g = { func :: g (Val -> Val), count :: Int }
+type FuncStack g = List (ApFunc g)
+type ValStack f = NEL.NonEmptyList (FreeAp f Val)
+type Stack f g = Tuple (FuncStack g) (ValStack f)
 
 -- | Run a free applicative functor with a natural transformation from
 -- | the type constructor `f` to the applicative functor `g`.
 foldFreeAp :: forall f g a. Applicative g => (f ~> g) -> FreeAp f a -> g a
-foldFreeAp k (Pure a) = pure a
-foldFreeAp k (Ap x) = runExists (\(ApF v k') -> apply (map (flip id) (k (v unit))) (foldFreeAp k (k' unit))) x
+foldFreeAp nat z =
+  unsafeToG $ go $ Tuple Nil (NEL.singleton $ unsafeToFVal z)
+  where
+  unsafeToG :: g Val -> g a
+  unsafeToG = unsafeCoerce
+
+  unsafeToFVal :: forall f' a'. FreeAp f' a' -> FreeAp f' Val
+  unsafeToFVal = unsafeCoerce
+
+  go :: Stack f g -> g Val
+  go (Tuple fStack (NEL.NonEmptyList (val :| vals))) =
+    case val of
+      Pure a -> case goApply fStack vals (pure a) of
+        Left x -> x
+        Right s -> go s
+      Lift a -> case goApply fStack vals (nat a) of
+        Left x -> x
+        Right s -> go s
+      Ap l r ->
+        let nextVals = NEL.NonEmptyList (r :| vals)
+        in go $ goLeft fStack nextVals nat l 1
+
+goApply
+  :: forall f g
+  . Applicative g
+  => FuncStack g
+  -> List (FreeAp f Val)
+  -> g Val
+  -> Either (g Val) (Stack f g)
+goApply fStack vals gVal =
+  case fStack of
+    Nil -> Left gVal
+    Cons f fs ->
+      let gRes = f.func <*> gVal
+      in if f.count == 1 then
+        case fs of
+          Nil ->
+            -- here vals must be empty
+            Left gRes
+          _ -> goApply fs vals gRes
+        else
+          case vals of
+            Nil -> Left gRes
+            Cons val vals' ->
+              Right $ Tuple
+                (Cons { func: unsafeToGFunc gRes, count: f.count - 1 } fs)
+                (NEL.NonEmptyList (val :| vals'))
+  where
+  unsafeToGFunc :: g Val -> g (Val -> Val)
+  unsafeToGFunc = unsafeCoerce
+
+goLeft
+  :: forall f g
+  . Applicative g
+  => FuncStack g
+  -> ValStack f
+  -> (f ~> g)
+  -> FreeAp f (Val -> Val)
+  -> Int
+  -> Stack f g
+goLeft fStack valStack nat func count = case func of
+  Pure a -> Tuple (Cons { func: pure a, count } fStack) valStack
+  Lift a -> Tuple (Cons { func: nat a, count } fStack) valStack
+  Ap l r -> goLeft fStack (NEL.cons r valStack) nat (unsafeToFunc l) (count + 1)
+  where
+  unsafeToFunc :: FreeAp f (Val -> Val -> Val) -> FreeAp f (Val -> Val)
+  unsafeToFunc = unsafeCoerce
+
+-- | Run a free applicative functor using the applicative instance for
+-- | the type constructor `f`.
+retractFreeAp :: forall f a. Applicative f => FreeAp f a -> f a
+retractFreeAp = foldFreeAp id
 
 -- | Natural transformation from `FreeAp f a` to `FreeAp g a` given a
 -- | natural transformation from `f` to `g`.
 hoistFreeAp :: forall f g a. (f ~> g) -> FreeAp f a -> FreeAp g a
-hoistFreeAp k (Pure a) = Pure a
-hoistFreeAp k (Ap x) = runExists (\(ApF v k') -> ap (\_ -> k (v unit)) (\_ -> hoistFreeAp k (k' unit))) x
+hoistFreeAp f = foldFreeAp (f >>> liftFreeAp)
 
 -- | Perform monoidal analysis over the free applicative functor `f`.
 analyzeFreeAp :: forall f m a. Monoid m => (forall b. f b -> m) -> FreeAp f a -> m
 analyzeFreeAp k = unwrap <<< foldFreeAp (Const <<< k)
 
+mkAp :: forall f a b. FreeAp f (b -> a) -> FreeAp f b -> FreeAp f a
+mkAp fba fb = Ap (coerceFunc fba) (coerceValue fb)
+  where
+  coerceFunc :: FreeAp f (b -> a) -> FreeAp f (Val -> a)
+  coerceFunc = unsafeCoerce
+
+  coerceValue :: FreeAp f b -> FreeAp f Val
+  coerceValue = unsafeCoerce
+
 instance functorFreeAp :: Functor (FreeAp f) where
-  map k (Pure a) = Pure (k a)
-  map k (Ap x) = runExists (\(ApF v k') -> ap v (\_ -> map ((<<<) k) (k' unit))) x
+  map f x = mkAp (Pure f) x
 
 instance applyFreeAp :: Apply (FreeAp f) where
-  apply (Pure k) f = map k f
-  apply (Ap x) f = runExists (\(ApF v k') -> ap v (\_ -> apply (map flip (k' unit)) f)) x
+  apply fba fb = mkAp fba fb
 
 instance applicativeFreeAp :: Applicative (FreeAp f) where
   pure = Pure
diff --git a/src/Control/Applicative/Free/Gen.purs b/src/Control/Applicative/Free/Gen.purs
new file mode 100644
index 0000000..3e9dcf6
--- /dev/null
+++ b/src/Control/Applicative/Free/Gen.purs
@@ -0,0 +1,40 @@
+module Control.Applicative.Free.Gen where
+
+import Prelude
+
+import Control.Applicative.Free as F
+import Control.Monad.Gen (class MonadGen, oneOf)
+import Control.Monad.Rec.Class (class MonadRec)
+import Data.NonEmpty (NonEmpty(..))
+
+genFree :: forall m f a
+   . MonadGen m
+  => MonadRec m
+  => m (f Unit)
+  -> m a
+  -> m (a -> a)
+  -> m (F.FreeAp f a)
+genFree genF genA genA2A = oneOf $ NonEmpty 
+    ( genA <#> pure)
+    [ do 
+        fUnit <- genF
+        a <- genA
+        pure $ 
+          pure (const a) <*> F.liftFreeAp fUnit
+    , do 
+        fUnit <- genF
+        a <- genA
+        a2a <- genA2A
+        pure $ 
+          (pure (const a) <*> F.liftFreeAp fUnit) <#> a2a
+    , do
+        fUnit <- genF
+        a <- genA
+        a2a <- genA2A
+        pure $
+          F.liftFreeAp fUnit <#> const a <#> a2a
+    , do
+        a <- genA
+        a2a <- genA2A
+        pure $ pure a <#> a2a
+    ]
diff --git a/test/Test/Control/Applicative/Free.purs b/test/Test/Control/Applicative/Free.purs
index b083445..1fb6503 100644
--- a/test/Test/Control/Applicative/Free.purs
+++ b/test/Test/Control/Applicative/Free.purs
@@ -1,10 +1,22 @@
 module Test.Control.Applicative.Free
   ( checkAnalyze
+  , checkStack
+  , check
   ) where
 
-import Prelude (Unit, (==), (<>), unit, apply, map)
-import Control.Applicative.Free (FreeAp, liftFreeAp, analyzeFreeAp)
+import Prelude
+
+import Control.Applicative.Free (FreeAp, liftFreeAp, analyzeFreeAp, retractFreeAp)
+import Control.Applicative.Free.Gen as GenF
 import Data.Either (Either(..))
+import Data.Tuple (Tuple)
+import Test.QuickCheck (class Arbitrary, class Coarbitrary, arbitrary)
+import Test.QuickCheck.Gen (Gen)
+import Test.QuickCheck.Laws (QC, A, checkLaws)
+import Test.QuickCheck.Laws.Control as Control
+import Test.QuickCheck.Laws.Data as Data
+import Type.Proxy (Proxy(..), Proxy2(..))
+
 
 data M r = A r | B r
 
@@ -15,17 +27,68 @@ mb :: FreeAp M Unit
 mb = liftFreeAp (B unit)
 
 printM :: forall a. FreeAp M a -> String
-printM = analyzeFreeAp go where
+printM fr =
+  analyzeFreeAp go fr
+  where
   go (A _) = "A"
   go (B _) = "B"
 
-result :: String
-result = printM (apply (map (\l r -> r) ma) mb)
+build :: Int -> FreeAp M Unit -> FreeAp M Unit -> FreeAp M Unit
+build 0 _ acc = acc
+build n x acc = build (n - 1) x (acc *> x)
 
-expected :: String
-expected = "AB"
+buildExpected :: Int -> String -> String -> String
+buildExpected 0 _ acc = acc
+buildExpected n x acc = buildExpected (n - 1) x (acc <> x)
 
 checkAnalyze :: Either String String
-checkAnalyze = if result == expected
-               then Right result
-               else Left (result <> " is not " <> expected)
+checkAnalyze = 
+  if result == expected
+    then Right result
+    else Left (result <> " is not " <> expected)
+  where
+  result :: String
+  result = printM (build 10 (ma *> mb) mb)
+
+  expected :: String
+  expected = buildExpected 10 "AB" "B"
+
+
+checkStack :: Either String String
+checkStack = 
+  if result == expected
+    then Right "safe for 100000 node"
+    else Left (result <> " is not " <> expected)
+  where
+  result :: String
+  result = printM (build 100000 (ma *> mb) mb)
+
+  expected :: String
+  expected = buildExpected 100000 "AB" "B"
+
+
+newtype ArbFreeAp a = ArbFreeAp (FreeAp (Tuple (Array String)) a)
+
+instance arbitraryArbFreeAp :: (Coarbitrary a, Arbitrary a) => Arbitrary (ArbFreeAp a) where
+  arbitrary = ArbFreeAp <$> 
+    GenF.genFree
+      arbitrary
+      (arbitrary :: Gen a)
+      (arbitrary :: Gen (a -> a))
+
+instance eqArbFreeAp :: Eq a => Eq (ArbFreeAp a) where
+  eq (ArbFreeAp a) (ArbFreeAp b) = retractFreeAp a == retractFreeAp b
+
+derive newtype instance functorArbFreeAp :: Functor ArbFreeAp
+derive newtype instance applyArbFreeAp :: Apply ArbFreeAp
+derive newtype instance applicativeArbFreeAp :: Applicative ArbFreeAp
+
+check ∷ ∀ eff. QC eff Unit
+check = checkLaws "FreeAp" do
+  Data.checkEq prxFree
+  Data.checkFunctor prx2Free
+  Control.checkApply prx2Free
+  Control.checkApplicative prx2Free
+  where
+  prxFree = Proxy ∷ Proxy (ArbFreeAp A)
+  prx2Free = Proxy2 ∷ Proxy2 ArbFreeAp
diff --git a/test/Test/Main.purs b/test/Test/Main.purs
index 584a1da..03db937 100644
--- a/test/Test/Main.purs
+++ b/test/Test/Main.purs
@@ -1,14 +1,14 @@
 module Test.Main where
 
-import Prelude (Unit, bind, discard)
-
+import Prelude
 import Control.Monad.Eff (Eff)
 import Control.Monad.Eff.Console (CONSOLE, log, logShow)
-
-import Test.Control.Applicative.Free.Validation as Validation
+import Control.Monad.Eff.Exception (EXCEPTION)
+import Control.Monad.Eff.Random (RANDOM)
 import Test.Control.Applicative.Free as FreeTest
+import Test.Control.Applicative.Free.Validation as Validation
 
-main :: Eff (console :: CONSOLE) Unit
+main :: Eff (console ∷ CONSOLE , random ∷ RANDOM , exception ∷ EXCEPTION) Unit
 main = do
   log "\nvalid case:"
   logShow (Validation.runForm "Joe" "Smith" "28")
@@ -21,3 +21,9 @@ main = do
 
   log "\nanalyze:"
   logShow FreeTest.checkAnalyze
+  
+  log "\nstack safety:"
+  logShow FreeTest.checkStack
+  
+  log "\nlaws:"
+  FreeTest.check