diff --git a/INSTALL b/INSTALL
--- a/INSTALL
+++ b/INSTALL
@@ -1,16 +1,16 @@
 # Installation Instructions
 
-You can install the `cflp` package as follows.
+You can install the `cflp` package as follows:
 
- 1. Unpack the sources and move into the source directory.
+    > ./configure
+    > make
+    > make install
 
-        > tar -xzf cflp-*.tar.gz
-        > cd cflp-*
+This will register the package in your user package databse. 
 
- 2. Run configure, build, test, and install.
+If you want to install it globally, type:
 
-        > runhaskell Setup.lhs configure --user
-        > runhaskell Setup.lhs build
-        > runhaskell Setup.lhs test
-        > runhaskell Setup.lhs install
+    > ./configure --global
+    > make
+    > sudo make install
 
diff --git a/Makefile b/Makefile
new file mode 100644
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,6 @@
+build:
+	runhaskell Setup.lhs build
+
+install:
+	runhaskell Setup.lhs install
+
diff --git a/README b/README
--- a/README
+++ b/README
@@ -12,3 +12,6 @@
 
 [cflp]: http://www-ps.informatik.uni-kiel.de/~sebf/projects/cflp.html
 
+Sebastian Fischer, 2008
+sebf@informatik.uni-kiel.de
+
diff --git a/cflp.cabal b/cflp.cabal
--- a/cflp.cabal
+++ b/cflp.cabal
@@ -1,5 +1,5 @@
 Name:          cflp
-Version:       0.1
+Version:       0.2.0
 Cabal-Version: >= 1.2
 Synopsis:      Constraint Functional-Logic Programming in Haskell
 Description:   This package provides combinators for constraint
@@ -17,7 +17,7 @@
 Build-Type:    Custom
 Stability:     alpha
 
-Extra-Source-Files: README, INSTALL, Test.lhs
+Extra-Source-Files: README, INSTALL, Makefile, configure, Test.lhs
 
 Library
   Build-Depends:    base >= 4, ghc, mtl, syb, HUnit
@@ -25,8 +25,14 @@
   Other-Modules:    Control.Monad.Constraint,
                     Control.Monad.Constraint.Choice,
                     Data.LazyNondet,
-                    Data.LazyNondet.Bool,
-                    Data.LazyNondet.List,
+                    Data.LazyNondet.Types,
+                    Data.LazyNondet.Types.Bool,
+                    Data.LazyNondet.Types.List,
+                    Data.LazyNondet.UniqueID,
+                    Data.LazyNondet.Matching,
+                    Data.LazyNondet.Narrowing,
+                    Data.LazyNondet.Primitive,
+                    Data.LazyNondet.Combinators,
                     Control.CFLP.Tests,
                     Control.CFLP.Tests.CallTimeChoice
   Hs-Source-Dirs:   src
@@ -34,9 +40,10 @@
                     MultiParamTypeClasses,
                     FlexibleInstances,
                     FlexibleContexts,
+                    PatternGuards,
                     TypeFamilies,
                     RankNTypes
-  Ghc-Options:      -O2 -Wall -fno-warn-orphans
+  Ghc-Options:      -Wall -fno-warn-orphans
 
 Source-Repository head
   type:     git
diff --git a/configure b/configure
new file mode 100644
--- /dev/null
+++ b/configure
@@ -0,0 +1,2 @@
+#!/bin/bash
+runhaskell Setup.lhs configure ${1-"--user"}
diff --git a/src/Control/CFLP.lhs b/src/Control/CFLP.lhs
--- a/src/Control/CFLP.lhs
+++ b/src/Control/CFLP.lhs
@@ -13,19 +13,20 @@
 >
 > module Control.CFLP (
 >
->   CFLP, Computation, eval, evalPrint,
+>   CFLP, ChoiceStore, Computation, eval, evalPartial, evalPrint,
 >
 >   Strategy, depthFirst,
 >
 >   module Data.LazyNondet,
->   module Data.LazyNondet.Bool,
->   module Data.LazyNondet.List
+>   module Data.LazyNondet.Types.Bool,
+>   module Data.LazyNondet.Types.List
 >
 > ) where
 >
 > import Data.LazyNondet
-> import Data.LazyNondet.Bool
-> import Data.LazyNondet.List
+> import Data.LazyNondet.Primitive
+> import Data.LazyNondet.Types.Bool
+> import Data.LazyNondet.Types.List
 >
 > import Control.Monad.State
 > import Control.Monad.Constraint
@@ -33,6 +34,7 @@
 >
 > class (MonadConstr Choice m,
 >        ConstraintStore Choice cs,
+>        ChoiceStore cs,
 >        MonadSolve cs m m)
 >  => CFLP cs m
 
@@ -41,17 +43,17 @@
 constraint store and a constraint monad. Hence, such computations can
 be executed with different constraint stores and search strategies.
 
-> instance CFLP ChoiceStore (ConstrT ChoiceStore [])
+> instance CFLP ChoiceStoreUnique (ConstrT ChoiceStoreUnique [])
 
 We declare instances for every combination of monad and constraint
 store that we intend to use.
 
-> type EvalStore = ChoiceStore
+> type CS = ChoiceStoreUnique
 >
-> noConstraints :: EvalStore
+> noConstraints :: CS
 > noConstraints = noChoices
 >
-> type Computation m a = EvalStore -> ID -> Nondet (ConstrT EvalStore m) a
+> type Computation m a = CS -> ID -> Nondet CS (ConstrT CS m) a
 
 Currently, the constraint store used to evaluate constraint
 functional-logic programs is simply a `ChoiceStore`. It will be a
@@ -68,20 +70,28 @@
 
 The strategy of the list monad is depth-first search.
 
-> eval :: (CFLP EvalStore m, MonadSolve EvalStore m m', Data a)
->      => Strategy m' -> (EvalStore -> ID -> Nondet m a)
->      -> IO [a]
-> eval enumerate op = do
+> evaluate :: (CFLP CS m, MonadSolve CS m m')
+>          => (Nondet CS m a -> CS -> m' b)
+>          -> Strategy m' -> (CS -> ID -> Nondet CS m a)
+>          -> IO [b]
+> evaluate evalNondet enumerate op = do
 >   i <- initID
->   return (enumerate (normalForm (op noConstraints i) noConstraints))
+>   return $ enumerate $ evalNondet (op noConstraints i) noConstraints
 
-The `eval` function enumerates the non-deterministic solutions of a
+The `evaluate` function enumerates the non-deterministic solutions of a
 constraint functional-logic computation according to a given strategy.
 
-> evalPrint :: (CFLP EvalStore m, MonadSolve EvalStore m m', Data a, Show a)
->           => Strategy m' -> (EvalStore -> ID -> Nondet m a)
+> eval, evalPartial :: (CFLP CS m, MonadSolve CS m m', Data a)
+>                   => Strategy m' -> (CS -> ID -> Nondet CS m a)
+>                   -> IO [a]
+> eval        s = liftM (map prim) . evaluate groundNormalForm  s
+> evalPartial s = liftM (map prim) . evaluate partialNormalForm s
+>
+> evalPrint :: (CFLP CS m, MonadSolve CS m m', Data a, Show a)
+>           => Strategy m' -> (CS -> ID -> Nondet CS m a)
 >           -> IO ()
 > evalPrint s op = eval s op >>= printSols
+>  -- evaluate partialNormalForm s op >>= printSols
 >
 > printSols :: Show a => [a] -> IO ()
 > printSols []     = putStrLn "No more solutions."
@@ -95,7 +105,14 @@
 >     then mapM_ print xs
 >     else printSols xs
 
-For convenience, we provide an `evalPrint` operation that
-interactively shows solutions of a constraint functional-logic
-computation.
+We provide
+
+  * an `eval` operation to compute Haskell terms from non-determinitic
+    data,
+
+  * an operation `evalPartial` to compute partial Haskell terms where
+    logic variables are replaced with an error, and
+
+  * an `evalPrint` operation that interactively shows (partial)
+    solutions of a constraint functional-logic computation.
 
diff --git a/src/Control/CFLP/Tests/CallTimeChoice.lhs b/src/Control/CFLP/Tests/CallTimeChoice.lhs
--- a/src/Control/CFLP/Tests/CallTimeChoice.lhs
+++ b/src/Control/CFLP/Tests/CallTimeChoice.lhs
@@ -30,9 +30,10 @@
 > ignoreFirstNarrowSecond :: Assertion
 > ignoreFirstNarrowSecond = assertResults comp [True,False]
 >  where
->   comp cs u = ignot (error "illegal demand") (unknown u) cs
+>   comp cs u = ignot (error "illegal demand") (unknown cs u) cs
 >
-> ignot :: CFLP cs m => Nondet m a -> Nondet m Bool -> cs -> Nondet m Bool
+> ignot :: CFLP cs m
+>       => Nondet cs m a -> Nondet cs m Bool -> cs -> Nondet cs m Bool
 > ignot _ x = not x
 
 This test checks a function with two arguments, where the first must
@@ -44,9 +45,9 @@
 > sharedVarsAreEqual :: Assertion
 > sharedVarsAreEqual = assertResults comp [[False,False],[True,True]]
 >  where
->   comp _ u = two (unknown u)
+>   comp cs u = two (unknown cs u)
 >
-> two :: Monad m => Nondet m a -> Nondet m [a]
+> two :: Monad m => Nondet cs m a -> Nondet cs m [a]
 > two x = x ^: x ^: nil
 
 This test checks call-time choice semantics: variables represent
@@ -61,7 +62,7 @@
 > noDemandOnSharedVar :: Assertion
 > noDemandOnSharedVar = assertResults comp [False]
 >  where
->   comp cs _ = null (two (error "illegal demand")) cs
+>   comp cs _ = null (two (error "illegal demand" :: Nondet cs m Bool)) cs
 
 Even with an explicit combinator for sharing (to be used, e.g., in the
 definition of the function `two`) there must not be demand on
@@ -70,9 +71,9 @@
 > sharedCompoundTerms :: Assertion
 > sharedCompoundTerms = assertResults comp [[True,False],[False,True]]
 >  where
->   comp cs u = negHeads (unknown u) cs
+>   comp cs u = negHeads (unknown cs u) cs
 >
-> negHeads :: CFLP cs m => Nondet m [Bool] -> cs -> Nondet m [Bool]
+> negHeads :: CFLP cs m => Nondet cs m [Bool] -> cs -> Nondet cs m [Bool]
 > negHeads l cs = not (head l cs) cs ^: head l cs ^: nil
 
 This test checks whether sharing is ensured on aruments of compound
diff --git a/src/Control/Monad/Constraint/Choice.lhs b/src/Control/Monad/Constraint/Choice.lhs
--- a/src/Control/Monad/Constraint/Choice.lhs
+++ b/src/Control/Monad/Constraint/Choice.lhs
@@ -17,7 +17,7 @@
 >
 > module Control.Monad.Constraint.Choice (
 >
->   Choice, ChoiceStore, noChoices, choice
+>   Choice, ChoiceStore(..), ChoiceStoreUnique, noChoices, choice
 >
 > ) where
 >
@@ -30,14 +30,27 @@
 We borrow unique identifiers from the package `ghc` which is hidden by
 default.
 
+> class ChoiceStore cs
+>  where
+>   lookupChoice :: Unique -> cs -> Maybe Int
+
+We define an interface for choice stores that provide an operation to
+lookup a previously made choice.
+
 > newtype Choice = Choice (Unique,Int)
-> newtype ChoiceStore = ChoiceStore (UniqFM Int)
+> newtype ChoiceStoreUnique = ChoiceStore (UniqFM Int)
 >
-> noChoices :: ChoiceStore
+> noChoices :: ChoiceStoreUnique
 > noChoices = ChoiceStore emptyUFM
 >
-> instance ConstraintStore Choice ChoiceStore
+> instance ChoiceStore ChoiceStoreUnique
 >  where
+>   lookupChoice u (ChoiceStore cs) = lookupUFM_Directly cs u
+
+A finite map mapping `Unique`s to integers is a `ChoiceStore`.
+
+> instance ConstraintStore Choice ChoiceStoreUnique
+>  where
 >   assert (Choice (u,x)) = do
 >     ChoiceStore cs <- get
 >     maybe (put (ChoiceStore (addToUFM_Directly cs u x)))
@@ -49,8 +62,12 @@
 
 The `assert` operations fails to insert conflicting choices.
 
-> choice :: MonadConstr Choice m => Unique -> [m a] -> m a
-> choice u = foldr1 mplus . (mzero:) . zipWith constrain [(0::Int)..]
+> choice :: (MonadConstr Choice m, ChoiceStore cs)
+>        => cs -> Unique -> [m a] -> m a
+> choice cs u xs =
+>   maybe (foldr1 mplus . (mzero:) . zipWith constrain [(0::Int)..] $ xs)
+>         (xs!!)
+>         (lookupChoice u cs)
 >  where constrain n = (constr (Choice (u,n))>>)
 
 The operation `choice` takes a unique label and a list of monadic
@@ -59,4 +76,12 @@
 occurs more than once in a bigger monadic action, the result is
 constrained to take the same alternative everywhere when collecting
 constraints.
+
+If a choice with the same label has been created previously and the
+label is already constrained to an alternative, then this alternative
+is returned directly and no choice is created.
+
+This situation may occur if a shared logic variable is renarrowed
+whenever it is demanded rather than shared and only narrowed on
+creation.
 
diff --git a/src/Data/LazyNondet.lhs b/src/Data/LazyNondet.lhs
--- a/src/Data/LazyNondet.lhs
+++ b/src/Data/LazyNondet.lhs
@@ -4,363 +4,28 @@
 This module provides a datatype with operations for lazy
 non-deterministic programming.
 
-> {-# LANGUAGE
->       ExistentialQuantification,
->       MultiParamTypeClasses,
->       FlexibleInstances,
->       FlexibleContexts,
->       TypeFamilies,
->       FunctionalDependencies
->   #-}
->
 > module Data.LazyNondet (
 >
->   NormalForm, HeadNormalForm(..), mkHNF, Nondet(..),
+>   NormalForm, Nondet,
 >
 >   ID, initID, withUnique,
 >
->   Unknown(..), failure, oneOf, withHNF, caseOf, caseOf_, Match,
+>   Narrow(..), NarrowPolicy(..), unknown, 
 >
->   Data, nondet, normalForm,
+>   failure, oneOf,
 >
->   ConsRep(..), cons, match,
+>   withHNF, caseOf, caseOf_, Match,
 >
->   prim_eq
+>   Data, nondet, groundNormalForm, partialNormalForm,
 >
+>   ConsRep(..), cons, match,
+>
 > ) where
 >
 > import Data.Data
-> import Data.Generics.Twins ( gmapAccumT )
->
-> import Control.Monad.State
-> import Control.Monad.Constraint
-> import Control.Monad.Constraint.Choice
->
-> import UniqSupply
-
-We borrow unique identifiers from the package `ghc` which is hidden by
-default.
-
-> data NormalForm = NormalForm Constr [NormalForm]
->  deriving Show
-
-The normal form of data is represented by the type `NormalForm` which
-defines a tree of constructors. The type `Constr` is a representation
-of constructors defined in the `Data.Generics` package. With generic
-programming we can convert between Haskell data types and the
-`NormalForm` type.
-
-> data HeadNormalForm m = Cons DataType ConIndex [Untyped m]
-> type Untyped m = m (HeadNormalForm m)
->
-> mkHNF :: Constr -> [Untyped m] -> HeadNormalForm m
-> mkHNF c args = Cons (constrType c) (constrIndex c) args
-
-Data in lazy functional-logic programs is evaluated on demand. The
-evaluation of arguments of a constructor may lead to different
-non-deterministic results. Hence, we use a monad around every
-constructor in the head-normal form of a value.
-
-In head-normal forms we split the constructor representation into a
-representation of the data type and the index of the constructor, to
-enable pattern matching on the index.
-
-> newtype Nondet m a = Typed { untyped :: Untyped m }
-
-Untyped non-deterministic data can be phantom typed in order to define
-logic variables by overloading. The phantom type must be the Haskell
-data type that should be used for conversion.
-
-Threading Unique Identifiers
-----------------------------
-
-Non-deterministic computations need a supply of unique identifiers in
-order to constrain shared choices.
-
-> newtype ID = ID UniqSupply
->
-> initID :: IO ID
-> initID = liftM ID $ mkSplitUniqSupply 'x'
->
-> class With x a
->  where
->   type Mon x a :: * -> *
->   type Typ x a
->
->   with :: a -> x -> Nondet (Mon x a) (Typ x a)
->
-> instance With x (Nondet m a)
->  where
->   type Mon x (Nondet m a) = m
->   type Typ x (Nondet m a) = a
->
->   with = const
->
-> instance With ID a => With ID (ID -> a)
->  where
->   type Mon ID (ID -> a) = Mon ID a
->   type Typ ID (ID -> a) = Typ ID a
->
->   with f (ID us) = withUnique (f (ID vs)) (ID ws)
->    where (vs,ws) = splitUniqSupply us
->
-> withUnique :: With ID a => a -> ID -> Nondet (Mon ID a) (Typ ID a)
-> withUnique = with
-
-We provide an overloaded operation `withUnique` to simplify the
-distribution of unique identifiers when defining possibly
-non-deterministic operations. Non-deterministic operations have an
-additional argument for unique identifiers. The operation `withUnique`
-allows to consume an arbitrary number of unique identifiers hiding
-their generation. Conceptually, it has all of the following types at
-the same time:
-
-    Nondet m a -> ID -> Nondet m a
-    (ID -> Nondet m a) -> ID -> Nondet m a
-    (ID -> ID -> Nondet m a) -> ID -> Nondet m a
-    (ID -> ID -> ID -> Nondet m a) -> ID -> Nondet m a
-    ...
-
-We make use of type families because GHC considers equivalent
-definitions with functional dependencies illegal due to the overly
-restrictive "coverage condition".
-
-Combinators for Functional-Logic Programming
---------------------------------------------
-
-> class Unknown a
->  where
->   unknown :: MonadConstr Choice m => ID -> Nondet m a
-
-The application of `unknown` to a unique identifier represents a logic
-variable of the corresponding type.
-
-> oneOf :: MonadConstr Choice m => [Nondet m a] -> ID -> Nondet m a
-> oneOf xs (ID us) = Typed (choice (uniqFromSupply us) (map untyped xs))
-
-The operation `oneOf` takes a list of non-deterministic values and
-returns a non-deterministic value that yields one of the elements in
-the given list.
-
-> failure :: MonadPlus m => Nondet m a
-> failure = Typed mzero
-
-A failing computation could be defined using `oneOf`, but we provide a
-special combinator that does not need a supply of unique identifiers.
-
-> withHNF :: (Monad m, MonadSolve cs m m)
->         => Nondet m a
->         -> (HeadNormalForm m -> cs -> Nondet m b)
->         -> cs -> Nondet m b
-> withHNF x b cs = Typed (do
->   (hnf,cs') <- runStateT (solve (untyped x)) cs
->   untyped (b hnf cs'))
-
-The `withHNF` operation can be used for pattern matching and solves
-constraints associated to the head constructor of a non-deterministic
-value. An updated constraint store is passed to the computation of the
-branch function. Collected constraints are kept attached to the
-computed value by using an appropriate instance of `MonadSolve` that
-does not eliminate them.
-
-> caseOf :: MonadSolve cs m m
->        => Nondet m a -> [Match cs m b] -> cs -> Nondet m b
-> caseOf x bs = caseOf_ x bs failure
->
-> caseOf_ :: MonadSolve cs m m
->         => Nondet m a -> [Match cs m b] -> Nondet m b -> cs -> Nondet m b
-> caseOf_ x bs def =
->   withHNF x $ \ (Cons _ idx args) cs ->
->                  maybe def (\b -> branch (b cs) args)
->                   (lookup idx (map unMatch bs))
->
-> newtype Match cs m a = Match { unMatch :: (ConIndex, cs -> Branch m a) }
-> data Branch m a = forall t . (WithUntyped t, m ~ M t, a ~ T t) => Branch t
->
-> branch :: Branch m a -> [Untyped m] -> Nondet m a
-> branch (Branch alt) = withUntyped alt
-
-We provide operations `caseOf` and `caseOf` (with and without a
-default alternative) for more convenient pattern matching. The untyped
-values are hidden so functional-logic code does not need to match on
-the `Cons` constructor explicitly. However, using this combinator
-causes an additional slowdown because of the list lookup. It remains
-to be checked how big the slowdown of using `caseOf` is compared to
-using `withHNF` directly.
-
-> class WithUntyped a
->  where
->   type M a :: * -> *
->   type T a
->
->   withUntyped :: a -> [Untyped (M a)] -> Nondet (M a) (T a)
-
-We repeat the definition of the type class `With` because the current
-implementation of GHC does not allow equality constraints in
-super-class constraints. We would prefer to define this class as
-follows:
-
-    class (With [Untyped m] a, m ~ Mon [Untyped m] a) => WithUnique a
-     where
-      withUnique :: a -> [Untyped m] -> Nondet m (Typ [Untyped m] a)
-      withUnique = with
-
-So it is just a copy of the type class `With` where the argument type
-is specialized to use the same monad.
-
-> instance WithUntyped (Nondet m a)
->  where
->   type M (Nondet m a) = m
->   type T (Nondet m a) = a
->
->   withUntyped = const
->
-> instance (WithUntyped a, m ~ M a) => WithUntyped (Nondet m b -> a)
->  where
->   type M (Nondet m b -> a) = M a
->   type T (Nondet m b -> a) = T a
->
->   withUntyped alt (x:xs) = withUntyped (alt (Typed x)) xs
->   withUntyped _ _ = error "LazyNondet.withUntyped: too few arguments"
-
-These instances define the overloaded function `withUntyped` that has
-all of the following types at the same time:
-
-    withUntyped :: Nondet m a -> [Untyped m] -> Nondet m a
-    withUntyped :: (Nondet m a -> Nondet m b) -> [Untyped m] -> Nondet m b
-    ...
-
-If the function given as first argument has n arguments, then the
-application of `withUntyped` to this function consumes n elements of
-the list of untyped values.
-
-Converting Between Primitive and Non-Deterministic Data
--------------------------------------------------------
-
-> prim :: Data a => NormalForm -> a
-> prim (NormalForm con args) =
->   snd (gmapAccumT perkid args (fromConstr con))
->  where
->   perkid ts _ = (tail ts, prim (head ts))
->
-> generic :: Data a => a -> NormalForm
-> generic x = NormalForm (toConstr x) (gmapQ generic x)
->
-> nf2hnf :: Monad m => NormalForm -> Untyped m
-> nf2hnf (NormalForm con args) = return (mkHNF con (map nf2hnf args))
->
-> nondet :: (Monad m, Data a) => a -> Nondet m a
-> nondet = Typed . nf2hnf . generic
-
-We provide generic operations to convert between instances of the
-`Data` class and non-deterministic data.
-
-> normalForm :: (MonadSolve cs m m', Data a) => Nondet m a -> cs -> m' a
-> normalForm x cs = liftM prim $ evalStateT (nf (untyped x)) cs
->
-> nf :: MonadSolve cs m m' => Untyped m -> StateT cs m' NormalForm
-> nf x = do
->   Cons typ idx args <- solve x
->   nfs <- mapM nf args
->   return (NormalForm (indexConstr typ idx) nfs)
-
-The `normalForm` function evaluates a non-deterministic value and
-lifts all non-deterministic choices to the top level. The results are
-deterministic values and can be converted into their Haskell
-representation.
-
-Syntactic Sugar for Datatype Declarations
------------------------------------------
-
-> class MkCons m a b | b -> m
->  where
->   mkCons :: a -> [Untyped m] -> b
->
-> instance (Monad m, Data a) => MkCons m a (Nondet m t)
->  where
->   mkCons c args = Typed (return (mkHNF (toConstr c) (reverse args)))
->
-> instance MkCons m b c => MkCons m (a -> b) (Nondet m t -> c)
->  where
->   mkCons c xs x = mkCons (c undefined) (untyped x:xs)
->
-> cons :: MkCons m a b => a -> b
-> cons c = mkCons c []
-
-The overloaded operation `constr` takes a Haskell constructor and yields
-a corresponding constructor function for non-deterministic values.
-
-> match :: (ConsRep a, WithUntyped b)
->       => a -> (cs -> b) -> Match cs (M b) (T b)
-> match c alt = Match (constrIndex (consRep c), Branch . alt)
-
-The operation `decons` is used to build destructor functions for
-non-deterministic values that can be used with `caseOf`.
-
-> class ConsRep a
->  where
->   consRep :: a -> Constr
->
-> instance ConsRep b => ConsRep (a -> b)
->  where
->   consRep c = consRep (c undefined)
-
-We provide an overloaded operation `consRep` that yields a `Constr`
-representation for a constructor rather than for a constructed value
-like `Data.Data.toConstr` does. We do not provide the base instance
-
-    instance Data a => ConsRep a
-     where
-      consRep = toConstr
-
-because this would require to allow undecidable instances. As a
-consequence, specialized base instances need to be defined for every
-used datatype. See `Data.LazyNondet.List` for an example of how to get
-the representation of polymorphic constructors and destructors.
-
-Primitive Generic Functions
----------------------------
-
-> prim_eq :: MonadSolve cs m m => Untyped m -> Untyped m -> StateT cs m Bool
-> prim_eq x y = do
->   Cons _ ix xs <- solve x
->   Cons _ iy ys <- solve y
->   if ix==iy then all_eq xs ys else return False
->  where
->   all_eq [] [] = return True
->   all_eq (v:vs) (w:ws) = do
->     eq <- prim_eq v w
->     if eq then all_eq vs ws else return False
->   all_eq _ _ = return False
-
-We provide a generic comparison function for untyped non-deterministic
-data that is used to define a typed equality test in the
-`Data.LazyNondet.Bool` module.
-
-`Show` Instances
-----------------
-
-> instance Show (HeadNormalForm [])
->  where
->   show (Cons typ idx args) 
->     | null args = show con
->     | otherwise = unwords (("("++show con):map show args++[")"])
->    where con = indexConstr typ idx
->
-> instance Show (Nondet [] a)
->  where
->   show = show . untyped
->
-> instance Show (Nondet (ConstrT cs []) a)
->  where
->   show = show . untyped
->
-> instance Show (HeadNormalForm (ConstrT cs []))
->  where
->   show (Cons typ idx [])   = show (indexConstr typ idx)
->   show (Cons typ idx args) =
->     "("++show (indexConstr typ idx)++" "++unwords (map show args)++")" 
-
-To simplify debugging, we provide `Show` instances for head-normal
-forms and non-deterministic values.
-
+> import Data.LazyNondet.Types
+> import Data.LazyNondet.UniqueID
+> import Data.LazyNondet.Matching
+> import Data.LazyNondet.Narrowing
+> import Data.LazyNondet.Primitive
+> import Data.LazyNondet.Combinators
diff --git a/src/Data/LazyNondet/Bool.lhs b/src/Data/LazyNondet/Bool.lhs
deleted file mode 100644
--- a/src/Data/LazyNondet/Bool.lhs
+++ /dev/null
@@ -1,43 +0,0 @@
-% Lazy Non-Deterministic Bools
-% Sebastian Fischer (sebf@informatik.uni-kiel.de)
-
-This module provides non-deterministic booleans.
-
-> module Data.LazyNondet.Bool where
->
-> import Data.Data
-> import Data.LazyNondet
->
-> import Control.Monad.State
-> import Control.Monad.Constraint
->
-> instance ConsRep Bool where consRep = toConstr
->
-> true :: Monad m => Nondet m Bool
-> true = cons True
->
-> pTrue :: (cs -> Nondet m a) -> Match cs m a
-> pTrue = match True
->
-> false :: Monad m => Nondet m Bool
-> false = cons False
->
-> pFalse :: (cs -> Nondet m a) -> Match cs m a
-> pFalse = match False
-
-In order to be able to use logic variables of boolean type, we make it
-an instance of the type class `Unknown`.
-
-> instance Unknown Bool
->  where
->   unknown = oneOf [false,true]
-
-Some operations with `Bool`s:
-
-> not :: MonadSolve cs m m => Nondet m Bool -> cs -> Nondet m Bool
-> not x = caseOf_ x [pFalse (\_ -> true)] false
-
-> (===) :: MonadSolve cs m m => Nondet m a -> Nondet m a -> cs -> Nondet m Bool
-> (x === y) cs = Typed $ do
->   eq <- evalStateT (prim_eq (untyped x) (untyped y)) cs
->   untyped $ if eq then true else false
diff --git a/src/Data/LazyNondet/Combinators.lhs b/src/Data/LazyNondet/Combinators.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/Combinators.lhs
@@ -0,0 +1,77 @@
+% Combinators for Programs on Lazy Non-Deterministic Data
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+> {-# LANGUAGE
+>       FlexibleContexts,
+>       FlexibleInstances,
+>       MultiParamTypeClasses,
+>       FunctionalDependencies
+>   #-}
+>
+> module Data.LazyNondet.Combinators (
+>
+>   cons, failure, oneOf, ConsRep(..)
+>
+> ) where
+>
+> import Data.Data
+> import Data.LazyNondet.Types
+>
+> import Control.Monad
+> import Control.Monad.Constraint
+> import Control.Monad.Constraint.Choice
+>
+> import UniqSupply
+>
+> oneOf :: (MonadConstr Choice m, ChoiceStore cs)
+>       => [Nondet cs m a] -> cs -> ID -> Nondet cs m a
+> oneOf xs cs (ID us) = Typed (choice cs (uniqFromSupply us) (map untyped xs))
+
+The operation `oneOf` takes a list of non-deterministic values and
+returns a non-deterministic value that yields one of the elements in
+the given list.
+
+> failure :: MonadPlus m => Nondet cs m a
+> failure = Typed mzero
+
+A failing computation could be defined using `oneOf`, but we provide a
+special combinator that does not need a supply of unique identifiers.
+
+> class MkCons cs m a b | b -> m, b -> cs
+>  where
+>   mkCons :: a -> [Untyped cs m] -> b
+>
+> instance (Monad m, Data a) => MkCons cs m a (Nondet cs m t)
+>  where
+>   mkCons c args = Typed (return (mkHNF (toConstr c) (reverse args)))
+>
+> instance MkCons cs m b c => MkCons cs m (a -> b) (Nondet cs m t -> c)
+>  where
+>   mkCons c xs x = mkCons (c undefined) (untyped x:xs)
+>
+> cons :: MkCons cs m a b => a -> b
+> cons c = mkCons c []
+
+The overloaded operation `cons` takes a Haskell constructor and yields
+a corresponding constructor function for non-deterministic values.
+
+> class ConsRep a
+>  where
+>   consRep :: a -> Constr
+>
+> instance ConsRep b => ConsRep (a -> b)
+>  where
+>   consRep c = consRep (c undefined)
+
+We provide an overloaded operation `consRep` that yields a `Constr`
+representation for a constructor rather than for a constructed value
+like `Data.Data.toConstr` does. We do not provide the base instance
+
+    instance Data a => ConsRep a
+     where
+      consRep = toConstr
+
+because this would require to allow undecidable instances. As a
+consequence, specialized base instances need to be defined for every
+used datatype. See `Data.LazyNondet.List` for an example of how to get
+the representation of polymorphic constructors and destructors.
diff --git a/src/Data/LazyNondet/List.lhs b/src/Data/LazyNondet/List.lhs
deleted file mode 100644
--- a/src/Data/LazyNondet/List.lhs
+++ /dev/null
@@ -1,54 +0,0 @@
-% Lazy Non-Deterministic Lists
-% Sebastian Fischer (sebf@informatik.uni-kiel.de)
-
-This module provides non-deterministic lists.
-
-> {-# LANGUAGE
->       FlexibleInstances
->   #-}
->
-> module Data.LazyNondet.List where
->
-> import Data.Data
-> import Data.LazyNondet
-> import Data.LazyNondet.Bool
->
-> import Control.Monad.Constraint
->
-> instance ConsRep [()] where consRep = toConstr
->
-> nil :: Monad m => Nondet m [a]
-> nil = cons ([] :: [()])
->
-> pNil :: (cs -> Nondet m a) -> Match cs m a
-> pNil = match ([] :: [()])
->
-> infixr 5 ^:
-> (^:) :: Monad m => Nondet m a -> Nondet m [a] -> Nondet m [a]
-> (^:) = cons ((:) :: () -> [()] -> [()])
->
-> pCons :: (cs -> Nondet m a -> Nondet m [a] -> Nondet m b) -> Match cs m b
-> pCons = match ((:) :: () -> [()] -> [()])
->
-> fromList :: Monad m => [Nondet m a] -> Nondet m [a]
-> fromList = foldr (^:) nil
-
-We can use logic variables of a list type if there are logic variables
-for the element type.
-
-> instance Unknown a => Unknown [a]
->  where
->   unknown = withUnique $ \u1 u2 -> 
->              oneOf [nil, unknown u1 ^: unknown u2]
-
-Some operations on lists:
-
-> null :: MonadSolve cs m m => Nondet m [a] -> cs -> Nondet m Bool
-> null xs = caseOf_ xs [pNil (\_ -> true)] false
->
-> head :: MonadSolve cs m m => Nondet m [a] -> cs -> Nondet m a
-> head l = caseOf l [pCons (\_ x _ -> x)]
->
-> tail :: MonadSolve cs m m => Nondet m [a] -> cs -> Nondet m [a]
-> tail l = caseOf l [pCons (\_ _ xs -> xs)]
-
diff --git a/src/Data/LazyNondet/Matching.lhs b/src/Data/LazyNondet/Matching.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/Matching.lhs
@@ -0,0 +1,134 @@
+% Pattern Matching of Lazy Non-Deterministic Data
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+> {-# LANGUAGE
+>       RankNTypes,
+>       TypeFamilies,
+>       FlexibleContexts,
+>       FlexibleInstances,
+>       ExistentialQuantification
+>   #-}
+>
+> module Data.LazyNondet.Matching (
+>
+>   Match, match, withHNF, caseOf, caseOf_
+>
+> ) where
+>
+> import Data.Data
+> import Data.LazyNondet.Types
+> import Data.LazyNondet.Combinators
+>
+> import Control.Monad.State
+> import Control.Monad.Constraint
+> import Control.Monad.Constraint.Choice
+>
+> withHNF :: (Monad m, MonadSolve cs m m)
+>         => Nondet cs m a
+>         -> (HeadNormalForm cs m -> cs -> Nondet cs m b)
+>         -> cs -> Nondet cs m b
+> withHNF x b cs = Typed (do
+>   (hnf,cs') <- runStateT (solve (untyped x)) cs
+>   untyped (b hnf cs'))
+
+The `withHNF` operation can be used for pattern matching and solves
+constraints associated to the head constructor of a non-deterministic
+value. An updated constraint store is passed to the computation of the
+branch function. Collected constraints are kept attached to the
+computed value by using an appropriate instance of `MonadSolve` that
+does not eliminate them.
+
+> class WithUntyped a
+>  where
+>   type C a
+>   type M a :: * -> *
+>   type T a
+>
+>   withUntyped :: a -> [Untyped (C a) (M a)] -> Nondet (C a) (M a) (T a)
+
+We repeat the definition of the type class `With` because the current
+implementation of GHC does not allow equality constraints in
+super-class constraints. We would prefer to define this class as
+follows:
+
+    class (With [Untyped cs m] a, m ~ Mon [Untyped cs m] a) => WithUnique a
+     where
+      withUnique :: a -> [Untyped cs m] -> Nondet cs m (Typ [Untyped cs m] a)
+      withUnique = with
+
+So it is just a copy of the type class `With` where the argument type
+is specialized to use the same monad.
+
+> instance WithUntyped (Nondet cs m a)
+>  where
+>   type C (Nondet cs m a) = cs
+>   type M (Nondet cs m a) = m
+>   type T (Nondet cs m a) = a
+>
+>   withUntyped = const
+>
+> instance (WithUntyped a, cs ~ C a, m ~ M a)
+>        => WithUntyped (Nondet cs m b -> a)
+>  where
+>   type C (Nondet cs m b -> a) = C a
+>   type M (Nondet cs m b -> a) = M a
+>   type T (Nondet cs m b -> a) = T a
+>
+>   withUntyped alt (x:xs) = withUntyped (alt (Typed x)) xs
+>   withUntyped _ _ = error "LazyNondet.withUntyped: too few arguments"
+
+These instances define the overloaded function `withUntyped` that has
+all of the following types at the same time:
+
+    withUntyped :: Nondet cs m a
+                -> [Untyped cs m] -> Nondet cs m a
+
+    withUntyped :: (Nondet cs m a -> Nondet cs m b)
+                -> [Untyped cs m] -> Nondet cs m b
+
+    withUntyped :: (Nondet cs m a -> Nondet cs m b -> Nondet cs m c)
+                -> [Untyped cs m] -> Nondet cs m c
+    ...
+
+If the function given as first argument has n arguments, then the
+application of `withUntyped` to this function consumes n elements of
+the list of untyped values and yields the result of applying the given
+function to typed versions of these values.
+
+> newtype Match a cs m b = Match { unMatch :: (ConIndex, cs -> Branch cs m b) }
+> data Branch cs m a =
+>   forall t . (WithUntyped t, cs ~ C t, m ~ M t, a ~ T t) => Branch t
+>
+> match :: (ConsRep a, WithUntyped b)
+>       => a -> (C b -> b) -> Match t (C b) (M b) (T b)
+> match c alt = Match (constrIndex (consRep c), Branch . alt)
+
+The operation `match` is used to build destructor functions for
+non-deterministic values that can be used with `caseOf`.
+
+> caseOf :: (MonadSolve cs m m, MonadConstr Choice m)
+>        => Nondet cs m a -> [Match a cs m b] -> cs -> Nondet cs m b
+> caseOf x bs = caseOf_ x bs failure
+>
+> caseOf_ :: (MonadSolve cs m m, MonadConstr Choice m)
+>         => Nondet cs m a -> [Match a cs m b] -> Nondet cs m b
+>         -> cs -> Nondet cs m b
+> caseOf_ x bs def =
+>   withHNF x $ \hnf cs ->
+>   case hnf of
+>     FreeVar _ y -> caseOf_ (Typed y) bs def cs
+>     Delayed res -> caseOf_ (Typed (res cs)) bs def cs
+>     Cons _ idx args ->
+>       maybe def (\b -> branch (b cs) args) (lookup idx (map unMatch bs))
+>
+> branch :: Branch cs m a -> [Untyped cs m] -> Nondet cs m a
+> branch (Branch alt) = withUntyped alt
+
+We provide operations `caseOf_` and `caseOf` (with and without a
+default alternative) for more convenient pattern matching. The untyped
+values are hidden so functional-logic code does not need to match on
+the `Cons` constructor explicitly. However, using this combinator
+causes an additional slowdown because of the list lookup. It remains
+to be checked how big the slowdown of using `caseOf` is compared to
+using `withHNF` directly.
+
diff --git a/src/Data/LazyNondet/Narrowing.lhs b/src/Data/LazyNondet/Narrowing.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/Narrowing.lhs
@@ -0,0 +1,71 @@
+% Logic Variables and Narrowing
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+> {-# LANGUAGE
+>       FlexibleContexts,
+>       MultiParamTypeClasses
+>   #-}
+>
+> module Data.LazyNondet.Narrowing (
+>
+>   unknown, Narrow(..), NarrowPolicy(..)
+>
+> ) where
+>
+> import Data.LazyNondet.Types
+>
+> import Control.Monad.Constraint
+> import Control.Monad.Constraint.Choice
+>
+> unknown :: (MonadConstr Choice m, Narrow cs a) => cs -> ID -> Nondet cs m a
+> unknown cs u = freeVar u (narrowWithPolicy cs u)
+
+The application of `unknown` to a constraint store and a unique
+identifier represents a logic variable of an arbitrary type. 
+
+> class ChoiceStore cs => Narrow cs a
+>  where
+>   narrowPolicy :: NarrowPolicy cs a
+>   narrowPolicy = OnDemand
+>
+>   narrow :: MonadConstr Choice m => cs -> ID -> Nondet cs m a
+
+Logic variables of type `a` can be narrowed to head-normal form if
+there is an instance of the type class `Narrow`. A constraint store
+may be used to find the possible results which are returned in a monad
+that supports choices. Usually, `narrow` will be implemented as a
+non-deterministic generator using `oneOf`, but for specific types
+different strategies may be implemented.
+
+The default policy is to narrow on demand in order to avoid
+unnessesary choices in shared free variables that can lead to
+exponential explosion of the search space.
+
+A `NarrowPolicy` specifies whether a logic variable should be
+
+ * narrowed whenever it is demanded according the current constraint
+   store or
+
+ * narrowed only on creation and shared on every demand.
+
+> data NarrowPolicy cs a = OnDemand | OnCreation
+
+Using `OnDemand` can avoid unnessesary branching when accessing a
+variable with an updated constraint store. Using `OnCreation` will
+avoid the reexecution of a non-deterministic generator.
+
+> narrowWithPolicy :: (MonadConstr Choice m, Narrow cs a)
+>                  => cs -> ID -> Nondet cs m a
+> narrowWithPolicy cs u = x
+>  where
+>   x = case policy x of
+>         OnDemand   -> delayed (`narrow`u)
+>         OnCreation -> narrow cs u
+>
+> policy :: Narrow cs a => Nondet cs m a -> NarrowPolicy cs a
+> policy _ = narrowPolicy
+
+The function `narrowWithPolicy` narrows a logic variable or creates a
+delayed execution that will be performed whenever the variable is
+demanded. The definition uses a helper function in order to constrain
+the type of the narrowing policy.
diff --git a/src/Data/LazyNondet/Primitive.lhs b/src/Data/LazyNondet/Primitive.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/Primitive.lhs
@@ -0,0 +1,118 @@
+% Primitive Generic Functions on Lazy Non-Deterministic Data
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+> {-# LANGUAGE
+>       FlexibleContexts
+>   #-}
+>
+> module Data.LazyNondet.Primitive (
+>
+>   nondet, prim, groundNormalForm, partialNormalForm,
+>
+>   prim_eq
+>
+> ) where
+>
+> import Data.Data
+> import Data.Generics.Twins
+> import Data.LazyNondet.Types
+>
+> import Control.Monad.State
+> import Control.Monad.Constraint
+> import Control.Monad.Constraint.Choice
+>
+> import Unique
+> import UniqSupply
+>
+> prim :: Data a => NormalForm -> a
+> prim (Var u) = error $ "demand on logic variable " ++ show u
+> prim (NormalForm con args) =
+>   snd (gmapAccumT perkid args (fromConstr con))
+>  where
+>   perkid ts _ = (tail ts, prim (head ts))
+
+The operation `prim` translates a normal form into a primitive Haskell
+value. Free logic variables are translated into a call to `error` so
+the result is a partial value if the argument contains logic
+variables.
+
+> generic :: Data a => a -> NormalForm
+> generic x = NormalForm (toConstr x) (gmapQ generic x)
+>
+> nf2hnf :: Monad m => NormalForm -> Untyped cs m
+> nf2hnf (Var _) = error $ "Primitive.nf2hnf: cannot convert logic variable"
+> nf2hnf (NormalForm con args) = return (mkHNF con (map nf2hnf args))
+>
+> nondet :: (Monad m, Data a) => a -> Nondet cs m a
+> nondet = Typed . nf2hnf . generic
+
+We also provide a generic operation `nondet` to translate instances of
+the `Data` class into non-deterministic data.
+
+> groundNormalForm :: MonadSolve cs m m' => Nondet cs m a -> cs -> m' NormalForm
+> groundNormalForm  = evalStateT . gnf . untyped
+>
+> partialNormalForm :: (MonadSolve cs m m', ChoiceStore cs)
+>                   => Nondet cs m a -> cs -> m' NormalForm
+> partialNormalForm = evalStateT . pnf . untyped
+
+The `...NormalForm` functions evaluate a non-deterministic value and
+lift all non-deterministic choices to the top level. The results are
+deterministic values and can be converted into their Haskell
+representation. Partial normal forms may contain unbound logic
+variables while ground normal forms are data terms.
+
+> gnf :: MonadSolve cs m m' => Untyped cs m -> StateT cs m' NormalForm
+> gnf = nf (\_ _ -> Just ()) NormalForm mkVar
+>
+> mkVar :: ID -> a -> NormalForm
+> mkVar (ID us) _ = Var (uniqFromSupply us)
+>
+> pnf :: (MonadSolve cs m m', ChoiceStore cs)
+>     => Untyped cs m -> StateT cs m' NormalForm
+> pnf x = nf lookupChoice ((return.).mkHNF) ((return.).FreeVar) x
+>     >>= nf lookupChoice NormalForm mkVar
+
+To compute ground normal forms, we ignore free variables and narrow
+them to ground terms. To compute partial normal forms, we do not
+narrow unbound variables and in a second phase bind those variables
+that were bound after we have visited them. For example, when
+computing the normal form of `let x free in (x,not x)` we don't know
+that `x` will be bound in the result when we encounter it for the
+first time.
+
+> nf :: MonadSolve cs m m'
+>    => (Unique -> cs -> Maybe a)
+>    -> (Constr -> [nf] -> nf)
+>    -> (ID -> Untyped cs m -> nf)
+>    -> Untyped cs m -> StateT cs m' nf
+> nf lkp cns fv x = do
+>   hnf <- solve x
+>   case hnf of
+>     FreeVar u@(ID us) y ->
+>       get >>= maybe (return (fv u y)) (const (nf lkp cns fv y))
+>             . lkp (uniqFromSupply us)
+>     Delayed resume -> get >>= nf lkp cns fv . resume
+>     Cons typ idx args -> do
+>       nfs <- mapM (nf lkp cns fv) args
+>       return (cns (indexConstr typ idx) nfs)
+
+The `nf` function is used by all normal-form functions and performs al
+the work.
+
+> prim_eq :: MonadSolve cs m m
+>         => Untyped cs m -> Untyped cs m -> StateT cs m Bool
+> prim_eq x y = do
+>   Cons _ ix xs <- solve x
+>   Cons _ iy ys <- solve y
+>   if ix==iy then all_eq xs ys else return False
+>  where
+>   all_eq [] [] = return True
+>   all_eq (v:vs) (w:ws) = do
+>     eq <- prim_eq v w
+>     if eq then all_eq vs ws else return False
+>   all_eq _ _ = return False
+
+We provide a generic comparison function for untyped non-deterministic
+data that is used to define a typed equality test in the
+`Data.LazyNondet.Bool` module.
diff --git a/src/Data/LazyNondet/Types.lhs b/src/Data/LazyNondet/Types.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/Types.lhs
@@ -0,0 +1,128 @@
+% Basic Types for Lazy Non-Deterministic Data
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+This module defines the basic types to represent lazy
+non-deterministic data.
+
+> {-# LANGUAGE
+>       PatternGuards,
+>       FlexibleInstances
+>   #-}
+>
+> module Data.LazyNondet.Types (
+>
+>   ID(..), NormalForm(..), HeadNormalForm(..), Untyped, Nondet(..),
+>
+>   mkHNF, freeVar, delayed
+>
+> ) where
+>
+> import Data.Data
+>
+> import Control.Monad.Constraint
+>
+> import Unique
+> import UniqSupply
+>
+> newtype ID = ID UniqSupply
+>
+> data NormalForm = NormalForm Constr [NormalForm] | Var Unique
+
+The normal form of data is represented by the type `NormalForm` which
+defines a tree of constructors and logic variables. The type `Constr`
+is a representation of constructors defined in the `Data.Generics`
+package. With generic programming we can convert between Haskell data
+types and the `NormalForm` type.
+
+> data HeadNormalForm cs m
+>   = Cons DataType ConIndex [Untyped cs m]
+>   | FreeVar ID (Untyped cs m)
+>   | Delayed (cs -> Untyped cs m)
+>
+> type Untyped cs m = m (HeadNormalForm cs m)
+
+Data in lazy functional-logic programs is evaluated on demand. The
+evaluation of arguments of a constructor may lead to different
+non-deterministic results. Hence, we use a monad around every
+constructor in the head-normal form of a value.
+
+> newtype Nondet cs m a = Typed { untyped :: Untyped cs m }
+
+Untyped non-deterministic data can be phantom typed in order to define
+logic variables by overloading. The phantom type must be the Haskell
+data type that should be used for conversion into primitive data.
+
+> mkHNF :: Constr -> [Untyped cs m] -> HeadNormalForm cs m
+> mkHNF c args = Cons (constrType c) (constrIndex c) args
+
+In head-normal forms we split the constructor representation into a
+representation of the data type and the index of the constructor, to
+enable pattern matching on the index.
+
+Free (logic) variables are represented by `Unknown u x` where `u` is a
+uniqe identifier and `x` represents the result of narrowing the
+variable according to the constraint store passed to the operation
+that creates the variable.
+
+> freeVar :: Monad m => ID -> Nondet cs m a -> Nondet cs m a
+> freeVar u = Typed . return . FreeVar u . untyped
+
+The function `freeVar` is used to put a name around a narrowed free
+variable.
+
+> delayed :: Monad m => (cs -> Nondet cs m a) -> Nondet cs m a
+> delayed resume = Typed . return . Delayed $ (untyped . resume)
+
+With `delayed` computations can be delayed to be reexecuted with the
+current constraint store whenever they are demanded. This is useful to
+avoid unessary branching when narrowing logic variables. Use with
+care: `delayed` intentionally destroys sharing!
+
+`Show` Instances
+----------------
+
+> instance Show (HeadNormalForm cs [])
+>  where
+>   show (FreeVar (ID u) _) = show (uniqFromSupply u)
+>   show (Delayed _) = "<delayed>"
+>   show (Cons typ idx args) 
+>     | null args = show con
+>     | otherwise = unwords (("("++show con):map show args++[")"])
+>    where con = indexConstr typ idx
+>
+> instance Show (Nondet cs [] a)
+>  where
+>   show = show . untyped
+>
+> instance Show (Nondet cs (ConstrT cs []) a)
+>  where
+>   show = show . untyped
+>
+> instance Show (HeadNormalForm cs (ConstrT cs []))
+>  where
+>   show (FreeVar (ID u) _)  = show (uniqFromSupply u)
+>   show (Delayed _)         = "<delayed>"
+>   show (Cons typ idx [])   = show (indexConstr typ idx)
+>   show (Cons typ idx args) =
+>     "("++show (indexConstr typ idx)++" "++unwords (map show args)++")" 
+
+To simplify debugging, we provide `Show` instances for head-normal
+forms and non-deterministic values.
+
+> instance Show NormalForm
+>  where
+>   showsPrec _ (Var u) = shows u
+>   showsPrec _ (NormalForm cons []) = shows cons
+>   showsPrec n x@(NormalForm cons args)
+>     | Just xs <- fromList x = shows xs
+>     | n == 0    = shows cons . foldr1 (\y z -> (' ':).y.z) (map shows args)
+>     | otherwise = ('(':) . shows x . (')':)
+>
+> fromList :: NormalForm -> Maybe [NormalForm]
+> fromList (NormalForm cons args)
+>   | show cons == "[]" = Just []
+>   | show cons == "(:)", [x,l] <- args, Just xs <- fromList l = Just (x:xs)
+> fromList _ = Nothing
+
+For normal forms we provide a custum `Show` instance because we want
+to use it to print partial values in the evaluator.
diff --git a/src/Data/LazyNondet/Types/Bool.lhs b/src/Data/LazyNondet/Types/Bool.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/Types/Bool.lhs
@@ -0,0 +1,54 @@
+% Lazy Non-Deterministic Bools
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+This module provides non-deterministic booleans.
+
+> {-# LANGUAGE
+>       MultiParamTypeClasses,
+>       FlexibleInstances,
+>       FlexibleContexts
+>   #-}
+>
+> module Data.LazyNondet.Types.Bool where
+>
+> import Data.Data
+> import Data.LazyNondet
+> import Data.LazyNondet.Types
+> import Data.LazyNondet.Primitive
+>
+> import Control.Monad.State
+> import Control.Monad.Constraint
+> import Control.Monad.Constraint.Choice
+>
+> instance ConsRep Bool where consRep = toConstr
+>
+> true :: Monad m => Nondet cs m Bool
+> true = cons True
+>
+> pTrue :: (cs -> Nondet cs m a) -> Match Bool cs m a
+> pTrue = match True
+>
+> false :: Monad m => Nondet cs m Bool
+> false = cons False
+>
+> pFalse :: (cs -> Nondet cs m a) -> Match Bool cs m a
+> pFalse = match False
+
+In order to be able to use logic variables of boolean type, we make it
+an instance of the type class `Narrow`.
+
+> instance ChoiceStore cs => Narrow cs Bool
+>  where
+>   narrow = oneOf [false,true]
+
+Some operations with `Bool`s:
+
+> not :: (MonadSolve cs m m, MonadConstr Choice m)
+>     => Nondet cs m Bool -> cs -> Nondet cs m Bool
+> not x = caseOf_ x [pFalse (\_ -> true)] false
+>
+> (===) :: MonadSolve cs m m
+>       => Nondet cs m a -> Nondet cs m a -> cs -> Nondet cs m Bool
+> (x === y) cs = Typed $ do
+>   eq <- evalStateT (prim_eq (untyped x) (untyped y)) cs
+>   untyped $ if eq then true else false
diff --git a/src/Data/LazyNondet/Types/List.lhs b/src/Data/LazyNondet/Types/List.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/Types/List.lhs
@@ -0,0 +1,61 @@
+% Lazy Non-Deterministic Lists
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+This module provides non-deterministic lists.
+
+> {-# LANGUAGE
+>       MultiParamTypeClasses,
+>       FlexibleInstances,
+>       FlexibleContexts
+>   #-}
+>
+> module Data.LazyNondet.Types.List where
+>
+> import Data.Data
+> import Data.LazyNondet
+> import Data.LazyNondet.Types.Bool
+>
+> import Control.Monad.Constraint
+> import Control.Monad.Constraint.Choice
+>
+> instance ConsRep [()] where consRep = toConstr
+>
+> nil :: Monad m => Nondet cs m [a]
+> nil = cons ([] :: [()])
+>
+> pNil :: (cs -> Nondet cs m b) -> Match [a] cs m b
+> pNil = match ([] :: [()])
+>
+> infixr 5 ^:
+> (^:) :: Monad m => Nondet cs m a -> Nondet cs m [a] -> Nondet cs m [a]
+> (^:) = cons ((:) :: () -> [()] -> [()])
+>
+> pCons :: (cs -> Nondet cs m a -> Nondet cs m [a] -> Nondet cs m b)
+>       -> Match [a] cs m b
+> pCons = match ((:) :: () -> [()] -> [()])
+>
+> fromList :: Monad m => [Nondet cs m a] -> Nondet cs m [a]
+> fromList = foldr (^:) nil
+
+We can use logic variables of a list type if there are logic variables
+for the element type.
+
+> instance (ChoiceStore cs, Narrow cs a) => Narrow cs [a]
+>  where
+>   narrow cs = withUnique $ \u1 u2 -> 
+>                 oneOf [nil, unknown cs u1 ^: unknown cs u2] cs
+
+Some operations on lists:
+
+> null :: (MonadSolve cs m m, MonadConstr Choice m)
+>      => Nondet cs m [a] -> cs -> Nondet cs m Bool
+> null xs = caseOf_ xs [pNil (\_ -> true)] false
+>
+> head :: (MonadSolve cs m m, MonadConstr Choice m)
+>      => Nondet cs m [a] -> cs -> Nondet cs m a
+> head l = caseOf l [pCons (\_ x _ -> x)]
+>
+> tail :: (MonadSolve cs m m, MonadConstr Choice m)
+>      => Nondet cs m [a] -> cs -> Nondet cs m [a]
+> tail l = caseOf l [pCons (\_ _ xs -> xs)]
+
diff --git a/src/Data/LazyNondet/UniqueID.lhs b/src/Data/LazyNondet/UniqueID.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/UniqueID.lhs
@@ -0,0 +1,73 @@
+% Unique Identifiers
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+> {-# LANGUAGE
+>       TypeFamilies,
+>       FlexibleContexts,
+>       FlexibleInstances,
+>       MultiParamTypeClasses
+>   #-}
+>
+> module Data.LazyNondet.UniqueID (
+>
+>   initID, withUnique
+>
+> ) where
+>
+> import Data.LazyNondet.Types
+>
+> import Control.Monad
+>
+> import UniqSupply
+
+Non-deterministic computations need a supply of unique identifiers in
+order to constrain shared choices.
+
+> initID :: IO ID
+> initID = liftM ID $ mkSplitUniqSupply 'x'
+>
+> class With x a
+>  where
+>   type C x a
+>   type M x a :: * -> *
+>   type T x a
+>
+>   with :: a -> x -> Nondet (C x a) (M x a) (T x a)
+>
+> instance With x (Nondet cs m a)
+>  where
+>   type C x (Nondet cs m a) = cs
+>   type M x (Nondet cs m a) = m
+>   type T x (Nondet cs m a) = a
+>
+>   with = const
+>
+> instance With ID a => With ID (ID -> a)
+>  where
+>   type C ID (ID -> a) = C ID a
+>   type M ID (ID -> a) = M ID a
+>   type T ID (ID -> a) = T ID a
+>
+>   with f (ID us) = withUnique (f (ID vs)) (ID ws)
+>    where (vs,ws) = splitUniqSupply us
+>
+> withUnique :: With ID a => a -> ID -> Nondet (C ID a) (M ID a) (T ID a)
+> withUnique = with
+
+We provide an overloaded operation `withUnique` to simplify the
+distribution of unique identifiers when defining possibly
+non-deterministic operations. Non-deterministic operations have an
+additional argument for unique identifiers. The operation `withUnique`
+allows to consume an arbitrary number of unique identifiers hiding
+their generation. Conceptually, it has all of the following types at
+the same time:
+
+    Nondet m a -> ID -> Nondet m a
+    (ID -> Nondet m a) -> ID -> Nondet m a
+    (ID -> ID -> Nondet m a) -> ID -> Nondet m a
+    (ID -> ID -> ID -> Nondet m a) -> ID -> Nondet m a
+    ...
+
+We make use of type families because GHC considers equivalent
+definitions with functional dependencies illegal due to the overly
+restrictive "coverage condition".