diff --git a/FerryCore.cabal b/FerryCore.cabal
new file mode 100644
--- /dev/null
+++ b/FerryCore.cabal
@@ -0,0 +1,72 @@
+cabal-version: >=1.8
+Name:           FerryCore
+Version:        0.4.5
+category:       Database
+Synopsis:       Ferry Core Components
+Description:    The Ferry 2.0 Core
+                This package contains the core components of the Ferry compiler [1]. It lacks a parser
+                for the ferry language and the normalisation ferry front, and the conversion of ferry
+                front language to the ferry core language.
+                . 
+                It exposes the compiler parts that transform (un)typed ferry core into table algebra [2].
+                When provided an untyped ferrycore AST this ast must have the shape of a normalised
+                ferry program. When a typed ast is used as input it is required to be typed correctly as well.
+                The ferry compiler uses this package providing it untyped ferrycore. DSH [3] uses this
+                package providing a typed AST.
+                .
+                1. <http://www-db.informatik.uni-tuebingen.de/research/ferry>
+                .
+                2. <http://dbworld.informatik.uni-tuebingen.de/projects/pathfinder/wiki/Logical_Algebra>
+                .
+                3. <http://www-db.informatik.uni-tuebingen.de/files/publications/ferryhaskell.pdf>
+License:        BSD3
+License-file:   LICENSE
+Author:			Jeroen Weijers <jeroen.weijers@uni-tuebingen.de> Tom Schreiber <tom.schreiber@uni-tuebingen.de>
+Maintainer:		Jeroen Weijers <jeroen.weijers@uni-tuebingen.de>
+Build-Type:     Simple
+library
+    buildable:        True
+    build-depends:    TableAlgebra >= 0.1.5, base >= 4.2 && < 5, HaXml >= 1.20.2, pretty >= 1.0.1.1, parsec >= 2.1.0.1, mtl >= 2.0.1.0, containers >= 0.3.0.0, haskell98 >= 1.0.1.1, template-haskell >= 2.4.0.0
+    exposed-modules:  Database.Ferry.Syntax
+                      Database.Ferry.Compiler
+                      Database.Ferry.SyntaxTyped
+    hs-source-dirs:   src
+    GHC-Options:       -Wall -fno-warn-orphans -fno-warn-type-defaults -fno-warn-unused-do-bind 
+    other-modules:
+        Database.Ferry.Common.Render.Dot 
+        Database.Ferry.Common.Render.Pretty 
+        Database.Ferry.Compiler.Error.Error 
+        Database.Ferry.Compiler.ExecuteStep 
+        Database.Ferry.Compiler.Stages
+        Database.Ferry.Compiler.Transform
+        Database.Ferry.Compiler.Pipeline
+        Database.Ferry.Compiler.Stages.AlgebraToXMLStage 
+        Database.Ferry.Compiler.Stages.BoxingStage 
+        Database.Ferry.Compiler.Stages.RewriteStage 
+        Database.Ferry.Compiler.Stages.ToAlgebraStage 
+        Database.Ferry.Compiler.Stages.TypeInferStage 
+        Database.Ferry.Compiler.Types 
+        Database.Ferry.Core.Data.Core 
+        Database.Ferry.Core.Render.Dot 
+        Database.Ferry.Core.Render.Pretty 
+        Database.Ferry.TypedCore.Boxing.Boxing 
+        Database.Ferry.TypedCore.Convert.CoreToAlgebra 
+        Database.Ferry.TypedCore.Convert.Specialize 
+        Database.Ferry.TypedCore.Convert.Traverse 
+        Database.Ferry.TypedCore.Data.Instances 
+        Database.Ferry.TypedCore.Data.Substitution 
+        Database.Ferry.TypedCore.Data.Type 
+        Database.Ferry.TypedCore.Data.TypeClasses 
+        Database.Ferry.TypedCore.Data.TypedCore 
+        Database.Ferry.TypedCore.Data.TypeFunction 
+        Database.Ferry.TypedCore.Render.Dot 
+        Database.Ferry.TypedCore.Render.Pretty 
+        Database.Ferry.TypedCore.Rewrite.Combinators 
+        Database.Ferry.TypedCore.Rewrite.OpRewrite 
+        Database.Ferry.TypeSystem.AlgorithmW 
+        Database.Ferry.TypeSystem.ContextReduction 
+        Database.Ferry.TypeSystem.Prelude 
+        Database.Ferry.TypeSystem.Types 
+        Database.Ferry.TypeSystem.Unification
+        Database.Ferry.Common.Data.Base
+        Database.Ferry.Impossible 
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,27 @@
+Copyright (c) Eberhard Karls Universität Tübingen 2010
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,4 @@
+import Distribution.Simple
+
+main = defaultMain
+
diff --git a/src/Database/Ferry/Common/Data/Base.hs b/src/Database/Ferry/Common/Data/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Common/Data/Base.hs
@@ -0,0 +1,27 @@
+{- | 
+This module contains some datatypes and functions that are used at various stages in the compiler.
+-}
+module Database.Ferry.Common.Data.Base where
+
+-- | Identifiers are represented as strings    
+type Identifier = String
+
+-- | Constant values
+data Const = CInt Integer
+           | CFloat Double
+           | CBool Bool
+           | CString String
+           | CUnit
+    deriving (Show, Eq)
+
+-- | Type class for extracting all variables that occur in a value of type a
+class VarContainer a where
+    vars :: a -> [Identifier]
+
+-- | Print constants    
+toString :: Const -> String
+toString (CInt i) = show i
+toString (CFloat d) = show d
+toString (CBool b) = show b
+toString (CString s) = s
+toString (CUnit) = "()"
diff --git a/src/Database/Ferry/Common/Render/Dot.hs b/src/Database/Ferry/Common/Render/Dot.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Common/Render/Dot.hs
@@ -0,0 +1,153 @@
+{-# LANGUAGE TypeSynonymInstances #-}
+{-| Infrastructure for generating Dot graphics files.
+-}
+module Database.Ferry.Common.Render.Dot where
+    
+import Database.Ferry.Compiler.Error.Error
+
+import Control.Monad.Error
+import Control.Monad.Writer
+import Control.Monad.State
+
+import qualified Data.List as L
+
+-- | Class for transforming values into either an error or a string representing a dot file.
+class Dotify a where
+  dot :: a -> Either FerryError String
+
+-- | Dot files are internally represented as a list of nodes and a list of edges
+data DotFile = DotFile [Node] [Edge]
+
+-- | A dot Id is just string
+type Id = String
+
+-- | A dot Node has an id (unique) and a list of properties decribing its shape
+data Node = Node Id [NodeProp]
+
+-- | An edge runs from one node to one or more others identified by unique ids
+data Edge = Edge Id [Id]
+
+-- | Node properties describing shape of a node
+data NodeProp = Label Label
+              | Shape Shape
+              | Color Color
+              | TextColor Color
+
+{- | A dot label comes in three forms:
+a primitive label (just a string) SLabel
+a horizontally list of labels HLabel
+and a vertically ordered list of labels VLabel
+-}
+data Label = SLabel String
+           | HLabel [Label]
+           | VLabel [Label]
+
+-- | The shape of a dot node           
+data Shape = Rect
+           | Circle
+           | Oval
+           | Triangle
+
+-- | Colors           
+data Color = Red
+           | Blue
+           | Green
+           | Yellow
+           | Black
+           | White
+           | Gray
+
+{- | Dot monad
+While generating a dot file it is most convenient to do this in a monadic environment.
+The inner state monad contains a supply that is used to generate unique identifiers.
+In the inner Writer monad we store all the edges, the second writer monad contains
+all the nodes. The error monad is used to register any eventual problems, while
+preserving the state of the inner monads.
+-}              
+type Dot = ErrorT FerryError (WriterT [Node] (WriterT [Edge] (State Int)))
+
+-- | Generate a new node with the given nodeproperties, returns the new
+-- fresh id in the Dot environment
+node :: [NodeProp] -> Dot Id
+node props = do
+                    i <- getFreshId
+                    addNode $ Node i props
+                    return i
+
+-- | Generate an edge from arg1 to the nodes in arg2 and register it in the dot environment.
+edge :: Id -> [Id] -> Dot ()
+edge i is = addEdge $ Edge i is
+
+-- | Given a dot environment generate either the error that the computation in the environment yields
+-- or the resulting dot file as a string.
+runDot :: Dot a -> Either FerryError String
+runDot d = case r of
+            Left err -> Left err
+            Right _  -> Right $ dotFile ns es 
+ where (((r, ns), es), _) = flip runState 0 $ runWriterT $ runWriterT $ runErrorT d
+
+-- | Given a list of nodes and a list of edges generate a dot graph
+dotFile :: [Node] -> [Edge] -> String
+dotFile ns es = "digraph g {\nordering=out;" ++ concatMap dotNode ns ++ concatMap dotEdge es ++ "}"
+
+-- | Generate the line that describes an edge in a dot file
+dotEdge :: Edge -> String
+dotEdge (Edge i ts) = concat [i ++ " -> " ++ t ++ ";\n" | t <- ts]
+
+-- | Generate the line that describes a node in a dot file
+dotNode :: Node -> String
+dotNode (Node i props) = i ++ "[" ++ (concat $ L.intersperse "," $ map propsDot props) ++"];\n"
+
+-- | Transform the properties into their dot representation
+propsDot :: NodeProp -> String
+propsDot (Shape Rect)     = "shape=record" 
+propsDot (Shape Circle)   = "shape=circle"
+propsDot (Shape Oval)     = "shape=ellipse"
+propsDot (Shape Triangle) = "shape=triangle"
+propsDot (Color Red)      = "fillcolor=red,style=filled"
+propsDot (Color Blue)     = "fillcolor=blue,style=filled"
+propsDot (Color Green)    = "fillcolor=green,style=filled"
+propsDot (Color Yellow)   = "fillcolor=yellow,style=filled"
+propsDot (Color Black)    = "fillcolor=black,style=filled"
+propsDot (Color White)    = "fillcolor=white,style=filled"
+propsDot (Color Gray)     = "fillcolor=gray,style=filled"
+propsDot (TextColor Red)      = "color=red"
+propsDot (TextColor Blue)     = "color=blue"
+propsDot (TextColor Green)    = "color=green"
+propsDot (TextColor Yellow)   = "color=yellow"
+propsDot (TextColor Black)    = "color=black"
+propsDot (TextColor White)    = "color=white"
+propsDot (TextColor Gray)     = "color=gray"
+propsDot (Label l)            = "label=\"" ++ labelDot l ++ "\""
+
+-- | Transform a label into its dot representation
+labelDot :: Label -> String
+labelDot (SLabel s) = escape s 
+labelDot (HLabel ls) = concat $ L.intersperse " | " $ map labelDot ls
+labelDot (VLabel ls) = "{" ++ (concat $ L.intersperse " | " $ map (\l -> "{" ++ labelDot l ++ "}") ls) ++"}"
+
+-- | Add an edge to the dot environment
+addEdge :: Edge -> Dot ()
+addEdge e = lift $ lift $ tell [e]
+
+-- | Add a node to the dot environment
+addNode :: Node -> Dot ()
+addNode n = tell [n]
+
+-- | Generate a fresh identifier
+getFreshId :: Dot Id
+getFreshId = do
+              n <- get
+              put $ n + 1
+              return $ (:) 'n' $ show n
+
+-- | Escape certain characters in a dot file              
+escape :: String -> String
+escape (x:xs) = case x of
+                  '{' -> "\\{"
+                  '}' -> "\\}"
+                  '>' -> "\\>"
+                  '<' -> "\\<"
+                  _ -> [x]
+                 ++ escape xs
+escape []     = []
diff --git a/src/Database/Ferry/Common/Render/Pretty.hs b/src/Database/Ferry/Common/Render/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Common/Render/Pretty.hs
@@ -0,0 +1,26 @@
+-- | Infrastructure for pretty printing
+module Database.Ferry.Common.Render.Pretty where
+    
+import qualified Data.List as L
+
+-- | Class for pretty printing a value of a.
+class Pretty a where
+    -- | pretty function transforms a value of a into a string with identation i.
+    pretty :: a -> Int -> String
+
+-- | Shorthand for pretty without the identation argument
+prettyPrint :: Pretty a => a -> String
+prettyPrint e = pretty e 0
+
+-- | A newline followed by indenting n positions
+newLine :: Int -> String
+newLine n = "\n" ++ (take n $ repeat ' ')
+
+-- | maps its first argument over the third, then intersperses
+-- the result with the second argument, and finally concatenates everything.
+mapIntersperseConcat :: (a -> [b]) -> [b] -> [a] -> [b]
+mapIntersperseConcat f e l = concat $ L.intersperse e $ map f l
+
+-- | Pretty print the values xs then intersperse with a comma and transform it into one string
+intersperseComma :: Pretty a => [a] -> Int -> String
+intersperseComma xs i = concat $ L.intersperse ", " $ map (flip pretty i) xs
diff --git a/src/Database/Ferry/Compiler.hs b/src/Database/Ferry/Compiler.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler.hs
@@ -0,0 +1,16 @@
+-- | The compiler interface
+module Database.Ferry.Compiler
+( module Database.Ferry.Compiler.Stages,
+  FerryError(..), handleError,
+  typedCoreToAlgebra,
+  module Database.Ferry.Compiler.Types,
+  backEndPipeline, backEndPipeline',
+  executeStep 
+) where
+    
+import Database.Ferry.Compiler.Error.Error (FerryError (..), handleError)
+import Database.Ferry.Compiler.Stages
+import Database.Ferry.Compiler.Transform
+import Database.Ferry.Compiler.Types
+import Database.Ferry.Compiler.Pipeline
+import Database.Ferry.Compiler.ExecuteStep
diff --git a/src/Database/Ferry/Compiler/Error/Error.hs b/src/Database/Ferry/Compiler/Error/Error.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler/Error/Error.hs
@@ -0,0 +1,35 @@
+-- | Internal compiler errors
+module Database.Ferry.Compiler.Error.Error where
+
+import Control.Monad.Error
+import Database.Ferry.TypedCore.Data.Type
+
+import Text.ParserCombinators.Parsec (ParseError())
+
+-- | The FerryError datatype represents errors that occur during compilation
+data FerryError = NoSuchFile String
+                | ParserError ParseError
+                | UnificationError FType FType
+                | UnificationRecError [(RLabel, FType)] [(RLabel, FType)]
+                | ClassAlreadyDefinedError String
+                | SuperClassNotDefined String [String]
+                | ClassNotDefined String
+                | RecordDuplicateFields (Maybe String) [(RLabel, FType)]
+                | NotARecordType FType
+                | RecordWithoutI FType String
+                | UnificationOfRecordFieldsFailed RLabel RLabel
+                | UnificationFail RLabel RLabel
+                | ProcessComplete
+        deriving Show
+                
+-- | Just to satisfy the Error monad 
+instance Error FerryError where
+    noMsg = error "This function should not be used Error.hs noMsg"
+    strMsg = error "This function should not be used Error.hs strMsg"
+
+-- | Print an error message    
+handleError :: FerryError -> IO ()
+handleError ProcessComplete = return () -- Process complete just means everything was fine but the pipeline was ordered to stop early
+handleError (ParserError e) = putStrLn $ show e
+handleError e               = putStrLn $ show e
+     
diff --git a/src/Database/Ferry/Compiler/ExecuteStep.hs b/src/Database/Ferry/Compiler/ExecuteStep.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler/ExecuteStep.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-| The compilation process is build out of small steps, this module provides the infrastructure
+that executes one such step. -}
+module Database.Ferry.Compiler.ExecuteStep (executeStep) where
+    
+import Database.Ferry.Compiler.Types
+
+-- | Apply a compilation step to an expression of type a. The result of type b is returned in a phaseresult monad
+executeStep :: CompilationStep a b -> a -> PhaseResult b
+executeStep step i = do
+                            opts <- getConfig
+                            phaseHeader (stageName step) (stageMode step)
+                            b <- stageStep step i  -- stageStep step gets the function that is to be applied this phase
+                            mapM_ (createArtefacts b) $ stageArtefacts step
+                            if (mode opts == stageMode step)
+                             then endProcess
+                             else return b
+
+-- | The artefacts that can be generated by a compilationstep are generated by this function
+createArtefacts :: b -> (Artefact, String, b -> ArtefactResult) -> PhaseResult ()
+createArtefacts i (a, e, f) = do
+                                  opts <- getConfig
+                                  logMsg line
+                                  logMsg $ "Artefact creation stage for: " ++ (show a)
+                                  if elem a $ artefact opts
+                                   then do 
+                                         let file = case output opts of
+                                                  Nothing -> Nothing
+                                                  (Just file') -> Just $ file' ++ "." ++ e
+                                         logMsg "Creating artefact"
+                                         s <- artefactToPhaseResult $ f i
+                                         addFile file s
+                                         logMsg "Artefact creation done"
+                                         logMsg line
+                                         return ()
+                                   else do
+                                         logMsg "Artefact not required. Skipping artefact creation."
+                                         logMsg line
+                                         return ()
+
+-- | Helper function to generate the phaseheader in the log    
+phaseHeader :: Name -> Mode -> PhaseResult ()
+phaseHeader n s = do
+                     c <- getConfig
+                     logMsg line
+                     logMsg $ "Compiler stage: " ++ (show s)
+                     logMsg $ "Stage name: " ++ n
+                     logMsg "Compiling with the following options:"
+                     logMsg $ show c
+                     logMsg line
+                     return ()
diff --git a/src/Database/Ferry/Compiler/Pipeline.hs b/src/Database/Ferry/Compiler/Pipeline.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler/Pipeline.hs
@@ -0,0 +1,27 @@
+-- | Module describing the general core flow
+module Database.Ferry.Compiler.Pipeline (backEndPipeline, backEndPipeline') where
+
+import Database.Ferry.Compiler.Types
+import Database.Ferry.Core.Data.Core (CoreExpr)
+import qualified Database.Ferry.TypedCore.Data.TypedCore as T (CoreExpr)
+
+import Database.Ferry.Compiler.Stages
+    
+-- | The compiler pipeline. The given Core AST is transformed dependent on the configuration of the Phaseresult
+--   monad.
+backEndPipeline :: CoreExpr -> PhaseResult ()
+backEndPipeline c =  typeInferPhase c >>=
+                     rewritePhase >>=
+                     boxingPhase >>=
+                     algebraPhase >>=
+                     xmlPhase >>
+                     return ()
+                     
+-- | The compiler pipeline. Some tools might already provide a typed AST, is the same as the normal backEndPipeline
+-- without type inferencing.
+backEndPipeline' :: T.CoreExpr -> PhaseResult ()
+backEndPipeline' c = rewritePhase c >>=
+                     boxingPhase >>=
+                     algebraPhase >>=
+                     xmlPhase >>
+                     return ()                     
diff --git a/src/Database/Ferry/Compiler/Stages.hs b/src/Database/Ferry/Compiler/Stages.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler/Stages.hs
@@ -0,0 +1,10 @@
+{-| Compiler stages of the backend-}
+module Database.Ferry.Compiler.Stages (xmlPhase, boxingPhase, rewritePhase, 
+                              algebraPhase, typeInferPhase) where
+    
+    
+import Database.Ferry.Compiler.Stages.AlgebraToXMLStage
+import Database.Ferry.Compiler.Stages.BoxingStage
+import Database.Ferry.Compiler.Stages.RewriteStage
+import Database.Ferry.Compiler.Stages.ToAlgebraStage
+import Database.Ferry.Compiler.Stages.TypeInferStage 
diff --git a/src/Database/Ferry/Compiler/Stages/AlgebraToXMLStage.hs b/src/Database/Ferry/Compiler/Stages/AlgebraToXMLStage.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler/Stages/AlgebraToXMLStage.hs
@@ -0,0 +1,22 @@
+{- | This module wraps the transform algebra into xml compilation stage
+-}
+module Database.Ferry.Compiler.Stages.AlgebraToXMLStage (xmlPhase) where
+    
+import Database.Ferry.Compiler.Types
+import Database.Ferry.Compiler.ExecuteStep
+
+import Database.Ferry.Algebra(AlgPlan, transform)
+
+import Database.Ferry.TypedCore.Data.Type
+
+xmlPhase :: (Qual FType, AlgPlan) -> PhaseResult String
+xmlPhase (_ :=> t, p) = executeStep xmlStage $ case t of
+                                                FList _ -> (True, p)
+                                                _       -> (False, p)
+
+xmlStage :: CompilationStep (Bool, AlgPlan) String
+xmlStage = CompilationStep "ToXML" AlgebraXML step artefacts
+    where
+        step :: (Bool, AlgPlan) -> PhaseResult String
+        step = return . show . transform 
+        artefacts = [(XML, "xml", return)]
diff --git a/src/Database/Ferry/Compiler/Stages/BoxingStage.hs b/src/Database/Ferry/Compiler/Stages/BoxingStage.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler/Stages/BoxingStage.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE TemplateHaskell #-}
+{- | This module wraps the boxing stage. Boxing is performed to ensure that nested lists are 
+   handled in a separate table in the database. 
+-}
+module Database.Ferry.Compiler.Stages.BoxingStage (boxingPhase) where
+    
+import Database.Ferry.Compiler.Types
+import Database.Ferry.Compiler.ExecuteStep
+
+import Database.Ferry.TypeSystem.Prelude
+import Database.Ferry.TypedCore.Render.Dot
+import Database.Ferry.Common.Render.Dot
+                                           
+import Database.Ferry.TypedCore.Data.TypedCore
+import Database.Ferry.TypedCore.Boxing.Boxing
+
+import Database.Ferry.Impossible
+
+boxingPhase :: CoreExpr -> PhaseResult CoreExpr
+boxingPhase e = executeStep inferStage e
+
+inferStage :: CompilationStep CoreExpr CoreExpr
+inferStage = CompilationStep "Boxing" Boxing step artefacts
+    where
+        step :: CoreExpr -> PhaseResult CoreExpr
+        step e = return $ runBoxing primitives e
+        artefacts = [(DotBox ,"dot", \s -> return $ makeDot s)]
+        
+makeDot :: CoreExpr -> String
+makeDot c = case runDot $ toDot c of
+            Right s -> s
+            Left _ -> $impossible
diff --git a/src/Database/Ferry/Compiler/Stages/RewriteStage.hs b/src/Database/Ferry/Compiler/Stages/RewriteStage.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler/Stages/RewriteStage.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE TemplateHaskell #-}
+-- | This module wraps the rewrite stage, performing some rewrites on the ferry core AST.
+module Database.Ferry.Compiler.Stages.RewriteStage (rewritePhase) where
+    
+import Database.Ferry.Compiler.Types
+import Database.Ferry.Compiler.ExecuteStep
+
+import Database.Ferry.TypedCore.Render.Dot
+import Database.Ferry.Common.Render.Dot
+                                           
+import Database.Ferry.TypedCore.Data.TypedCore
+import Database.Ferry.TypedCore.Rewrite.OpRewrite
+
+import Database.Ferry.Impossible
+
+rewritePhase :: CoreExpr -> PhaseResult CoreExpr
+rewritePhase e = executeStep inferStage e
+
+inferStage :: CompilationStep CoreExpr CoreExpr
+inferStage = CompilationStep "Rewrite" OpRewrite step artefacts
+    where
+        step :: CoreExpr -> PhaseResult CoreExpr
+        step e = return $ rewrite e
+        artefacts = [(DotRewrite ,"dot", \s -> return $ makeDot s)]
+        
+makeDot :: CoreExpr -> String
+makeDot c = case runDot $ toDot c of
+            Right s -> s
+            Left _ -> $impossible
diff --git a/src/Database/Ferry/Compiler/Stages/ToAlgebraStage.hs b/src/Database/Ferry/Compiler/Stages/ToAlgebraStage.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler/Stages/ToAlgebraStage.hs
@@ -0,0 +1,24 @@
+-- | This module wraps the stage that translates ferry core into an algebraic graph
+module Database.Ferry.Compiler.Stages.ToAlgebraStage (algebraPhase) where
+    
+import Database.Ferry.Compiler.Types
+import Database.Ferry.Compiler.ExecuteStep
+
+import Database.Ferry.Algebra(runGraph, initLoop, AlgPlan)
+
+import Database.Ferry.TypedCore.Data.Instances()
+import Database.Ferry.TypedCore.Convert.CoreToAlgebra
+import Database.Ferry.TypedCore.Data.Type
+                                           
+import Database.Ferry.TypedCore.Data.TypedCore
+
+algebraPhase :: CoreExpr -> PhaseResult (Qual FType, AlgPlan)
+algebraPhase e = executeStep algebraStage e
+
+algebraStage :: CompilationStep CoreExpr (Qual FType, AlgPlan)
+algebraStage = CompilationStep "ToAlg" Algebra step artefacts
+    where
+        step :: CoreExpr -> PhaseResult (Qual FType, AlgPlan)
+        step e = let eTy = typeOf e
+                  in return $ (eTy, runGraph initLoop $ coreToAlgebra e)
+        artefacts = []
diff --git a/src/Database/Ferry/Compiler/Stages/TypeInferStage.hs b/src/Database/Ferry/Compiler/Stages/TypeInferStage.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler/Stages/TypeInferStage.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE TemplateHaskell #-}
+-- | This module wraps the transformation stage from ferry core, to typed ferry core.
+module Database.Ferry.Compiler.Stages.TypeInferStage (typeInferPhase) where
+    
+import Database.Ferry.Compiler.Types
+import Database.Ferry.Compiler.ExecuteStep
+
+import Database.Ferry.Common.Render.Pretty
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.TypeSystem.Prelude
+import Database.Ferry.TypedCore.Render.Dot
+import Database.Ferry.Common.Render.Dot
+import Database.Ferry.TypedCore.Convert.Specialize
+
+import qualified Database.Ferry.Core.Data.Core as C
+import Database.Ferry.TypedCore.Data.TypedCore
+import Database.Ferry.TypeSystem.AlgorithmW
+
+import Database.Ferry.Impossible
+
+typeInferPhase :: C.CoreExpr -> PhaseResult CoreExpr
+typeInferPhase e = executeStep inferStage e
+
+inferStage :: CompilationStep C.CoreExpr CoreExpr
+inferStage = CompilationStep "TypeInfer" TypeInfer step artefacts
+    where
+        step :: C.CoreExpr -> PhaseResult CoreExpr
+        step e = let (res, _) = typeInfer primitives e
+                  in case res of
+                       Left err -> newError err
+                       Right expr -> return $ groupNSpecialize expr
+        artefacts = [(Type ,"ty", \s -> return $ prettyPrint $ typeOf s)
+                    ,(DotType ,"dot", \s -> return $ makeDot s)]
+        
+makeDot :: CoreExpr -> String
+makeDot c = case runDot $ toDot c of
+            Right s -> s
+            Left _ -> $impossible
diff --git a/src/Database/Ferry/Compiler/Transform.hs b/src/Database/Ferry/Compiler/Transform.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler/Transform.hs
@@ -0,0 +1,24 @@
+-- | This module is exposed in the library allowing other applications to compile typedCore to relational algebra
+{-# LANGUAGE TemplateHaskell #-}
+module Database.Ferry.Compiler.Transform (typedCoreToAlgebra) where
+    
+import Database.Ferry.Compiler.Pipeline (backEndPipeline')
+import Database.Ferry.TypedCore.Data.TypedCore (CoreExpr)
+import Database.Ferry.Compiler.Types
+import Database.Ferry.Compiler.Error.Error
+import Database.Ferry.Impossible
+
+typedCoreToAlgebra :: CoreExpr -> String
+typedCoreToAlgebra = compile defaultConfig 
+
+-- | The compiler pipeline
+--   Note that there should be a monadic style for handling all the steps in the pipeline
+compile :: Config -> CoreExpr -> String
+compile opts inp = do
+                        let (r, _, f) = runPhase opts $ backEndPipeline' inp   
+                        case (r, f) of
+                            (Right (), [(_, o)]) -> o
+                            (Left ProcessComplete, [(_, o)]) -> o
+                            (Left err, _)       -> error $ show err
+                            _                   -> $impossible
+                            
diff --git a/src/Database/Ferry/Compiler/Types.hs b/src/Database/Ferry/Compiler/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Compiler/Types.hs
@@ -0,0 +1,164 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-| Types used by the compiler infrastructure-}
+module Database.Ferry.Compiler.Types where
+    
+import Control.Monad.Error
+import Control.Monad.Writer
+import Control.Monad.Reader
+
+import Database.Ferry.Compiler.Error.Error
+
+-- | The config datatype is used to store program flags given by the user 
+--   The compiler can be put in a 'Mode' that determines what sort of
+--   result the compilation process will result in.
+--   The 'Input' element is set to specify whether a file should be compiled or 
+--   input from the stdin
+--   The debug component is set to switch on debugging mode, debugging mode
+--   results in log information on the stdin and possibly extra compiler artifacts.
+data Config = Config {
+              mode :: Mode,
+              logFile :: Maybe String,
+              output :: Maybe String,
+              input :: Input,
+              artefact :: [Artefact],
+              debug :: Bool
+            }
+            deriving Show
+
+-- | The modes that are supported by the compiler.
+--   run ferryc -h to see a list of all options
+data Mode = Read
+          | Parse  -- ^ Parse mode will stop the compiler after the parsing phase
+          | Normalise 
+          | Transform
+          | TypeInfer
+          | OpRewrite
+          | Boxing
+          | Algebra
+          | AlgebraXML
+    deriving (Show, Eq)
+          
+data Artefact = Echo   -- ^ Echo mode prints the given input to the console
+              | PrettyAST -- ^ Pretty mode parses the given input and pretty prints the result
+              | PrettyNormalAST
+              | PrettyCore
+              | DotAST
+              | DotCore
+              | DotType
+              | DotRewrite
+              | DotBox
+              | DotAlg
+              | XML
+              | Type
+    deriving (Show, Eq)
+
+-- All possible artefacts
+allArtefacts :: [Artefact]
+allArtefacts = [Echo, PrettyAST, PrettyCore, DotAST, DotCore, DotType, DotBox, DotAlg, XML]
+
+-- | The input mode determines whether the source program is given through a file or via stdin
+data Input  = File String-- ^ File mode, the program is read from a file 
+            | Arg  -- ^ Argument mode, the program is given as input directly
+    deriving (Show, Eq)
+
+-- | The default configuration for the compiler
+defaultConfig :: Config
+defaultConfig = Config {
+                --  Standard 'Mode' is set to Full
+                mode        = AlgebraXML,
+                logFile     = Nothing,
+                output      = Nothing, 
+                --  By default the program is given through a File
+                input       = Arg,
+                -- Standard output is the empty list, denoting regular compilation proces
+                artefact    = [XML], 
+                --  Debug turned of by default
+                debug       = False 
+              }
+
+-- | The results of artefact generation are all collected in a reader monad
+-- The final result is written to disk or screen when compilation has succeeded
+type ArtefactResult = Reader Config String
+
+-- | Result of a compilation phase.
+-- The error monad is used in case something went wrong during compilation
+-- The first writer monad is used for logging purposes.
+-- The second writer monad is used to store the artefacts generated by the compiler
+-- And the reader monad stores the compiler configuration              
+type PhaseResult r = ErrorT FerryError (WriterT Log (WriterT [File] (Reader Config))) r
+
+-- | Name of an artefact file
+type FileName = String
+
+-- | Artefact file, the first element represents the output file, in case of nothing output is given
+-- on stdout. The second component is the file content.
+type File = (Maybe FileName, String)
+
+-- | Compilationstep datatype.
+-- A compilation step is a record containg a description (stageName field),
+-- the internal mode name (stageMode field),
+-- the actual stage computation (stageStep field) that transforms element of type a into a PhaseResult of type b
+-- and stage artefact generators, a list of function generating artefacts (stageArtefacts field).
+data CompilationStep a b  = CompilationStep { 
+                                stageName :: Name, 
+                                stageMode :: Mode,
+                                stageStep :: a -> PhaseResult b,
+                                stageArtefacts :: [(Artefact, String, b -> ArtefactResult)]
+                                }
+
+-- | Type synonym for a stage name type
+type Name = String
+
+-- | Every stage has a stage number
+type Stage = Int
+
+-- | The compilation log is just a string
+type Log = [String]
+
+-- | Lift the result of generating an artefact into the overall phase result type
+artefactToPhaseResult :: ArtefactResult -> PhaseResult String
+artefactToPhaseResult r = lift $ lift $ lift r
+
+-- | Get the compiler configuration
+getConfig :: PhaseResult Config
+getConfig = ask
+
+-- | Get the current log from a phaseresult
+getLog :: Config -> PhaseResult r -> Log
+getLog c n = (\(_, l, _) -> l) $ runPhase c n
+
+-- | Get the artefacts from the phaseresult            
+getFiles :: Config -> PhaseResult r -> [File]
+getFiles c n = (\(_, _, f) -> f) $ runPhase c n        
+
+-- | Execute a phaseresult under a given configuration,, resulting in triple of:
+-- 1.) An error or the result
+-- 2.) The compilation log
+-- 3.) The generated artefacts
+runPhase :: Config -> PhaseResult r -> (Either FerryError r, Log, [File])
+runPhase c n = (\((r, l), f) -> (r, l, f)) $ flip runReader c $ runWriterT $ runWriterT $ runErrorT n
+
+-- | Throw an error
+newError :: FerryError -> PhaseResult r
+newError e = ErrorT $ return $ Left e
+
+-- | Final log message when end of compilation is reached
+endProcess :: PhaseResult b
+endProcess = do
+                logMsg line
+                logMsg "Reached compilation target"
+                logMsg "Quiting compilation"
+                logMsg line
+                newError ProcessComplete
+
+-- | Seperator line for logging
+line :: String
+line = "--------------------------------------------------"
+
+-- | Log the message t
+logMsg :: (MonadWriter [t] m) => t -> m ()
+logMsg s = tell [s]
+
+-- | Add the given file with contents to the phaseresult.
+addFile :: Maybe FileName -> String -> PhaseResult ()
+addFile n c = lift $ lift $ tell [(n, c)]
diff --git a/src/Database/Ferry/Core/Data/Core.hs b/src/Database/Ferry/Core/Data/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Core/Data/Core.hs
@@ -0,0 +1,59 @@
+{-| Untyped core data type -}
+{-# LANGUAGE GADTs #-}
+module Database.Ferry.Core.Data.Core where
+
+import Database.Ferry.Common.Data.Base
+
+-- | An identifier is represented by a string
+type Ident = String
+
+-- | Operator constructor
+data Op where
+    Op :: String -> Op
+
+-- | Datatype for building untyped core ASTs
+data CoreExpr where
+    BinOp :: Op -> CoreExpr -> CoreExpr -> CoreExpr
+--    UnaOp :: Op -> CoreExpr -> CoreExpr
+    Constant :: Const -> CoreExpr
+    Var  :: String -> CoreExpr
+    App :: CoreExpr -> Param -> CoreExpr
+    Let :: String -> CoreExpr -> CoreExpr -> CoreExpr
+    Rec :: [RecElem] -> CoreExpr
+    Cons :: CoreExpr -> CoreExpr -> CoreExpr
+    Nil :: CoreExpr
+    Elem :: CoreExpr -> String -> CoreExpr
+    Table :: String -> [Column] -> [Key] -> CoreExpr
+    If :: CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
+
+-- | Record elements
+data RecElem where
+    RecElem :: String -> CoreExpr -> RecElem
+    
+-- | Function arguments
+-- In future, that is when defunctionalisation is implemented function arguments should just be expressions.
+data Param where
+     ParExpr :: CoreExpr -> Param
+     ParAbstr :: [String] -> CoreExpr -> Param
+{- 
+-- | Patterns   
+data Pattern where
+    PVar :: String -> Pattern
+    Pattern :: [String] -> Pattern
+-}
+  
+-- | Database table column
+data Column where
+     Column :: String -> Type -> Column
+
+-- | Database column type    
+data Type
+    = TInt 
+    | TFloat 
+    | TString 
+    | TBool
+    | TUnit
+
+-- | Database table key    
+data Key where
+    Key :: [String] -> Key
diff --git a/src/Database/Ferry/Core/Render/Dot.hs b/src/Database/Ferry/Core/Render/Dot.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Core/Render/Dot.hs
@@ -0,0 +1,97 @@
+-- | Provides Dotify instance for untyped core 
+module Database.Ferry.Core.Render.Dot() where
+
+import Database.Ferry.Common.Render.Dot    
+import Database.Ferry.Core.Data.Core
+import Database.Ferry.Common.Data.Base
+import Database.Ferry.Core.Render.Pretty
+
+import qualified Data.List as L
+
+
+instance Dotify CoreExpr where
+    dot e = runDot $ toDot e
+
+-- | Transform core expression to dot environment
+toDot :: CoreExpr -> Dot Id
+toDot (BinOp o e1 e2) = do
+                          id1 <- toDot e1
+                          id2 <- toDot e2
+                          let o' = (\(Op op) -> op) o
+                          nId <- node [Label $ SLabel o', Color Green, Shape Circle]
+                          edge nId [id1, id2]
+                          return nId
+toDot (Constant c) = let s = toString c
+                      in node [Label $ SLabel s, Color Yellow, Shape Triangle]
+toDot (Var i) = node [Label $ SLabel i, Color Red, Shape Triangle]
+toDot (App c ps) = do
+                     nId <- node [Label $ SLabel "$", Color Green, Shape Circle]
+                     fId <- toDot c
+                     pIds <- paramToDot ps
+                     edge nId [fId, pIds]
+                     return nId
+toDot (Let s e1 e2) = do
+                       nId <- node [Label $ SLabel "Let", Color Blue, Shape Rect]
+                       id0 <- node [Label $ SLabel s, Color Red, Shape Rect, TextColor White]
+                       id1 <- toDot e1
+                       id2 <- toDot e2
+                       edge nId [id0, id1, id2]
+                       return nId
+toDot (Rec es) = do
+                  nId <- node [Label $ SLabel "Rec", Color Blue, Shape Oval]
+                  eIds <- mapM recToDot es
+                  edge nId eIds
+                  return nId
+toDot (Cons e1 e2) = do
+                     nId <- node [Label $ SLabel "Cons", Color Blue, Shape Oval]
+                     eIdh <- toDot e1
+                     eIdt <- toDot e2
+                     edge nId [eIdh, eIdt]
+                     return nId
+toDot (Nil)      = node [Label $ SLabel "Nil", Color Blue, Shape Oval]
+toDot (Elem c s) = do
+                    nId <- node [Label $ SLabel ".", Color Green, Shape Circle]
+                    sId <- node [Label $ SLabel s, Color Red, Shape Triangle]
+                    cId <- toDot c
+                    edge nId [cId, sId]
+                    return nId
+toDot (Table n cs ks) = let label = VLabel $ ((HLabel [SLabel "Table:", SLabel n])
+                                            : [HLabel [SLabel $ n' ++ "::", SLabel $ prettyTy t ] | (Column n' t) <- cs])
+                                            ++ [SLabel $ keyToString k | k <- ks]
+                         in node [Shape Rect, Label label, Color Yellow]
+toDot (If e1 e2 e3) = do
+                        nId <- node [Label $ SLabel "If", Color Blue, Shape Circle]
+                        eId1 <- toDot e1
+                        eId2 <- toDot e2
+                        eId3 <- toDot e3
+                        edge nId [eId1, eId2, eId3]
+                        return nId
+                        
+-- | Convert function parameters to dot representations
+paramToDot :: Param -> Dot Id
+paramToDot (ParExpr e) = toDot e
+paramToDot (ParAbstr p e) = do
+                             nId <- node [Label $ SLabel "\\   ->", Color Blue, Shape Circle]
+                             pId <- node [Label $ SLabel (concat $ L.intersperse " " p), Color Red, Shape Triangle]
+                             eId <- toDot e
+                             edge nId [pId, eId]
+                             return nId
+
+{-
+-- | Convert a pattern to a dot node                             
+patToDot :: Pattern -> Dot Id
+patToDot (PVar s) = node [Label $ SLabel s, Color Red, Shape Triangle]
+patToDot (Pattern s) = node [Label $ SLabel $  "(" ++ (concat $ L.intersperse ", " s) ++ ")", Color Red, Shape Triangle]
+-}
+
+-- | Convert a record element to a dot node
+recToDot :: RecElem -> Dot Id
+recToDot (RecElem s e) = do
+                          nId <- node [Label $ SLabel s, Color Red, Shape Oval]
+                          eId <- toDot e
+                          edge nId [eId]
+                          return nId
+
+-- | Generate a string representation of a database key
+keyToString :: Key -> String
+keyToString (Key ks) = "(" ++ (concat $ L.intersperse ", " ks) ++ ")"
diff --git a/src/Database/Ferry/Core/Render/Pretty.hs b/src/Database/Ferry/Core/Render/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Core/Render/Pretty.hs
@@ -0,0 +1,15 @@
+-- | Pretty print instance for database types
+module Database.Ferry.Core.Render.Pretty where
+
+import Database.Ferry.Core.Data.Core
+import Database.Ferry.Common.Render.Pretty
+
+instance Pretty Type where
+    pretty a _ = prettyTy a
+
+prettyTy :: Type -> String
+prettyTy TUnit = "()"
+prettyTy TInt = "Int"
+prettyTy TFloat = "Float" 
+prettyTy TString = "String" 
+prettyTy TBool = "Bool"    
diff --git a/src/Database/Ferry/Impossible.hs b/src/Database/Ferry/Impossible.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Impossible.hs
@@ -0,0 +1,11 @@
+-- | Utility module for reporting impossible events
+module Database.Ferry.Impossible (impossible) where
+
+import qualified Language.Haskell.TH as TH
+
+impossible :: TH.ExpQ
+impossible = do
+  loc <- TH.location
+  let pos =  (TH.loc_filename loc, fst (TH.loc_start loc), snd (TH.loc_start loc))
+  let message = "ferry: Impossbile happend at " ++ show pos
+  return (TH.AppE (TH.VarE (TH.mkName "error")) (TH.LitE (TH.StringL message)))
diff --git a/src/Database/Ferry/Syntax.hs b/src/Database/Ferry/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/Syntax.hs
@@ -0,0 +1,16 @@
+{-# OPTIONS_GHC -fno-warn-unused-imports   #-}
+{-| Everything related to untyped core -}
+module Database.Ferry.Syntax {-# DEPRECATED "Use Database.Ferry.SyntaxTyped instead of this module. This module will not be available in future FerryCore releases." #-}
+(
+Ident,
+Identifier, Const (..), VarContainer(..),
+Op (..), CoreExpr (..), RecElem (..), Param (..), Column (..), Key (..), Type(..),
+Dotify(..),
+module Database.Ferry.Common.Render.Pretty
+)
+where
+import Database.Ferry.Common.Data.Base    
+import Database.Ferry.Core.Data.Core (Op (..), CoreExpr (..), RecElem (..), Param (..), Column (..), Key (..), Ident, Type(..))
+import Database.Ferry.Core.Render.Dot()
+import Database.Ferry.Common.Render.Dot(Dotify(..))
+import Database.Ferry.Common.Render.Pretty
diff --git a/src/Database/Ferry/SyntaxTyped.hs b/src/Database/Ferry/SyntaxTyped.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/SyntaxTyped.hs
@@ -0,0 +1,16 @@
+{-| Everything related to typed core-}
+module Database.Ferry.SyntaxTyped 
+(
+Ident,
+Identifier, Const (..),
+Op (..), CoreExpr (..), RecElem (..), Param (..), Column (..), Key (..),
+int, float, string, bool, list, var, rec, fn, genT, (.->), TyScheme (..), Qual (..), Pred (..), FType (..), RLabel (..), FTFn (..), HasType, typeOf,
+Dotify(..)
+)
+where
+import Database.Ferry.Common.Data.Base    
+import Database.Ferry.TypedCore.Data.TypedCore (Op (..), CoreExpr (..), RecElem (..), Param (..), Column (..), Key (..), Ident)
+import Database.Ferry.TypedCore.Data.Type (int, float, string, bool, list, var, rec, fn, genT, (.->), TyScheme (..), Qual (..), Pred (..), FType (..), RLabel (..), FTFn (..), HasType, typeOf)
+import Database.Ferry.TypedCore.Data.Instances() 
+import Database.Ferry.TypedCore.Render.Dot()
+import Database.Ferry.Common.Render.Dot
diff --git a/src/Database/Ferry/TypeSystem/AlgorithmW.hs b/src/Database/Ferry/TypeSystem/AlgorithmW.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypeSystem/AlgorithmW.hs
@@ -0,0 +1,220 @@
+{-| Infer types for a program, transform an untyped core AST into a typed core AST.
+Standard Algorithm W, with some modifications to deal with records.-}
+module Database.Ferry.TypeSystem.AlgorithmW (typeInfer) where
+
+import Database.Ferry.TypeSystem.Types    
+import qualified Database.Ferry.Core.Data.Core as C
+import Database.Ferry.TypedCore.Data.TypedCore
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.TypedCore.Data.Substitution 
+import Database.Ferry.Compiler.Error.Error
+import Database.Ferry.Common.Data.Base (Const (..)) 
+import Database.Ferry.TypeSystem.Unification
+import Database.Ferry.TypeSystem.ContextReduction
+
+
+import qualified Data.Set as S
+import qualified Data.List as L
+import qualified Data.Map as M
+
+import Control.Applicative hiding (Const(..))
+import Control.Monad.Reader
+import Control.Monad.Error
+
+typeInfer :: TyEnv -> C.CoreExpr -> (Either FerryError CoreExpr, Subst)
+typeInfer gam c = runAlgW gam $ do 
+                                   e <- algW c
+                                   -- (p, s@(Forall _ t)) <- gen $ pure $ typeOf e
+                                   let (q :=> t) = typeOf e
+                                   q' <- consistents $ pure q
+                                   let (qs, q'' :=> _t') = reduce (q' :=> t) M.empty
+                                   qual <- mergeQuals qs q''
+                                   applySubst $ setType (qual :=> t) e
+                                   --pure e
+                  
+algW :: C.CoreExpr -> AlgW CoreExpr
+algW (C.Constant c)  = Constant <$> typeOfConst c <*> pure c
+algW (C.Var x)       = Var <$> (inst $ lookupVariable x) <*> pure x
+algW (C.Let x c1 c2) = do
+                            c1' <- algW c1
+                            (p, ts@(Forall _ _ qt)) <- gen $ pure $ typeOf c1'
+                            let c1'' = setType qt  c1'
+                            c2' <- addToEnv x ts (algW c2)
+                            let (q2 :=> t2) = typeOf c2'
+                            q <- mergeQuals q2 p
+                            applySubst $ Let (q :=> t2) x c1'' c2' 
+algW (C.Nil) = Nil <$> liftM (\v -> [] :=> (list $ FVar v)) freshTyVar
+algW (C.Cons c1 c2) = do
+                        c1' <- algW c1
+                        c2' <- algW c2
+                        let (q1 :=> t1) = typeOf c1'
+                        let (q2 :=> t2) = typeOf c2'
+                        unify t2 $ FList t1
+                        q <- mergeQuals q1 q2
+                        applySubst $ Cons (q :=> t2) c1' c2'
+algW (C.If c1 c2 c3) = do
+                         c1' <- algW c1
+                         c2' <- algW c2
+                         c3' <- algW c3
+                         let (q1 :=> t1) = typeOf c1'
+                         let (q2 :=> t2) = typeOf c2'
+                         let (q3 :=> t3) = typeOf c3' 
+                         s <- getSubst
+                         unify (apply s $ t1) FBool
+                         s' <- getSubst
+                         unify (apply s' $ t2) (apply s' $ t3) 
+                         q <- mergeQuals' [q1, q2, q3]
+                         applySubst $ If (q :=> t2) c1' c2' c3'
+algW (C.Table n cs ks) = let recTys = L.sortBy (\(n1, _t1) (n2, _t2) -> compare n1 n2) $ map columnToRecElem cs
+                             in if length (uniqueKeys recTys) == length recTys 
+                                 then applySubst $ Table ([] :=> (list $ FRec recTys)) n (map columnToTyColumn cs) (map keyToTyKey ks)
+                                 else throwError $ RecordDuplicateFields (Just n) $ map columnToRecElem cs
+algW (C.Elem e i) = do
+                       fresh <- liftM FVar freshTyVar
+                       c1' <- algW e
+                       let (q1 :=> t1) = typeOf c1'
+                       case t1 of
+                            (FVar _v) -> do 
+                                          q <- insertQual (Has t1 (RLabel i) fresh) q1 
+                                          applySubst $ Elem (q :=> fresh) c1' i
+                            (FRec els) -> case lookup (RLabel i) els of
+                                            Nothing -> throwError $ RecordWithoutI t1 i
+                                            (Just a) -> applySubst $ Elem (q1 :=> a) c1' i
+                            _       -> throwError $ NotARecordType t1
+algW (C.Rec elems) = do
+                        els <- recElemsToTyRecElems elems
+                        let (qs, nt) = foldr (\(RecElem (q :=> t) n _) (qs', nt') -> (q:qs', (RLabel n, t):nt')) ([], []) els
+                        let t = FRec $ L.sortBy (\(n1, _t1) (n2, _t2) -> compare n1 n2) nt
+                        q <- mergeQuals' qs
+                        if (length (uniqueKeys nt) == length nt) 
+                                then applySubst $ Rec (q :=> t) els
+                                else throwError $ RecordDuplicateFields Nothing nt
+algW (C.BinOp (C.Op o) e1 e2) = do
+                            ot <- inst $ lookupVariable o
+                            let (q :=> FFn ot1 (FFn ot2 otr)) = ot
+                            e1' <- algW e1
+                            e2' <- algW e2
+                            let (q1 :=> t1) = typeOf e1'
+                                (q2 :=> t2) = typeOf e2'
+                            unify t1 ot1
+                            unify t2 ot2
+                            q' <- mergeQuals' [q, q1, q2] 
+                            applySubst $ BinOp (q' :=> otr) (Op o) e1' e2'
+{- algW (C.UnaOp (C.Op o) e1) = 
+                          do
+                            ot <- inst $ lookupVariable o
+                            let (q :=> FFn ot1 otr) = ot
+                            e1' <- algW e1
+                            let (q1 :=> t1) = typeOf e1'
+                            unify t1 ot1
+                            q' <- mergeQuals q q1 
+                            applySubst $ UnaOp (q :=> otr) (Op o) e1' -}
+algW (C.App e arg) = do
+                         ar <- liftM FVar freshTyVar
+                         e' <- algW e
+                         arg' <- algWArg arg
+                         let (qt1 :=> t1) = typeOf e'
+                             (qta :=> ta) = typeOf arg'
+                         unify t1 (FFn ta ar)
+                         q1 <- applySubst qt1
+                         q2 <- applySubst qta
+                         
+                         rqt <- (mergeQuals q1 q2)
+                         t <- applyS $ pure (rqt :=> ar)
+                         applySubst $ App t e' arg'
+                         
+
+algWArg :: C.Param -> AlgW Param
+algWArg (C.ParExpr e) = do
+                         e' <- algW e
+                         applySubst $ ParExpr (typeOf e') e'  
+algWArg (C.ParAbstr p e) = do
+                             let vars' = p
+                             bindings <- foldr (\v r -> do
+                                                          t <- liftM (\var' -> [] :=> FVar var') freshTyVar
+                                                          r' <- r
+                                                          return $ (v, t):r' 
+                                                          ) (pure []) vars'
+                             e' <- foldr (\(v, t) r -> addToEnv v (Forall 0 0 t) r) (algW e) bindings
+                             let (q :=> rt) = typeOf e'
+                             let t = q :=> (foldr (\(_, _ :=> ty) r -> FFn ty r) rt bindings)  
+                             applySubst $ ParAbstr t vars' e'
+                             
+{-
+toPattern :: [String] -> Pattern
+toPattern [x]   = PVar x
+toPattern xs    = Pattern xs
+                    
+getVars :: C.Pattern -> [String]
+getVars (C.PVar v) = [v]
+getVars (C.Pattern p) = p                     
+-}                           
+uniqueKeys :: Eq k => [(k, a)] -> [(k, a)]
+uniqueKeys l1 = L.nubBy (\(k1, _) (k2, _) -> k1 == k2) l1  
+
+recElemsToTyRecElems :: [C.RecElem] -> AlgW [RecElem]
+recElemsToTyRecElems (x:xs) = do
+                                x' <- recElemToTyRecElem x
+                                xs' <- recElemsToTyRecElems xs
+                                pure (x':xs')
+recElemsToTyRecElems [] = pure []
+
+recElemToTyRecElem :: C.RecElem -> AlgW RecElem
+recElemToTyRecElem (C.RecElem s e) = do
+                                        e' <- algW e
+                                        let t = typeOf e'
+                                        applySubst $ RecElem t s e'    
+                           
+                            
+columnToTyColumn :: C.Column -> Column
+columnToTyColumn (C.Column s t) = Column s $ typeToFType t
+
+columnToRecElem :: C.Column -> (RLabel, FType)
+columnToRecElem (C.Column s t) = (RLabel s, typeToFType t)
+
+typeToFType :: C.Type -> FType
+typeToFType C.TInt = FInt
+typeToFType C.TFloat = FFloat
+typeToFType C.TString = FString
+typeToFType C.TBool = FBool
+typeToFType C.TUnit = FUnit   
+
+keyToTyKey :: C.Key -> Key
+keyToTyKey (C.Key k) = Key k                     
+
+typeOfConst :: Const -> AlgW (Qual FType)
+typeOfConst (CInt _) = pure $ [] :=> FInt
+typeOfConst (CFloat _) = pure $ [] :=> FFloat
+typeOfConst (CBool _) = pure $ [] :=>  FBool
+typeOfConst (CString _) = pure $ [] :=> FString
+typeOfConst (CUnit) = pure $ [] :=> FUnit
+
+
+gen :: AlgW (Qual FType) -> AlgW ([Pred], TyScheme)
+gen s = do
+           s' <- s
+           gam <- getGamma
+           let freeInT = ftv s'
+           let freeInGam = ftv gam
+           let freeRInT = frv s'
+           let freeRInGam = frv gam
+           let quant = S.toList $ freeInT S.\\ freeInGam
+           let quantR = S.toList $ freeRInT S.\\ freeRInGam
+           let substs = zip quant [FGen i | i <- [1..]]
+           let substsR = zip quantR [RGen i | i <- [1..]]
+           qualT <- foldr (\(i, q) -> localAddSubstitution (FVar i) q) (applyS $ pure s') substs
+           qualR <- foldr (\(i, q) -> localAddRecSubstitution (RVar i) q) (applyS $ pure qualT) substsR
+           let (qg, qt) = reduce qualR M.empty
+           return $ (qg, Forall (length substs) (length substsR) $ qt)
+           
+inst :: AlgW TyScheme -> AlgW (Qual FType)
+inst s = do
+            s' <- s
+            case s' of
+                Forall 0 0 t -> applyS $ pure t
+                Forall 0 t ty -> do
+                                  freshVar <- freshTyVar
+                                  localAddRecSubstitution (RGen t) (RVar freshVar) (inst $ pure $ Forall 0 (t - 1) ty)
+                Forall i t ty -> do
+                                  freshVar <- freshTyVar
+                                  localAddSubstitution (FGen i) (FVar freshVar) (inst $ pure $ Forall (i-1) t ty)
diff --git a/src/Database/Ferry/TypeSystem/ContextReduction.hs b/src/Database/Ferry/TypeSystem/ContextReduction.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypeSystem/ContextReduction.hs
@@ -0,0 +1,38 @@
+module Database.Ferry.TypeSystem.ContextReduction where
+    
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.TypedCore.Data.TypeClasses
+import Database.Ferry.TypedCore.Data.Instances()
+
+import qualified Data.List as L
+import qualified Data.Set as S
+
+reduce :: Qual FType -> ClassEnv -> ([Pred], Qual FType)
+reduce (preds :=> tau) _ = (gamPreds, tyPreds :=> tau)
+    where
+        (tyPreds, gamPreds) = L.partition hasQVar (simplifyPreds $ foldr filterImpossiblePreds [] recPr)
+        (recPr, _classPr) = L.partition (\p -> case p of
+                                                Has _ _ _ -> True
+                                                _ -> False) preds
+
+simplifyPreds :: [Pred] -> [Pred]
+simplifyPreds ps = foldr (\x l -> (flatten x) : l)  [] groups
+   where
+    flatten x = case x of
+                 [x'] -> x'
+                 _   -> error "Multiple types for one field"
+    groups = map L.nub $ L.groupBy (\c1 c2 -> case (c1, c2) of
+                                                ((Has f1 r1 _), (Has f2 r2 _)) -> f1 == f2 && r1 == r2
+                                                _                              -> error "Wrong type of predicate") ps
+
+
+filterImpossiblePreds :: Pred -> [Pred] -> [Pred]
+filterImpossiblePreds p@(Has (FVar v) _ t) ps = case S.member v (ftv t) of
+                                    True -> error "infinite type in record"
+                                    False -> p:ps
+filterImpossiblePreds p@(Has (FRec _) _ (FVar _)) ps = (p:ps)
+                                                         
+filterImpossiblePreds p@(Has (FRec rs) f t) ps = case L.lookup f rs of
+                                       Nothing -> error "record does not contain file"
+                                       (Just t2) -> if t == t2 then ps else error $ show p ++ "incompatable types"
+filterImpossiblePreds _                    _ = error "Not a record type"
diff --git a/src/Database/Ferry/TypeSystem/Prelude.hs b/src/Database/Ferry/TypeSystem/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypeSystem/Prelude.hs
@@ -0,0 +1,109 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Database.Ferry.TypeSystem.Prelude where
+
+import Database.Ferry.Impossible    
+import Database.Ferry.TypedCore.Data.TypeClasses
+import Database.Ferry.TypedCore.Data.Type
+
+import qualified Data.Map as M
+
+baseEnv :: ClassEnv
+baseEnv = case addAll emptyClassEnv of
+            Right a -> a
+            _       -> $impossible
+    where
+        addAll =
+                do
+                    addBaseClasses <:> addBaseInstances
+        addBaseClasses =
+         addClass "Eq" []
+         <:> addClass "Num" []
+         <:> addClass "Ord" ["Eq"]
+        addBaseInstances =
+         addInstance [] (IsIn "Eq" FInt)
+         <:> addInstance [] (IsIn "Eq" FFloat)
+         <:> addInstance [] (IsIn "Eq" FBool)
+         <:> addInstance [] (IsIn "Eq" FString)
+         <:> addInstance [IsIn "Eq" $ FVar "a"] (IsIn "Eq" $ FList $ FVar "a")
+         <:> addInstance [] (IsIn "Num" FFloat)
+         <:> addInstance [] (IsIn "Num" FInt)
+         <:> addInstance [] (IsIn "Ord" FFloat)
+         <:> addInstance [] (IsIn "Ord" FBool)
+         <:> addInstance [] (IsIn "Ord" FString)
+         <:> addInstance [IsIn "Ord" $ FVar "a"] (IsIn "Ord" $ FList $ FVar "a")
+         
+primitives :: TyEnv
+primitives = M.fromList $
+             [("+", Forall 1 0 $ [IsIn "Num" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) (FGen 1)))
+             ,("-", Forall 1 0 $ [IsIn "Num" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) (FGen 1)))
+             ,("*", Forall 1 0 $ [IsIn "Num" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) (FGen 1)))
+             ,("/", Forall 1 0 $ [IsIn "Num" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) (FGen 1)))
+             ,("%", Forall 1 0 $ [IsIn "Num" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) (FGen 1)))
+             ,("^", Forall 1 0 $ [IsIn "Num" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) (FGen 1)))
+             ,("max", Forall 1 0 $ [IsIn "Num" (FGen 1)] :=> FGen 1 .-> FGen 1 .-> FGen 1)
+             ,("min", Forall 1 0 $ [IsIn "Num" (FGen 1)] :=> FGen 1 .-> FGen 1 .-> FGen 1)
+             ,("sum", Forall 1 0 $ [IsIn "Num" (FGen 1)] :=> (list $ genT 1) .-> genT 1)
+             ,("product", Forall 1 0 $ [IsIn "Num" (FGen 1)] :=> (list $ genT 1) .-> genT 1)
+             ,("maximum", Forall 1 0 $ [IsIn "Ord" (FGen 1)] :=> (list $ genT 1) .-> genT 1)
+             ,("minimum", Forall 1 0 $ [IsIn "Ord" (FGen 1)] :=> (list $ genT 1) .-> genT 1)
+             ,("==", Forall 1 0 $ [IsIn "Eq" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) bool))
+             ,("!=", Forall 1 0 $ [IsIn "Eq" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) bool))
+             ,("<=", Forall 1 0 $ [IsIn "Ord" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) bool))
+             ,(">=", Forall 1 0 $ [IsIn "Ord" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) bool))
+             ,("<", Forall 1 0 $ [IsIn "Ord" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) bool))
+             ,(">", Forall 1 0 $ [IsIn "Ord" (FGen 1)] :=> FFn (FGen 1) (FFn (FGen 1) bool))
+             ,("not", Forall 0 0 $ [] :=> bool .-> bool)
+             ,("and", Forall 0 0 $ [] :=> list bool .-> bool)
+             ,("or", Forall 0 0 $ [] :=> list bool .-> bool)
+             ,("&&", Forall 0 0 $ [] :=> bool .-> bool .-> bool)
+             ,("||", Forall 0 0 $ [] :=> bool .-> bool .-> bool)
+             ,("minP", Forall 1 0 $ [] :=> (list $ genT 1) .-> (list $ genT 1) .-> FInt)
+             ,("count", Forall 1 0 $ [] :=> (list $ genT 1) .-> FInt)
+             ,("length", Forall 1 0 $ [] :=> (list $ genT 1) .-> FInt)
+             ,("all", Forall 0 0 $ [] :=> (list bool) .-> bool)
+             ,("map", Forall 2 0 $ [] :=> (genT 1 .-> genT 2) .-> list (genT 1) .-> list (genT 2))
+             ,("concatMap", Forall 2 0 $ [] :=> (genT 1 .-> list (genT 2)) .-> list (genT 1) .-> list (genT 2))
+             ,("zipWith", Forall 3 0 $ [] :=> (genT 1 .-> genT 2 .-> genT 3) .-> list (genT 1) .-> list (genT 2) .-> list (genT 3))
+             ,("takeWhile", Forall 1 0 $ [] :=> (genT 1 .-> bool) .-> (list $ genT 1) .-> (list $ genT 1))
+             ,("dropWhile", Forall 1 0 $ [] :=> (genT 1 .-> bool) .-> (list $ genT 1) .-> (list $ genT 1))
+             ,("concat", Forall 1 0 $ [] :=> (list $ list $ genT 1) .-> (list $ genT 1))
+             ,("single", Forall 1 0 $ [] :=> (list $ genT 1) .-> genT 1)
+             ,("filter", Forall 1 0 $ [] :=> (genT 1 .-> bool) .-> (list $ genT 1) .-> (list $ genT 1))
+             ,("lookup", Forall 2 0 $ [IsIn "Eq" (genT 1)] :=> list (rec [(RLabel "1", genT 1), (RLabel "2", genT 2)]) .-> genT 1 .-> genT 2)
+             ,("length", Forall 1 0 $ [] :=> (list $ genT 1) .-> FInt)
+             ,("splitAt", Forall 1 0 $ [] :=> int .-> (list $ genT 1) .-> rec [(RLabel "1", genT 1), (RLabel "2", genT 1)])
+             ,("fst", Forall 2 0 $ [] :=> rec [(RLabel "1", genT 1), (RLabel "2", genT 2)] .-> genT 1)
+             ,("snd", Forall 2 0 $ [] :=> rec [(RLabel "1", genT 1), (RLabel "2", genT 2)] .-> genT 2)
+             ,("the", Forall 1 0 $ [] :=> (list $ genT 1) .-> genT 1)
+             ,("head", Forall 1 0 $ [] :=> (list $ genT 1) .-> genT 1)
+             ,("take", Forall 1 0 $ [] :=> FInt .-> (list $ genT 1) .-> (list $ genT 1))
+             ,("drop", Forall 1 0 $ [] :=> FInt .-> (list $ genT 1) .-> (list $ genT 1))
+             ,("reverse", Forall 1 0 $ [] :=> (list $ genT 1) .-> (list $ genT 1))
+             ,("index", Forall 1 0 $ [] :=> (list $ genT 1) .-> FInt .-> genT 1)
+             ,("last", Forall 1 0 $ [] :=> (list $ genT 1) .-> (list $ genT 1))
+             ,("tail", Forall 1 0 $ [] :=> (list $ genT 1) .-> (list $ genT 1))
+             ,("init", Forall 1 0 $ [] :=> (list $ genT 1) .-> (list $ genT 1))
+             ,("null", Forall 1 0 $ [] :=> (list $ genT 1) .-> bool)
+             ,("nub", Forall 1 0 $ [] :=> (list $ genT 1) .-> (list $ genT 1))
+             ,("integerToDouble", Forall 0 0 $ [] :=> int .-> float)
+             ,("sortWith", Forall 2 0 $ [IsIn "Ord" (FGen 2)] :=> (genT 1 .-> genT 2) .-> (list $ genT 1) .-> (list $ genT 1))
+             ,("groupByN", Forall 3 0 $ [] :=> (genT 1 .-> genT 2) .-> (genT 1 .-> genT 3) .-> list (genT 1) .-> (list $ FTF Tr (genT 2)))
+             ,("groupBy'", Forall 3 1 $ [] :=> (genT 1 .-> genT 2) .-> (genT 1 .-> genT 3) .-> list (genT 1) .-> (list $ list $ genT 2))
+             ,("groupBy1", Forall 3 1 $ [] :=> (genT 1 .-> rec [(RGen 1 ,genT 2)]) .-> (genT 1 .-> genT 3) .-> list (genT 1) .-> (list $ rec [(RGen 1 , list $ genT 2)]))
+             ,("groupBy2", Forall 4 2 $ [] :=> (genT 1 .-> rec [(RGen 1 ,genT 2), (RGen 2, genT 4)]) .-> (genT 1 .-> genT 3) .-> list (genT 1) .-> (list $ rec [(RGen 1 , list $ genT 2), (RGen 2, list $ genT 4)]))
+             ,("groupBy3", Forall 5 3 $ [] :=> (genT 1 .-> rec [(RGen 1 ,genT 2), (RGen 2, genT 4), (RGen 3, genT 5)]) .-> (genT 1 .-> genT 3) .-> list (genT 1) .-> (list $ rec [(RGen 1 , list $ genT 2), (RGen 2, list $ genT 4), (RGen 3, list $ genT 5)]))
+             ,("groupBy4", Forall 6 4 $ [] :=> (genT 1 .-> rec [(RGen 1 ,genT 2), (RGen 2, genT 4), (RGen 3, genT 5), (RGen 4, genT 6)]) .-> (genT 1 .-> genT 3) .-> list (genT 1) .-> (list $ rec [(RGen 1 , list $ genT 2), (RGen 2, list $ genT 4), (RGen 3, list $ genT 5), (RGen 4, list $ genT 6)]))
+             ,("groupBy5", Forall 7 5 $ [] :=> (genT 1 .-> rec [(RGen 1 ,genT 2), (RGen 2, genT 4), (RGen 3, genT 5), (RGen 4, genT 6), (RGen 5, genT 7)]) .-> (genT 1 .-> genT 3) .-> list (genT 1) .-> (list $ rec [(RGen 1 , list $ genT 2), (RGen 2, list $ genT 4), (RGen 3, list $ genT 5), (RGen 4, list $ genT 6), (RGen 5, list $ genT 7)]))
+             ,("groupBy6", Forall 8 6 $ [] :=> (genT 1 .-> rec [(RGen 1 ,genT 2), (RGen 2, genT 4), (RGen 3, genT 5), (RGen 4, genT 6), (RGen 5, genT 7), (RGen 6, genT 8)]) .-> (genT 1 .-> genT 3) .-> list (genT 1) .-> (list $ rec [(RGen 1 , list $ genT 2), (RGen 2, list $ genT 4), (RGen 3, list $ genT 5), (RGen 4, list $ genT 6), (RGen 5, list $ genT 7), (RGen 6, list $ genT 8)]))
+             ,("zip", Forall 2 0 $ [] :=> (list $ genT 1) .-> (list $ genT 2) .-> list (rec [(RLabel "1", genT 1),(RLabel "2", genT 2)]))
+             ,("unzip", Forall 2 0 $ [] :=> (list $ rec [(RLabel "1", genT 1), (RLabel "2", genT 2)]) .-> rec [(RLabel "1", list $ genT 1), (RLabel "2", list $ genT 2)])
+             ,("orderBy", Forall 2 0 $ [] :=> (genT 1 .-> genT 2) .-> (list $ genT 1) .-> (list $ genT 2))
+             ,("orderByDescending", Forall 2 0 $ [] :=> (genT 1 .-> genT 2) .-> (list $ genT 1) .-> (list $ genT 2))
+             ,("thenBy", Forall 2 0 $ [] :=> (genT 1 .-> genT 2) .-> (list $ genT 1) .-> (list $ genT 2))
+             ,("thenByDescending", Forall 2 0 $ [] :=> (genT 1 .-> genT 2) .-> (list $ genT 1) .-> (list $ genT 2))
+             ,("concatMap", Forall 2 0 $ [] :=> (genT 1 .-> (list $ genT 2)) .-> (list $ genT 1) .-> (list $ genT 2))
+             -- ,("mapConst", Forall 2 0 $ [] :=> genT 1 .-> (list $ genT 2) .-> (list $ genT 1))
+             ,("groupWith", Forall 3 0 $ [] :=> (genT 1 .-> genT 2) .-> (genT 1 .-> genT 3) .-> (list $ genT 1) .-> (list $ rec [(RLabel "1", genT 3), (RLabel "2", list $ genT 2)]))
+             ,("const", Forall 2 0 $ [] :=> genT 1 .-> genT 2 .-> genT 1)
+             -- ,("groupWithN", Forall 3 0 $ [] :=> (genT 1 .-> genT 2) .-> (genT 1 .-> genT 3) .-> (list $ genT 1) .-> (list $ rec [(RLabel "1", genT 3), (RLabel "2", list $ genT 2)]))
+             ]
diff --git a/src/Database/Ferry/TypeSystem/Types.hs b/src/Database/Ferry/TypeSystem/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypeSystem/Types.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE TypeSynonymInstances #-}
+module Database.Ferry.TypeSystem.Types where
+
+import Control.Monad.Reader
+import Control.Monad.State
+import Control.Monad.Error
+import Control.Applicative hiding (Const(..))
+
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.TypedCore.Data.Substitution 
+import Database.Ferry.Compiler.Error.Error
+import Database.Ferry.TypedCore.Data.Instances()
+
+import qualified Data.Map as M
+
+type AlgW = ErrorT FerryError (ReaderT TyEnv (State (Int, Subst)))
+
+runAlgW :: Substitutable a => TyEnv -> AlgW a -> (Either FerryError a, Subst)
+runAlgW gam a = (x, s)
+   where
+    (x, (_, s)) = runState (runReaderT (runErrorT $ applyS a) gam) (1, (M.empty, M.empty))
+
+getGamma :: AlgW TyEnv
+getGamma = applyS ask
+
+getSubst :: AlgW Subst
+getSubst = liftM snd get
+
+putSubst :: Subst -> AlgW ()
+putSubst s = do
+             (i, _) <- get
+             put (i, s)
+
+freshTyVar :: AlgW Ident 
+freshTyVar = do
+                (n, theta) <- get
+                put (n + 1, theta)
+                return (show n)
+
+lookupVariable :: Ident -> AlgW TyScheme
+lookupVariable i = do 
+                liftM (M.findWithDefault err i) getGamma
+            where 
+                err = error $ "Variable " ++ i ++ " not bound in env." 
+
+addToEnv :: Ident -> TyScheme -> AlgW a -> AlgW a
+addToEnv x t a = do
+                  _ <- getSubst
+                  gam <- getGamma
+                  local (\ _ -> M.insert x t gam) a
+
+addSubstitution :: Subst -> FType -> FType -> Subst
+addSubstitution (s, r) i t = let s' = M.singleton i t
+                                 s'' = M.map (apply (s', M.empty)) s
+                              in (s' `M.union` s'', r)
+
+updateSubstitution :: FType -> FType -> AlgW ()
+updateSubstitution v t = do
+                            (i, s) <- get
+                            let s' = addSubstitution s v t
+                            put (i, s')
+
+localAddSubstitution :: Substitutable a => FType -> FType -> AlgW a -> AlgW a
+localAddSubstitution i t l = do
+                            s <- getSubst
+                            updateSubstitution i t
+                            v <- applyS l
+                            putSubst s
+                            return v
+
+localAddRecSubstitution :: Substitutable a => RLabel -> RLabel -> AlgW a -> AlgW a
+localAddRecSubstitution i t l = do
+                             s <- getSubst
+                             updateRecSubstitution i t
+                             v <- applyS l
+                             putSubst s
+                             return v
+
+updateRecSubstitution :: RLabel -> RLabel -> AlgW ()
+updateRecSubstitution v t = do
+                           (i, s) <- get
+                           let s' = addRecSubstitution s v t
+                           put (i, s')
+
+addRecSubstitution :: Subst -> RLabel -> RLabel -> Subst
+addRecSubstitution (s, r) i t = let r' = M.singleton i t
+                                    r'' = M.map (apply (M.empty, r')) r
+                                 in (s, r' `M.union` r'')
+
+applyS :: Substitutable a => AlgW a -> AlgW a
+applyS v = do
+             s <- getSubst
+             v' <- v
+             return $ apply s v'
+             
+applySubst :: Substitutable a => a -> AlgW a
+applySubst v = applyS $ pure v
diff --git a/src/Database/Ferry/TypeSystem/Unification.hs b/src/Database/Ferry/TypeSystem/Unification.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypeSystem/Unification.hs
@@ -0,0 +1,109 @@
+module Database.Ferry.TypeSystem.Unification where
+    
+import Database.Ferry.TypeSystem.Types
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.Compiler.Error.Error
+import Database.Ferry.TypedCore.Data.TypeFunction
+
+import Control.Applicative hiding (Const(..))
+import Control.Monad.Error
+
+import qualified Data.List as L
+import qualified Data.Set as S
+
+
+-- | Wrapper for type unification function
+-- | it makes sure all substitutions are applied before actual unification is performed
+unify :: FType -> FType -> AlgW ()
+unify a  b = do
+                a' <- applyS $ pure a
+                b' <- applyS $ pure b
+                unify' (evalTy a') (evalTy b')
+
+-- | Unification according to specification in documentation
+-- | unify' is not a total function types star cannot be unified
+-- | with anything.
+unify' :: FType -> FType -> AlgW ()
+unify' FUnit       FUnit       = pure ()
+unify' FInt        FInt        = pure ()
+unify' FFloat      FFloat      = pure ()
+unify' FBool       FBool       = pure ()
+unify' FString     FString     = pure ()
+unify' (FList a)   (FList b)   = unify a b
+unify' (FFn a1 b1) (FFn a2 b2) = unify a1 a2 >> unify b1 b2
+unify' (FRec r1)   (FRec r2)   = unifyRecords r1 r2
+unify' t           v@(FVar a)  = if v == t || S.notMember a (ftv t)
+                                     then updateSubstitution v t
+                                     else pure ()
+unify' v@(FVar a)  t           = if v == t || S.notMember a (ftv t)
+                                     then updateSubstitution v t
+                                     else pure ()
+unify' a1          a2          = throwError $ UnificationError a1 a2
+
+-- | Helper functions for unifying records
+unifyRecords :: [(RLabel, FType)] -> [(RLabel, FType)] -> AlgW ()
+unifyRecords ((l1, t1):r1) ((l2, t2):r2) = do
+                                                unifyFields l1 l2
+                                                unify t1 t2
+                                                unifyRecords r1 r2
+unifyRecords []         [] = pure ()
+unifyRecords r1         r2 = throwError $ UnificationRecError r1 r2 
+
+-- | Helper function for unifyin individual record fields
+unifyFields :: RLabel -> RLabel -> AlgW ()
+unifyFields r1@(RLabel l1) r2@(RLabel l2) = if l1 == l2 then return () else throwError $ UnificationOfRecordFieldsFailed r1 r2
+unifyFields r1@(RVar i) r2                = if r1 == r2 || S.notMember i (frv r2)
+                                              then updateRecSubstitution r1 r2
+                                              else pure ()
+unifyFields r1          r2@(RVar i)       = if r1 == r2 || S.notMember i (frv r1)
+                                              then updateRecSubstitution r2 r1
+                                              else pure ()
+unifyFields r1          r2                = throwError $ UnificationFail r1 r2
+
+-- | Function for helping with predicate merging
+mergeQuals :: [Pred] -> [Pred] -> AlgW [Pred]
+mergeQuals t1     t2 = consistents $ mergeQualsW t1 t2
+ where
+    mergeQualsW []     t  = pure t
+    mergeQualsW t      [] = pure t
+    mergeQualsW (p:ps) t  = if L.elem p t then mergeQualsW ps t else mergeQualsW ps (p:t)
+
+-- | Add a predicate to a list of predicates
+insertQual :: Pred -> [Pred] -> AlgW [Pred]
+insertQual p@(IsIn _ _) ps = pure (p:ps)
+insertQual p@(Has v f t) (p2@(Has v2 f2 t2):ps) | v == v2 && f == f2 = do
+                                                                        unify t t2
+                                                                        t' <- applySubst t
+                                                                        pure ((Has v f t'):ps)
+                                                | otherwise          = do
+                                                                        ps' <- insertQual p ps
+                                                                        pure (p2:ps')
+insertQual p           (p':ps) = do
+                                    ps' <- insertQual p ps
+                                    pure (p':ps')
+insertQual p           []      = pure [p]
+
+mergeQuals' :: [[Pred]] -> AlgW [Pred]
+mergeQuals' pss = foldr (\p r -> do
+                                   r' <- r
+                                   mergeQuals p r') (pure []) pss
+
+-- | Check concistency of set of predicates                                   
+consistents :: AlgW [Pred] -> AlgW [Pred]
+consistents pss = do 
+                       ps <- pss
+                       case ps of
+                        (p:ps') -> do
+                                    p' <- consistent p
+                                    applySubst ps'
+                                    ps'' <- consistents $ pure ps'
+                                    applySubst (p':ps'')
+                        [] -> pure []
+
+consistent :: Pred -> AlgW Pred
+consistent p@(Has (FRec els) f t)  = case (L.lookup f els) of
+                                       Just a -> do
+                                                   unify a t
+                                                   applySubst p
+                                       Nothing -> pure p
+consistent p                       = pure p
diff --git a/src/Database/Ferry/TypedCore/Boxing/Boxing.hs b/src/Database/Ferry/TypedCore/Boxing/Boxing.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Boxing/Boxing.hs
@@ -0,0 +1,243 @@
+{-| This module performs boxing on a typed AST.
+This is an essential step in the compilation pipeline.
+It is described in more detail in:
+http://www-db.informatik.uni-tuebingen.de/files/publications/avalanche-safe-linq.pdf
+Figure 7 rule 17 and 18
+-}
+module Database.Ferry.TypedCore.Boxing.Boxing where
+
+import Database.Ferry.TypedCore.Data.TypedCore
+import Database.Ferry.TypedCore.Data.Instances()
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.Common.Data.Base
+
+import Control.Monad.Reader
+                               
+import qualified Data.Map as M (lookup)
+import Data.Maybe (fromJust)
+
+-- | Execute the unboxing in the presence of type environment env
+runBoxing :: TyEnv -> CoreExpr -> CoreExpr
+runBoxing env = fst . flip runReader (env, Nothing, emptyEnv) . topBox
+
+-- | An expression can be either a list or an atom.
+--  a unboxed list is atom. An boxed atom becomes a list.
+data Box = Atom
+         | List
+         | BFn Box Box
+       deriving (Eq, Show)
+
+-- | Box environment  
+type BoxEnv = [(Identifier, Box)]
+
+-- | Expected boxing value
+type Context = Maybe Box
+
+-- | Initial box environment
+emptyEnv :: BoxEnv
+emptyEnv = []    
+
+-- | Boxing environment, containing type environment, context and boxing environment
+type Boxing = Reader (TyEnv, Context, BoxEnv)
+
+-- * Helper function that modify the state
+
+-- | Store identifier i with boxing value b in the boxing environment for
+-- the given boxing computation
+addToEnv :: Identifier -> Box -> Boxing a -> Boxing a
+addToEnv i b = local (\(gE, cE, bE) -> (gE, cE, (i, b):bE))
+
+-- | Lookup the type scheme of an identifier in the type environment
+fromGam :: Identifier -> Boxing (Maybe TyScheme)
+fromGam i = do
+             (g, _, _) <- ask
+             return $ M.lookup i g
+
+-- | Lookup the boxing value of an identifier in the box environment                 
+fromEnv :: Identifier -> Boxing Box
+fromEnv i = do
+              (_, _, env) <- ask
+              case lookup i env of
+                  Just x -> return x
+                  Nothing -> error $ "Identifier: " ++ i ++ " not found in env during boxing."
+
+-- | Run the boxing computation with expected boxing value t
+withContext :: Box -> Boxing a -> Boxing a
+withContext t = local (\(gE, _, bE) -> (gE, Just t, bE)) 
+
+-- | Get the boxing context value (or expected boxing value)
+getFromContext :: Boxing (Maybe Box) 
+getFromContext = do
+                    (_, c, _) <- ask
+                    return c
+
+-- | Run the boxing computation without an expected boxing value                                                     
+noContext :: Boxing a -> Boxing a
+noContext = local (\(gE, _, bE) -> (gE, Nothing, bE))
+
+-- | Convert a type into a boxing value 
+trans :: FType -> Box
+trans (FList _) = List
+trans (FFn t1 t2) = BFn (trans t1) (trans t2)
+trans _           = Atom
+    
+{-|
+Heavily simplified inst, it doesn't work as a proper inst
+ from the type system it only works for types that are passed to trans.
+-}
+inst :: TyScheme -> FType
+inst (Forall _ _ (_ :=> t)) = t
+
+{-| 
+Determine how to transform an expression given an expected box value
+and the box value of the expression. 
+-}
+boxOp :: Box -> Box -> CoreExpr -> CoreExpr
+boxOp Atom List = unboxFn
+boxOp List Atom = boxFn
+boxOp _ _ = id
+
+{-| Wrap the given expression in a box-function call -}
+boxFn :: CoreExpr -> CoreExpr
+boxFn e = App t (Var t' "box") $ ParExpr t e
+  where 
+    t@(q :=> ty) = typeOf e
+    t' = q :=> ty .-> ty
+
+{-| Wrap the given expression in an unbox-function call -}
+unboxFn :: CoreExpr -> CoreExpr
+unboxFn e = App t (Var t' "unBox") $ ParExpr t e
+  where 
+    t@(q :=> ty) = typeOf e
+    t' = q :=> ty .-> ty 
+
+{-| Check whether the expected box value (if specified) matches the inferred box value-}
+resultCheck :: (CoreExpr, Box) -> Boxing (CoreExpr, Box)
+resultCheck (e, psi) = do
+                        psir <- getFromContext 
+                        case (psir, psi) of
+                            (Just p, psi') | p == psi' -> return (e, psi') 
+                                           | otherwise -> error $ "Expected box sort doesn't match inferred sort in expression: " ++ show e
+                            (Nothing, psi') -> return (e, psi')
+
+-- * The actual boxing process
+
+
+-- | Deal with corner case of lazy unboxing, the result 
+-- type is a list but the boxing says it's an atom
+-- in that case we perform the unboxing
+topBox :: CoreExpr -> Boxing (CoreExpr, Box)
+topBox e = do 
+            (e', psi) <- box e
+            let t = typeOf e'
+            case t of
+                (_ :=> (FList _)) -> return (boxOp psi List e', List)
+                _                 -> return (e', psi)
+
+-- | Run the boxing transformation over an expression, computing
+-- for every epression a new expression and its box value
+box :: CoreExpr -> Boxing (CoreExpr, Box)
+-- A constant is simply an atom
+box c@(Constant _ _) = resultCheck (c, Atom)
+-- Nil is an empty list and thus box value list
+box n@(Nil _)        = resultCheck (n, List)
+-- Const adds an element (an atom, a nested list has to be unboxed!) to another list
+-- There are no expectations on the box value of its children.
+box (Cons t e1 e2)   = do
+                         (e1', psi) <- noContext $ box e1
+                         (e2', psi2) <- noContext $ box e2 
+                         resultCheck (Cons t (boxOp psi Atom e1') (boxOp psi2 List e2'), List)
+-- Element from a list is an atom (even it is a list, it is still unboxed)
+box (Elem t e s) = do
+                      (e', psi) <- noContext $ box e
+                      resultCheck (Elem t (boxOp psi Atom e') s, Atom)
+-- A table is a list of tuples and thus has box value list
+box t@(Table _ _ _ _) = resultCheck (t, List)
+-- There are no expectations on the context of the conditional,
+-- the branches however have to meet the expectations of the entire
+-- if then else construction
+box (If t e1 e2 e3) = do
+                        (e1', psi1) <- noContext $ box e1
+                        (e2', psi2) <- box e2
+                        (e3', psi3) <- box e3
+                        if psi2 == psi3
+                            then resultCheck (If t (boxOp psi1 Atom e1') e2' e3', psi3)
+                            else resultCheck (If t (boxOp psi1 Atom e1') (boxOp psi2 Atom e2') (boxOp psi3 Atom e3'), Atom) 
+-- The bound expression doesn't have a context, the context of the whole let is equal to the context of e2
+box (Let t s e1 e2) = do
+                        (e1', psi1) <- noContext $ box e1
+                        (e2', psi2) <- addToEnv s psi1 $ box e2
+                        resultCheck (Let t s e1' e2', psi2)
+-- A variable has a type in the environment if it is a global variable
+-- it's box value can be retrieved from its type.
+-- Otherwise the variable has to have a box value in the box environment
+box (Var t x) = do 
+                  ty <- fromGam x
+                  case ty of
+                      Nothing -> do
+                                  psi <- fromEnv x
+                                  resultCheck (Var t x, psi)
+                      (Just t') -> do
+                                   let psi = trans $ inst t' 
+                                   resultCheck (Var t x, psi)
+-- A record is an atom 
+box (Rec t els) = do 
+                    els' <- mapM (noContext . boxRec) els
+                    return (Rec t els', Atom)
+-- Function application
+-- There are no expectations about the box value of e1
+-- It will however give a box value from box value to box value.
+-- The expected box value of the argument is equal to the box value
+-- at the argument position of the box function type.
+-- The result of the application is equal to the box value of result box value
+-- in the inferred box function type.
+box (App t e1 e2) = do
+                     (e1', psi) <- noContext $ box e1
+                     let (psia, psir ) = case psi of
+                                           (BFn psia' psir') -> (psia', psir')
+                                           _               -> error $ show psi ++ "not a function box"   
+                     (e2', _psi2) <- withContext psia $ boxParam e2
+                     resultCheck (App t e1' e2', psir)
+-- Similar to app
+box (BinOp t (Op o) e1 e2) = do
+                               ty <- fromGam o
+                               case ty of
+                                   Nothing -> error $ "Non primitive operator during boxing phase, this should not happen: " ++ show o
+                                   (Just t') -> do
+                                                let (BFn psi1 (BFn psi2 psi3)) = trans $ inst t'
+                                                (e1', psi1') <- noContext $ box e1
+                                                (e2', psi2') <- noContext $ box e2
+                                                resultCheck (BinOp t (Op o) (boxOp psi1' psi1 e1') (boxOp psi2' psi2 e2'), psi3)
+
+-- Box the expression in a record element
+-- They should be of box type atom, a list needs to be unboxed.
+boxRec :: RecElem -> Boxing RecElem 
+boxRec (RecElem t x e) = do
+                          (e', psi) <- box e
+                          return $ RecElem t x (boxOp psi Atom e')    
+
+-- | Box function parameters
+boxParam :: Param -> Boxing (Param, Box)   
+boxParam (ParExpr t e) = do
+                           (e', psi) <- noContext $ box e
+                           psie <- getFromContext
+                           return $ (ParExpr t $ boxOp psi (fromJust psie) e', fromJust psie)
+boxParam (ParAbstr t p e) = do
+                             let args = p
+                             psie <- getFromContext
+                             let (asso, boxR) = varsWithBox args $ fromJust psie
+                             (e', psi) <- foldr (\(v, t') r -> addToEnv v t' r) (noContext $ box e) asso
+                             return (ParAbstr t p (boxOp psi boxR e'), boxR)
+ 
+{-
+-- | Retrieve the variables in a pattern    
+getVars :: Pattern -> [String]
+getVars (PVar v) = [v]
+getVars (Pattern p) = p  
+-}
+
+-- | Construct a list of all function arguments with their respective box value, and the result box value of the function.
+varsWithBox :: [String] -> Box -> ([(String, Box)], Box)
+varsWithBox []             b = ([], b)
+varsWithBox (x:xs) (BFn b1 b2) = (\(l, b) -> ((x, b1):l, b)) (varsWithBox xs b2)
+varsWithBox _      _           = error $ "varswithBox err, should not happen"   
diff --git a/src/Database/Ferry/TypedCore/Convert/CoreToAlgebra.hs b/src/Database/Ferry/TypedCore/Convert/CoreToAlgebra.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Convert/CoreToAlgebra.hs
@@ -0,0 +1,960 @@
+{-# LANGUAGE TemplateHaskell #-}
+{- |
+This module transforms typed ferry core into a relational algebra DAG.
+The transformation assumes that given programs are type correct and some
+functions on lists have been inlined (transformations performed by RewriteStage).
+
+For a more complete overview see:
+
+http://www-db.informatik.uni-tuebingen.de/files/publications/avalanche-safe-linq.pdf
+-}
+module Database.Ferry.TypedCore.Convert.CoreToAlgebra where
+
+
+import Database.Ferry.Impossible
+import Database.Ferry.Common.Data.Base
+
+import Database.Ferry.Algebra
+
+import Database.Ferry.TypedCore.Data.Type (Qual (..), FType (..), RLabel (..), isPrim)
+import Database.Ferry.TypedCore.Data.TypedCore as T
+
+import qualified Data.Map as M 
+import qualified Data.List as L
+import Data.Maybe (fromJust, isJust)
+
+-- | Section introducing aliases for commonly used columns
+
+-- | Results are stored in column:
+resCol, resColPrime, resColPrimePrime, ordCol, ordPrime, iterPrime, iterR, posPrime, posPrimePrime, outer, inner, oldCol :: String
+resCol    = "item99999001"
+resColPrime = "item99999002"
+resColPrimePrime = "item99999003"
+ordCol    = "item99999801"
+ordPrime  = "item99999804"
+iterPrime = "item99999701"
+iterR     = "item99999703"
+posPrime  = "item99999601"
+posPrimePrime = "item99999602"
+outer     = "item99999501"
+inner     = "item99999401"
+oldCol    = "item99999301"
+
+-- | Construct the ith item columns
+mkPrefixCol :: Int -> String
+mkPrefixCol i = "item" ++ prefixCol ++ (show i)
+
+-- | Construct the ith iter column
+mkPrefixIter :: Int -> String
+mkPrefixIter i = "iter" ++ prefixCol ++ (show i)
+
+-- | Prefix for intermediate column numbers
+prefixCol :: String
+prefixCol = "9999"
+
+-- | Transform Ferry core into a relation algebra modelled as a DAG
+coreToAlgebra :: CoreExpr -> GraphM AlgRes
+-- | Primitive values
+coreToAlgebra (Constant _ CUnit) = do
+                                    n1 <- attach "pos" natT (nat 1) 
+                                            =<< attach "item1" intT (int 0) 
+                                            =<< getLoop
+                                    return (n1, [Col 1 AInt], emptyPlan)
+coreToAlgebra (Constant _ (CInt i)) = do 
+                                        n1 <- attach "pos" natT (nat 1) 
+                                                =<< attach "item1" intT (int i) 
+                                                =<< getLoop
+                                        return (n1, [Col 1 AInt], emptyPlan)
+coreToAlgebra (Constant _ (CBool i)) = do
+                                         n1 <- attach "pos" natT (nat 1) 
+                                                =<< attach "item1" boolT (bool i) 
+                                                =<< getLoop
+                                         return (n1, [Col 1 ABool], emptyPlan)
+coreToAlgebra (Constant _ (CFloat i)) = do
+                                         n1 <- attach "pos" natT (nat 1) 
+                                            =<< attach "item1" doubleT (double i) 
+                                            =<< getLoop
+                                         return (n1, [Col 1 ADouble], emptyPlan)
+coreToAlgebra (Constant _ (CString i)) = do
+                                          n1 <- attach "pos" natT (nat 1) 
+                                                =<< attach "item1" stringT (string i) 
+                                                =<< getLoop
+                                          return (n1, [Col 1 AStr], emptyPlan)
+-- Binary operators
+coreToAlgebra (BinOp (_ :=> t) (Op o) e1 e2) = do
+                                         (q1, [Col 1 _t1], _m1) <- coreToAlgebra e1
+                                         (q2, [Col 1 _t2], _m2) <- coreToAlgebra e2
+                                         n1 <- proj [("iter", "iter"), ("pos", "pos"), ("item1", resCol)] 
+                                                =<< oper o resCol  "item1" (mkPrefixCol 1) 
+                                                =<< eqJoin "iter" (mkPrefixIter 1) q1 
+                                                =<< proj [(mkPrefixIter 1, "iter"), (mkPrefixCol 1, "item1")] q2
+                                         return (n1, fst $ typeToCols t 1, emptyPlan)
+-- Let bindings
+coreToAlgebra (Let _ s e1 e2) = do
+                                    (q1, cs1, m1) <- coreToAlgebra e1
+                                    withBinding s (q1, cs1, m1) $ coreToAlgebra e2
+-- Variable lookup
+coreToAlgebra (Var _ n) = fromGam n
+-- Record construction, body of the rule can be found in recElemsToAlgebra
+coreToAlgebra (Rec _ (e:els)) = foldl recElemsToAlgebra (recElemToAlgebra e) els
+coreToAlgebra (Rec _ []) = $impossible
+-- Record element access.
+coreToAlgebra (Elem _ e n) = do
+                                (q1, cs1 ,(SubPlan ts1)) <- coreToAlgebra e
+                                let csn = getCol n cs1
+                                let (csn', i) = decrCols csn
+                                let ln = leafNumbers csn'
+                                let ts = SubPlan $ M.fromList [ (l, fromJust r) | l <- ln, let r = M.lookup (l+i) ts1, isJust r]
+                                let projPairs = zip (leafNames csn') (leafNames csn)
+                                n1 <- proj (("iter", "iter"):("pos", "pos"):projPairs) q1
+                                return (n1, csn', ts)
+--Empty lists
+coreToAlgebra (Nil (_ :=> (FList t))) = do
+                                 let cs = fst $ typeToCols t 1
+                                 let schema = ("iter", natT):("pos", natT):(colsToSchema cs)
+                                 n1 <- emptyTable schema
+                                 sub <- case t of
+                                         (FList _) -> do
+                                                        s <- coreToAlgebra $ Nil $ [] :=> t
+                                                        return $ SubPlan $ M.singleton 1 s
+                                         _ -> return emptyPlan
+                                 return (n1, cs, sub)
+coreToAlgebra (Nil _) = $impossible -- After type checking the only thing that reaches this stage has a list type
+-- List constructor, because of optimisation chances contents has been directed to special functions
+coreToAlgebra (c@(Cons _ _ _)) = listFirst c
+-- Database tables
+coreToAlgebra (Table _ n cs ks) = do
+                                    let cs' = coreCol2AlgCol cs
+                                    let keys' = key2Key cs' ks
+                                    loop <- getLoop
+                                    n1 <- cross loop 
+                                            =<< rank "pos" (map (\ki -> (ki, Asc)) $ head keys') 
+                                            =<< dbTable n cs' keys'
+                                    return (n1, cs', emptyPlan)
+-- If then else
+coreToAlgebra (If _ e1 e2 e3) = do
+                                  (q1, _cs1, _ts1) <- coreToAlgebra e1
+                                  -- Get current gamma
+                                  gam <- getGamma
+                                  -- Build loop and gamma for then branch 
+                                  loopThen <- proj [("iter", "iter")] =<< select "item1" q1
+                                  gamThen <- transformGam algResLoop loopThen gam 
+                                  --Evaluate then branch
+                                  (q2, cs2, ts2) <- withContext gamThen loopThen $ coreToAlgebra e2
+                                  -- Build loop and gamma for else branch
+                                  loopElse <- proj [("iter", "iter")] 
+                                                =<< select resCol 
+                                                =<< notC resCol "item1" q1
+                                  gamElse <- transformGam algResLoop loopElse gam 
+                                  --Evaluate else branch
+                                  (q3, _cs3, ts3) <- withContext gamElse loopElse $ coreToAlgebra e3
+                                  --Construct result
+                                  let ks = keys ts2
+                                  let cols = leafNames cs2
+                                  let colsDiff = cols L.\\ ks
+                                  n1 <- attach ordCol natT (nat 1) q2
+                                  q' <- rownum iterPrime ["iter", ordCol, "pos"] Nothing
+                                            =<< union n1 
+                                                =<< attach ordCol natT (nat 2) q3
+                                  let projPairs = zip colsDiff colsDiff ++ zip ks (repeat iterPrime)
+                                  n2 <- proj (("iter","iter"):("pos","pos"):projPairs) q'
+                                  ts <- mergeTableStructure q' ts2 ts3
+                                  return (n2, cs2, ts)
+-- Compile function application, as we do not have functions as results the given
+-- argument can be evaluated and then be passed to the compileApp function.
+coreToAlgebra (App _ e1 e2) = compileAppE1 e1 =<< compileParam e2
+                                
+
+-- | Transform the variable environment                                  
+transformGam :: (AlgNode -> (String, AlgRes) -> GraphM (String, AlgRes)) 
+                -> AlgNode -> Gam -> GraphM Gam
+transformGam f loop gamma  = mapM (f loop) gamma
+
+-- | Transformation of gamma for if then else    
+algResLoop :: AlgNode -> (String, AlgRes) -> GraphM (String, AlgRes)
+algResLoop loop (n, (i, cs, pl)) = do
+                              i' <- eqJoin "iter" "iter" i loop
+                              return (n, (i', cs, pl))
+
+-- | Compile a function parameter
+-- | Function is partial, i.e. it doesn't compile lambda's as arguments                              
+compileParam :: Param -> GraphM AlgRes
+compileParam (ParExpr _ e1) = coreToAlgebra e1
+compileParam (ParAbstr _ _ _) = $impossible
+
+-- | Compile function application.
+-- | Expects a core expression the function, and the evaluated argument
+compileAppE1 :: CoreExpr -> AlgRes -> GraphM AlgRes
+compileAppE1 (App _ (Var _ "zip") (ParExpr _ e1)) (q2', cs2, (SubPlan ts2)) =
+                do
+                    (q1', cs1, (SubPlan ts1)) <- coreToAlgebra e1
+                    q1 <- absPos q1' cs1
+                    q2 <- absPos q2' cs2
+                    let offSet = colSize cs1
+                    let cs2' = incrCols offSet cs2
+                    let projPairs1 = zip (leafNames cs1) (leafNames cs1)
+                    let projPairs2 = zip (leafNames cs2') (leafNames cs2')
+                    let projPairs2' = zip (leafNames cs2') (leafNames cs2) 
+                    q <- eqTJoin [("iter", iterPrime), ("pos", posPrime)] (("iter", "iter"):("pos", "pos"):(projPairs1 ++ projPairs2)) q1
+                            =<< proj ((iterPrime, "iter"):(posPrime, "pos"):projPairs2') q2
+                    let cs = [NCol "1" cs1, NCol "2" cs2']
+                    let ts = SubPlan $ M.union ts1 $ M.mapKeysMonotonic (+ offSet) ts2
+                    return (q, cs, ts)
+compileAppE1 (Var _ "unzip") (q, [NCol "1" cs1, NCol "2" cs2], (SubPlan ts)) =
+               do
+                   let (cs2d, d) = decrCols cs2
+                   let projPairs1 = zip (leafNames cs1) (leafNames cs1)
+                   let projPairs2 = zip (leafNames cs2d) (leafNames cs2)
+                   q' <- proj [("iter", "iter"),("pos", "pos"), ("item1", "iter"), ("item2", "iter")]
+                            =<< attach "pos" natT (nat 1) =<< getLoop
+                   q1 <- proj (("iter", "iter"):("pos", "pos"):projPairs1) q
+                   q2 <- proj (("iter", "iter"):("pos", "pos"):projPairs2) q
+                   let cs = [NCol "1" [Col 1 surT], NCol "2" [Col 2 surT]]
+                   let ln1 = leafNumbers cs1
+                   let ln2 = leafNumbers cs2d
+                   let ts1 = SubPlan $ M.fromList [(l, ts M.! l)  | l <- ln1, isJust $ M.lookup l ts]
+                   let ts2 = SubPlan $ M.fromList [(l, ts M.! (l + d)) | l <- ln2, isJust $ M.lookup (l +d) ts]
+                   let ts' = SubPlan $ M.fromList [(1, (q1, cs1, ts1)),(2, (q2, cs2d,ts2))]
+                   return (q', cs, ts')
+                    
+compileAppE1 (App _ (Var _ "map") l@(ParAbstr _ _ _)) (q1, cs1, ts1) = 
+                do
+                    gam <- getGamma
+                    (_qv', qv, mapv, loopv, gamV) <- mapForward gam q1 cs1
+                    (q2, cs2, ts2) <- withContext gamV loopv $ compileLambda [(qv, cs1, ts1)] l
+                    let csProj2 = zip (leafNames cs2) (leafNames cs2)
+                    q <- proj (("iter",outer):("pos", posPrime):csProj2)
+                            =<< eqJoin "iter" inner q2 mapv
+                    return (q, cs2, ts2)
+compileAppE1 (App _ (Var _ "takeWhile") l@(ParAbstr _ _ _)) (q1, cs1, ts1) =
+                do
+                    gam <- getGamma
+                    loop <- getLoop
+                    (qv', qv, _mapv, loopv, gamV) <- mapForward gam q1 cs1
+                    (q2, _cs2, _ts2) <- withContext gamV loopv $ compileLambda [(qv, cs1, ts1)] l
+                    let projPairs = zip (leafNames cs1) (leafNames cs1)
+                    q' <- proj (("iter","iter"):("pos", "pos"):(resCol, resCol):projPairs)
+                            =<< eqJoin inner iterPrime qv'
+                                =<< proj [(iterPrime, "iter"),(resCol, "item1")] q2
+                    qM <- aggr [(Min, posPrime, Just "pos")] (Just "iter")
+                           =<< select posPrime 
+                             =<< notC posPrime resCol q'
+                    qE <- proj (("iter", "iter"):("pos", "pos"):projPairs)
+                            =<< eqJoin "iter" iterPrime q1
+                                =<< proj [(iterPrime, "iter")] 
+                                    =<< difference loop 
+                                        =<< proj [("iter", "iter")] qM
+                    q'' <- union qE
+                            =<< proj (("iter", "iter"):("pos", "pos"):projPairs)
+                                =<< select resColPrime
+                                    =<< oper ">" resColPrime posPrime "pos"
+                                        =<< eqJoin "iter" iterPrime q'
+                                            =<< proj [(iterPrime, "iter"), (posPrime, posPrime)] qM
+                    return (q'', cs1, ts1)
+compileAppE1 (App _ (App _ (Var _ "zipWith") l@(ParAbstr _ _ _)) (ParExpr _ e1)) (q2, cs2, ts2) =
+                do
+                    gam <- getGamma
+                    (q1, cs1, ts1) <- coreToAlgebra e1
+                    q1' <- absPos q1 cs1
+                    q2' <- absPos q2 cs2
+                    let offSet = colSize cs1
+                    let cs2' = incrCols offSet cs2
+                    q <- eqTJoin [("pos", posPrime), ("iter", iterPrime)] (("iter", "iter"):("pos", "pos"): ((zip (leafNames cs1) (leafNames cs1)) ++ (zip (leafNames cs2') (leafNames cs2')))) q1'
+                        =<< proj ((iterPrime, "iter"):(posPrime, "pos"):(zip (leafNames cs2') (leafNames cs2))) q2'
+                    (_qv', qv, mapv, loopv, gamV) <- mapForward gam q $ cs1 ++ cs2'
+                    qv1 <- proj (("iter", "iter"):("pos", "pos"):(zip (leafNames cs1) (leafNames cs1))) qv
+                    qv2 <- proj (("iter", "iter"):("pos", "pos"):(zip (leafNames cs2) (leafNames cs2'))) qv
+                    (q3, cs3, ts3) <- withContext gamV loopv $ compileLambda [(qv1, cs1, ts1), (qv2, cs2, ts2)] l
+                    qr <- proj (("iter", outer):("pos", posPrime):(zip (leafNames cs3) (leafNames cs3))) 
+                            =<< eqJoin "iter" inner q3 mapv
+                    return (qr, cs3, ts3)
+compileAppE1 (App _ (Var _ "dropWhile") l@(ParAbstr _ _ _)) (q1, cs1, ts1) =
+                do
+                    gam <- getGamma
+                    (qv', qv, _mapv, loopv, gamV) <- mapForward gam q1 cs1
+                    (q2, _cs2, _ts2) <- withContext gamV loopv $ compileLambda [(qv, cs1, ts1)] l
+                    let projPairs = zip (leafNames cs1) (leafNames cs1)
+                    q' <- proj (("iter","iter"):("pos", "pos"):(resCol, resCol):projPairs)
+                            =<< eqJoin inner iterPrime qv'
+                                =<< proj [(iterPrime, "iter"),(resCol, "item1")] q2
+                    q'' <- proj (("iter", "iter"):("pos", "pos"):projPairs)
+                            =<< select ordCol
+                                =<< oper "||" ordCol resColPrimePrime resColPrime
+                                    =<< oper "==" resColPrimePrime "pos" posPrime
+                                        =<< oper ">" resColPrime "pos" posPrime 
+                                            =<< eqJoin "iter" iterPrime q'
+                                                =<< proj [(iterPrime, "iter"), (posPrime, posPrime)]
+                                                    =<< aggr [(Min, posPrime, Just "pos")] (Just "iter")
+                                                        =<< select posPrime 
+                                                            =<< notC posPrime resCol q'
+                    return (q'', cs1, ts1)
+compileAppE1 (App _ (Var _ "sortWith") l@(ParAbstr _ _ _)) (q1, cs1, ts1) =
+                do
+                    gam <- getGamma
+                    (_qv', qv, mapv, loopv, gamV) <- mapForward gam q1 cs1
+                    (q2, cs2, _ts2) <- withContext gamV loopv $ compileLambda [(qv, cs1, ts1)] l
+                    let projPairs = zip (leafNames cs1) (leafNames cs1)
+                    q <- proj (("iter", outer):("pos", resCol):projPairs) =<< select resColPrime
+                        =<< oper "==" resColPrime "pos" posPrime  
+                            =<< eqJoin "iter" outer q1 
+                                =<< proj [(inner, inner), (outer, outer), (posPrime, posPrime), (resCol, resCol)]    
+                                    =<< rownum resCol (leafNames cs2) (Just outer)  
+                                        =<< eqJoin "iter" inner q2 mapv
+                    return (q, cs1, ts1)
+compileAppE1 (App _ (Var _ "max") (ParExpr _ e1)) (q2, [Col 1 t], _ts2) = 
+                do
+                    (q1, [Col 1 _], _ts1) <- coreToAlgebra e1
+                    q <- attach "pos" natT (nat 1)  
+                        =<< proj [("iter", "iter"),("item1", resCol)]    
+                            =<< aggr [(Max, resCol, Just "item1")] (Just "iter") 
+                                =<< union q1 q2
+                    return (q, [Col 1 t], emptyPlan)
+compileAppE1 (App _ (Var _ "min") (ParExpr _ e1)) (q2, [Col 1 t], _ts2) =
+                do
+                    (q1, [Col 1 _], _ts1) <- coreToAlgebra e1
+                    q <- attach "pos" natT (nat 1)  
+                        =<< proj [("iter", "iter"),("item1", resCol)]    
+                            =<< aggr [(Min, resCol, Just "item1")] (Just "iter") 
+                                =<< union q1 q2
+                    return (q, [Col 1 t], emptyPlan)
+compileAppE1 (App _ (Var _ "filter") l@(ParAbstr _ _ _)) (q1, cs1, ts1) =
+                do
+                    gam <- getGamma
+                    (qv', qv, _mapv, loopv, gamV) <- mapForward gam q1 cs1
+                    (q2, _cs2, _ts2) <- withContext gamV loopv $ compileLambda [(qv, cs1, ts1)] l
+                    let csProj = zip (leafNames cs1) (leafNames cs1)
+                    q <- proj (("iter", "iter"):("pos", "pos"):csProj)
+                            =<< select resCol  
+                                =<< eqJoin inner iterPrime qv' 
+                                    =<< proj [(iterPrime, "iter"), (resCol, "item1")] q2
+                    return (q, cs1, ts1)
+compileAppE1 (Var _ "head") (q1', cs1, ts1) =
+                do
+                    q1 <- absPos q1' cs1
+                    q <- posSelect 1 [("pos", Asc)] (Just "iter") q1
+                    return (q, cs1, ts1)
+compileAppE1 (Var _ "tail") (q1', cs1, ts1) =
+                    do
+                        let projPairs = zip (leafNames cs1) (leafNames cs1)
+                        q1 <- absPos q1' cs1
+                        q <- proj (("iter", "iter"):("pos", "pos"):projPairs)
+                                =<< select resCol 
+                                    =<< oper ">" resCol "pos" oldCol 
+                                        =<< attach oldCol natT (nat 1) q1
+                        return (q, cs1, ts1)
+compileAppE1 (Var _ "concat") (q, _cs, SubPlan ts) =
+                    do
+                        let [(1, (qs, css, tss))] = M.toList ts
+                        let projPairs = zip (leafNames css) (leafNames css)
+                        q' <- proj (("iter", iterPrime):("pos", posPrimePrime):projPairs)
+                                =<< rank posPrimePrime [(posPrime, Asc), ("pos", Asc)]
+                                    =<< eqJoin "iter" resCol qs
+                                        =<< proj [(iterPrime, "iter"),(posPrime, "pos"), (resCol, "item1")] q
+                        return (q', css, tss)    
+compileAppE1 (Var _ "nub") (q, cs, ts) =
+                    do
+                        let projPairs = ("iter", "iter"):("pos", "pos"):(zip (leafNames cs) (leafNames cs))
+                        q' <- proj projPairs
+                            =<< aggr ((Min, "pos", Just "pos"):(Dist, "iter", Just "iter"):[(Dist, c, Just c) | c <- leafNames cs]) (Just resCol)
+                                =<< rowrank resCol (map (\x -> (x, Asc)) ("iter":(leafNames cs))) q
+                        return (q', cs, ts)
+compileAppE1 (Var mt "count") (q, cs, ts) = compileAppE1 (Var mt "length") (q, cs, ts)
+compileAppE1 (App _ (Var _ "index") (ParExpr _ e1)) (q2, _cs2, _ts2) =
+                    do
+                        (q1, cs1, ts1) <- coreToAlgebra e1
+                        is <- proj [(iterPrime, "iter"), (resCol, resColPrimePrime)] 
+                            =<< oper "+" resColPrimePrime resColPrime resCol
+                                =<< attach resColPrime natT (nat 1)
+                                    =<< cast "item1" resCol natT q2
+                        let projPairs = zip (leafNames cs1) (leafNames cs1) 
+                        q <- proj (("iter", "iter"):("pos", "pos"):projPairs)
+                            =<< select resColPrime    
+                                =<< oper "==" resColPrime resCol "pos"
+                                    =<< eqJoin iterPrime "iter" is q1
+                        return (q, cs1, ts1)
+compileAppE1 (App _ (Var _ "mapConst") (ParExpr _ e1)) (q2, _cs2, _ts2) =
+                    do
+                        (q1, cs1, ts1) <- coreToAlgebra e1
+                        let projPairs = zip (leafNames cs1) (leafNames cs1)
+                        q1' <- proj ((iterPrime, "iter") : projPairs) q1
+                        q <- proj (("iter", "iter"):("pos", "pos"):projPairs)
+                            =<< eqJoin iterPrime "iter"  q1' 
+                                =<< proj [("iter", "iter"),("pos", "pos")] q2
+                        return (q, cs1, ts1)
+compileAppE1 (Var _ "reverse") (q1, cs1, ts1) =
+                    do
+                        let projPairs = zip (leafNames cs1) (leafNames cs1)
+                        q <- proj (("iter", "iter"):("pos", posPrime):projPairs)
+                            =<< rownum' posPrime [("pos", Desc)] (Just "iter") q1
+                        return (q, cs1, ts1)
+compileAppE1 (Var _ "length") (q, _cs, _ts) = 
+                    do
+                        loop <- getLoop
+                        q''' <- aggr [(Count, "item1", Nothing)] (Just "iter") q
+                        q'' <- attach "item1" intT (int 0)
+                                =<< difference loop 
+                                    =<< proj [("iter", "iter")] q'''
+                        q' <- attach "pos" natT (nat 1)
+                                =<< union q'' q''' 
+                        return (q', [Col 1 AInt], emptyPlan)
+                        
+compileAppE1 (Var _ "box") (q, cs, ts) =
+                    do
+                        q' <- attach "pos" natT (nat 1) 
+                                =<< proj [("iter", "iter"),("item1", "iter")] 
+                                    =<< getLoop
+                        return (q', [Col 1 surT], subPlan 1 (q, cs, ts))
+compileAppE1 (Var mt@(_ :=> FFn _ t) "the") (q, cs, ts) = 
+                                                     if (isPrim t) 
+                                                      then
+                                                       do 
+                                                         let projPairs = (:) ("iter", "iter") $ zip (leafNames cs) (leafNames cs)
+                                                         q' <- attach "pos" natT (nat 1) =<< distinct =<< proj projPairs q
+                                                         return (q', cs, ts) 
+                                                      else 
+                                                        compileAppE1 (Var mt "head") (q, cs, ts)
+compileAppE1 (Var mt "all") (q, cs, ts) = compileAppE1 (Var mt "and") (q, cs, ts)
+compileAppE1 (Var _ "and") (q, cs, ts) =
+                    do
+                        q' <- attach "pos" natT (nat 1)
+                                =<< proj [("iter", "iter"), ("item1", resCol)]
+                                    =<< aggr [(Min, resCol, Just "item1")] (Just "iter")
+                                        =<< union q
+                                            =<< attach "pos" natT (nat 1) =<< attach "item1" boolT (bool True) =<< getLoop 
+                        return (q', cs, ts)
+compileAppE1 (Var (_ :=> FFn _ t) "sum") (q, cs, _) =
+                    do
+                        let ty = case t of
+                                    FInt -> intT
+                                    FFloat -> doubleT
+                                    (FVar _) -> intT
+                                    _ -> $impossible
+                        loop <- getLoop
+                        q' <- aggr [(Sum, "item1", Just "item1")] (Just "iter") q
+                        q'' <- attach "item1" ty (int 0)
+                                =<< difference loop 
+                                    =<< proj [("iter", "iter")] q'
+                        q''' <- attach "pos" natT (nat 1) 
+                                    =<< union q'' q'
+                        return (q''', cs, emptyPlan)
+compileAppE1 (Var _ "maximum") (q, cs, _) =
+                    do
+                        q' <- attach "pos" natT (nat 1)
+                                =<< proj [("iter", "iter"), ("item1", resCol)]
+                                    =<< aggr [(Max, resCol, Just "item1")] (Just "iter") q
+                        return (q', cs, emptyPlan)
+compileAppE1 (Var _ "minimum") (q, cs, _) =
+                    do
+                        q' <- attach "pos" natT (nat 1)
+                                =<< proj [("iter", "iter"), ("item1", resCol)]
+                                    =<< aggr [(Min, resCol, Just "item1")] (Just "iter") q
+                        return (q', cs, emptyPlan)
+compileAppE1 (Var (_ :=> FFn _ t) "product") (q, cs, _) =
+                    do
+                        let ty = case t of
+                                    FInt -> intT
+                                    FFloat -> doubleT
+                                    (FVar _) -> intT
+                                    _ -> $impossible
+                        loop <- getLoop
+                        q' <- aggr [(Prod, "item1", Just "item1")] (Just "iter") q
+                        q'' <- attach "item1" ty (int 1)
+                                =<< difference loop 
+                                    =<< proj [("iter", "iter")] q'
+                        q''' <- attach "pos" natT (nat 1) 
+                                    =<< union q'' q'
+                        return (q''', cs, emptyPlan)
+compileAppE1 (Var _ "or") (q, cs, ts) =
+                    do
+                        q' <- attach "pos" natT (nat 1)
+                                =<< proj [("iter", "iter"), ("item1", resCol)]
+                                    =<< aggr [(Max, resCol, Just "item1")] (Just "iter") 
+                                        =<< union q
+                                            =<< attach "pos" natT (nat 1) =<< attach "item1" boolT (bool False) =<< getLoop
+                        return (q', cs, ts)
+compileAppE1 (Var _ "not") (q, [Col 1 t], _ts) =
+                    do
+                        q' <- proj [("iter", "iter"), ("pos", "pos"), ("item1", resCol)]
+                                =<< notC resCol "item1" q
+                        return (q', [Col 1 t], emptyPlan)
+compileAppE1 (Var _ "integerToDouble") (q, _cs, _ts) =
+                    do
+                        q' <- proj [("iter", "iter"), ("pos", "pos"), ("item1", resCol)]
+                                =<< cast "item1" resCol ADouble q
+                        return (q', [Col 1 ADouble], emptyPlan )
+compileAppE1 (App _ (Var _ "splitAt") (ParExpr _ e1)) (q2, cs2, ts2) =
+                    do
+                        (q1, [Col 1 AInt], _ts1) <- coreToAlgebra e1
+                        let projPairs = zip (leafNames cs2) (leafNames cs2) 
+                        q2' <- absPos q2 cs2
+                        q' <- oper ">" resCol posPrime ordCol
+                                =<< cast "pos" posPrime intT
+                                    =<< eqJoin "iter" iterPrime q2'
+                                        =<< proj [(ordCol, "item1"), (iterPrime, "iter")] q1
+                        ql <- proj (("iter", "iter"):("pos", "pos"):projPairs)
+                                =<< select resColPrime 
+                                    =<< notC resColPrime resCol q'
+                        qr <- proj (("iter", "iter"):("pos", "pos"):projPairs)
+                                =<< select resCol q'
+                        loop <- getLoop
+                        q'' <- attach "pos" natT (nat 1)
+                                =<< proj [("iter", "iter"), ("item1", "iter"), ("item2", "iter")] loop
+                        return (q'', [Col 1 ASur, Col 2 ASur], SubPlan $ M.fromList [(1, (ql, cs2, ts2)), (2, (qr, cs2, ts2))])
+compileAppE1 (App _ (Var _ "take") (ParExpr _ e1)) (q2, cs2, ts2) =
+                    do
+                        (q1, [Col 1 AInt], _ts) <- coreToAlgebra e1
+                        q2' <- absPos q2 cs2
+                        let csProj = zip (leafNames cs2) (leafNames cs2)
+                        q <- proj (("iter", "iter"):("pos", "pos"):csProj)    
+                            =<< select resColPrimePrime
+                            =<< oper "||" resColPrimePrime resColPrime resCol 
+                            =<< oper "==" resColPrime oldCol posPrime 
+                                =<< oper ">" resCol oldCol posPrime 
+                                    =<< cast "pos" posPrime intT
+                                    =<< eqJoin "iter" iterPrime q2' 
+                                        =<< proj [(iterPrime, "iter"), (oldCol, "item1")] q1
+                        return (q, cs2, ts2)
+compileAppE1 (App _ (Var _ "drop") (ParExpr _ e1)) (q2, cs2, ts2) =
+                    do
+                        (q1, [Col 1 AInt], _ts) <- coreToAlgebra e1
+                        q2' <- absPos q2 cs2
+                        let csProj = zip (leafNames cs2) (leafNames cs2)
+                        q <- proj (("iter", "iter"):("pos", "pos"):csProj)    
+                            =<< select resCol
+                                =<< oper ">" resCol posPrime oldCol 
+                                    =<< cast "pos" posPrime intT
+                                    =<< eqJoin "iter" iterPrime q2' 
+                                        =<< proj [(iterPrime, "iter"), (oldCol, "item1")] q1
+                        return (q, cs2, ts2)
+compileAppE1 (Var _ "last") (q1, cs1, ts1) =
+                    do
+                        let csProj = zip (leafNames cs1) (leafNames cs1)
+                        q' <- eqTJoin [("iter", iterPrime), ("pos", resCol)] (("iter", "iter"):("pos", "pos"):csProj) q1
+                                =<< proj [(resCol, resCol), (iterPrime, "iter")]
+                                    =<< aggr [(Max, resCol, Just "pos")] (Just "iter") q1
+                        return (q', cs1, ts1)
+compileAppE1 (Var _ "init") (q1, cs1, ts1) =
+                    do
+                        let csProj = zip (leafNames cs1) (leafNames cs1)
+                        q <- proj (("iter", "iter"):("pos","pos"):csProj)
+                            =<< select resColPrime
+                                =<< oper ">" resColPrime resCol "pos" 
+                                    =<< eqJoin "iter" iterPrime q1
+                                        =<< proj [(resCol, resCol), (iterPrime, "iter")] 
+                                            =<< aggr [(Max, resCol, Just "pos")] (Just "iter") q1
+                        return (q, cs1, ts1)
+compileAppE1 (Var _ "null") (q1, _cs1, _ts1) =
+                    do
+                        loop <- getLoop
+                        notEmpty <- distinct =<< proj [("iter", "iter")] q1
+                        empty <- difference loop notEmpty
+                        notEmpty' <- attach "item1" boolT (bool False) notEmpty
+                        q <- attach "pos" natT (nat 1) 
+                                =<< union notEmpty'
+                                    =<< attach "item1" boolT (bool True) empty
+                        return (q, [Col 1 ABool], emptyPlan)                        
+compileAppE1 (Var _ "unBox") (q, [Col 1 ASur], ts) = 
+                    do
+                        let (q', cs', ts') = getPlan 1 ts
+                        let csProj = zip (leafNames cs') (leafNames cs')
+                        q'' <- proj (("iter", iterPrime):("pos","pos"):csProj)
+                                =<< eqJoin "iter" resCol q'
+                                    =<< proj [(iterPrime, "iter"),(resCol, "item1")] q
+                        return (q'', cs', ts')
+compileAppE1 (App _ (App _ (Var _ "groupWith") e1@(ParAbstr _ _ _)) e2@(ParAbstr _ _ _)) (q3, cs3, ts3) =
+            do
+                gam <- getGamma
+                (qv', qv, _map', loop', gam') <- mapForward gam q3 cs3
+                (q1, cs1, ts1) <- withContext gam' loop' $ compileLambda [(qv, cs3, ts3)] e1
+                (q2, cs2, _ts2) <- withContext gam' loop' $ compileLambda [(qv, cs3, ts3)] e2
+                let offSet = colSize cs1
+                let cs2' = incrCols offSet cs2
+                let projPairs1 = zip (leafNames cs1) (leafNames cs1)
+                let projPairs2 = zip (leafNames cs2') (leafNames cs2)
+                q1' <- proj ((iterR, "iter"):projPairs1) q1
+                q2' <- proj ((iterPrime, "iter"):projPairs2) q2
+                qs <- eqJoin iterR iterPrime q1' q2'
+                qvs <- proj [("iter", "iter"), ("pos", "pos"), (inner, inner)] qv'
+                q <- rowrank resCol (map (\ki -> (ki, Asc)) ((:) "iter" $ leafNames cs2'))
+                        =<< eqJoin inner iterPrime qvs qs
+                let newCol = (+) 1 $ colSize cs2
+                let projPairs2' = zip (leafNames cs2) (leafNames cs2')
+                qout <- distinct =<< proj (("iter", "iter"):("pos", resCol):("item" ++ show newCol, resCol):projPairs2') q
+                qin <- proj (("iter", resCol):("pos", "pos"):projPairs1) q
+                let cs = [NCol "1" cs2, NCol "2" [Col newCol surT]]
+                let ts = subPlan newCol (qin, cs1, ts1)
+                return (qout, cs, ts)
+compileAppE1 (App t2 (App t1 (Var mt "groupByN") e1) e2) e3 = compileAppE1 (App t2 (App t1 (Var mt "groupBy") e1) e2) e3
+compileAppE1 (App t2 (App t1 (Var mt "groupBy'") e1) e2) e3 = compileAppE1 (App t2 (App t1 (Var mt "groupBy") e1) e2) e3
+compileAppE1 (App t2 (App t1 (Var mt "groupBy1") e1) e2) e3 = compileAppE1 (App t2 (App t1 (Var mt "groupBy") e1) e2) e3
+compileAppE1 (App t2 (App t1 (Var mt "groupBy2") e1) e2) e3 = compileAppE1 (App t2 (App t1 (Var mt "groupBy") e1) e2) e3
+compileAppE1 (App t2 (App t1 (Var mt "groupBy3") e1) e2) e3 = compileAppE1 (App t2 (App t1 (Var mt "groupBy") e1) e2) e3
+compileAppE1 (App t2 (App t1 (Var mt "groupBy4") e1) e2) e3 = compileAppE1 (App t2 (App t1 (Var mt "groupBy") e1) e2) e3
+compileAppE1 (App t2 (App t1 (Var mt "groupBy5") e1) e2) e3 = compileAppE1 (App t2 (App t1 (Var mt "groupBy") e1) e2) e3
+compileAppE1 (App t2 (App t1 (Var mt "groupBy6") e1) e2) e3 = compileAppE1 (App t2 (App t1 (Var mt "groupBy") e1) e2) e3
+compileAppE1 (App _ (App _ (Var _ "groupBy") e1@(ParAbstr _ _ _)) e2@(ParAbstr _ _ _)) (q3, cs3, ts3) =
+            do
+                gam <- getGamma
+                (qv', qv, _map', loop', gam') <- mapForward gam q3 cs3
+                (q1, cs1, ts1) <- withContext gam' loop' $ compileLambda [(qv, cs3, ts3)] e1
+                (q2, cs2, _ts2) <- withContext gam' loop' $ compileLambda [(qv, cs3, ts3)] e2
+                let offSet = colSize cs1
+                let cs2' = incrCols offSet cs2
+                let projPairs1 = zip (leafNames cs1) (leafNames cs1)
+                let projPairs2 = zip (leafNames cs2') (leafNames cs2)
+                q1' <- proj ((iterR, "iter"):projPairs1) q1
+                q2' <- proj ((iterPrime, "iter"):projPairs2) q2
+                qs <- eqJoin iterR iterPrime q1' q2'
+                qvs <- proj [("iter", "iter"), ("pos", "pos"), (inner, inner)] qv'
+                q <- rowrank resCol (map (\ki -> (ki, Asc)) ((:) "iter" $ leafNames cs2'))
+                        =<< eqJoin inner iterPrime qvs qs
+                let nrFields = length cs1
+                let projOut = zip ["item" ++ show i | i <- [1..nrFields]] $ repeat resCol
+                qout <- distinct =<< proj (("iter", "iter"):("pos", resCol):projOut) q
+                (ts, cs) <- makeSubPlan 1 cs1 ts1 q
+                return (qout, cs, ts)
+compileAppE1 e1 _ = error $ "Not implemented yet: " ++ show e1           
+
+
+makeSubPlan :: Int -> Columns -> SubPlan -> AlgNode -> GraphM (SubPlan, Columns)
+makeSubPlan 1 [Col _ t] (SubPlan ts) q = do
+                                            qi <- proj [("iter", resCol),("pos", posPrime),("item1", "item1")] q
+                                            let tsi = case M.lookup 1 ts of
+                                                        Nothing -> emptyPlan
+                                                        (Just p) -> subPlan 1 p
+                                            return (subPlan 1 (qi, [Col 1 t], tsi), [Col 1 surT])
+makeSubPlan i ((NCol n csi):css) (SubPlan ts) q = do
+                                                    (SubPlan ts', cs') <- makeSubPlan (i + 1) css (SubPlan ts) q
+                                                    let (csi', d) = decrCols csi
+                                                    let ln = leafNumbers csi'
+                                                    let projPairs = zip (leafNames csi') (leafNames csi)
+                                                    qi <- proj (("iter", resCol):("pos", "pos"):projPairs) q
+                                                    let tsi = SubPlan $ M.fromList [(l, ts M.! (l + d)) | l <- ln, isJust $ M.lookup (l + d) ts]
+                                                    return (SubPlan $ M.insert i (qi, csi', tsi) ts', (NCol n [Col i surT]):cs')
+                                                    
+makeSubPlan _ [] _  _ = return (emptyPlan, [])
+makeSubPlan _ _ _ _ = $impossible
+                    
+-- | Compile a lambda where the argument variable is bound to the given expression                    
+compileLambda :: [AlgRes] -> Param -> GraphM AlgRes
+compileLambda args (ParAbstr _ xs e) = let pairs = zip xs args
+                                        in foldr (\(v, a) -> withBinding v a) (coreToAlgebra e) pairs
+compileLambda _ p = $impossible
+
+-- | Transform gamma for map function                
+algResv :: AlgNode -> (String, AlgRes) -> GraphM (String, AlgRes)
+algResv m (n, (q, cs, ts)) = do
+                                let projPairs = zip (leafNames cs) (leafNames cs)
+                                q' <- proj (("iter", inner):("pos","pos"):projPairs) =<< eqJoin "iter" outer q m
+                                return (n, (q', cs, ts))
+
+keys :: SubPlan -> [String]
+keys (SubPlan ts) = map (\i -> "item" ++ show i) $ M.keys ts 
+
+
+mergeTableStructure :: AlgNode -> SubPlan -> SubPlan -> GraphM SubPlan
+mergeTableStructure qo (SubPlan ts1') (SubPlan ts2') | M.null ts1' = return $ SubPlan ts2'
+                                                     | M.null ts2' = return $ SubPlan ts1'
+                                                     | otherwise = do
+                                                        rs <- mapM mergeBinds items
+                                                        return $ SubPlan $ M.fromList rs    
+    where
+        items = M.toList ts1'
+        mergeBinds :: (Int, AlgRes) -> GraphM (Int, AlgRes)
+        mergeBinds (i, (q1, cs1, ts1)) = do
+                                            let (q2, _cs2, ts2) = case M.lookup i ts2' of
+                                                                    Nothing -> error "jikes"
+                                                                    Just a -> a
+                                            let ks = keys ts1
+                                            let cols = leafNames cs1
+                                            let colsDiff = cols L.\\ ks
+                                            let projPairs = zip cols cols
+                                            let projPairsD = zip colsDiff colsDiff
+                                            let projPairsKs = zip ks $ repeat iterPrime
+                                            n1 <- attach ordCol natT (nat 1) q1
+                                            n2 <- attach ordCol natT (nat 2) q2
+                                            qo'' <- proj [(ordPrime, ordCol), (iterR, iterPrime), (oldCol, "item" ++ show i)] qo
+                                            qo' <- eqTJoin [(ordPrime, ordCol), (oldCol, "iter")] 
+                                                           (("iter", "iter"):(iterR, iterR):("pos", "pos"):(ordCol, ordCol):projPairs)
+                                                           qo''
+                                                           =<< union n1 n2
+                                            q <- rownum iterPrime ["iter", ordCol, "pos"] Nothing qo'
+                                            qr <- proj ((iterPrime, iterPrime):(ordCol, ordCol):projPairs) q
+                                            q' <- proj (("iter", iterR):("pos", "pos"):(projPairsD ++ projPairsKs)) q
+                                            ts' <- mergeTableStructure qr ts1 ts2
+                                            return (i, (q', cs1, ts'))
+                                            
+mergeTableStructureFirst :: AlgNode -> SubPlan -> SubPlan -> GraphM SubPlan
+mergeTableStructureFirst qo (SubPlan ts1') (SubPlan ts2') 
+                            | M.null ts1' = return $ SubPlan ts2'
+                            | M.null ts2' = return $ SubPlan ts1'
+                            | otherwise= do
+                                          rs <- mapM mergeBinds items
+                                          return $ SubPlan $ M.fromList rs
+     where
+        items = M.toList ts1'
+        mergeBinds :: (Int, AlgRes) -> GraphM (Int, AlgRes)
+        mergeBinds (i, (q1, cs1, ts1)) = do 
+                                            let (q2, _cs2, ts2) = ts2' M.! i
+                                            let ks = keys ts1
+                                            let cols = leafNames cs1
+                                            let colsDiff = cols L.\\ ks
+                                            let projPairs = zip cols cols
+                                            let projPairsD = zip colsDiff colsDiff
+                                            let projPairsKs = zip ks $ repeat iterPrime
+                                            qo'' <- (proj [(ordPrime, ordCol),(iterR, iterPrime),(oldCol, "item" ++ show i)] qo)
+                                            qo' <- eqTJoin [(ordPrime, ordCol), (oldCol, "iter")] 
+                                                           (("iter", "iter"):(iterR,iterR):("pos", "pos"):(ordCol, ordCol):(iterPrime, iterPrime) : projPairs) 
+                                                           qo''
+                                                           =<< rownum iterPrime ["iter", ordCol, "pos"] Nothing
+                                                            =<< flip union q2 =<< attach ordCol natT (nat 1) q1
+                                            qr <- proj ((iterPrime, iterPrime):(ordCol, ordCol):projPairs) qo'
+                                            q' <- proj (("iter", iterR):("pos", "pos"):(projPairsD ++ projPairsKs)) qo'
+                                            ts' <- mergeTableStructureFirst qr ts1 ts2
+                                            return (i, (q', cs1, ts'))
+                                            
+
+mergeTableStructureLast :: Int -> SubPlan -> GraphM SubPlan
+mergeTableStructureLast n (SubPlan ts1') = do
+                                            rs <- mapM updateBinds items
+                                            return $ SubPlan $ M.fromList rs
+    where
+        items = M.toList ts1'
+        updateBinds :: (Int, AlgRes) -> GraphM (Int, AlgRes)
+        updateBinds (i, (q1, cs1, ts1)) = do
+                                            q <- attach ordCol natT (nat $ toInteger n) q1
+                                            ts <- mergeTableStructureLast n ts1
+                                            return (i, (q, cs1, ts))
+                                            
+mergeTableStructureSeq :: Int -> SubPlan -> SubPlan -> GraphM SubPlan
+mergeTableStructureSeq n (SubPlan ts1') (SubPlan ts2') 
+                                | M.null ts1' = return $ SubPlan ts2'
+                                | M.null ts2' = return $ SubPlan ts1'
+                                | otherwise= do
+                                              rs <- mapM mergeBinds items
+                                              return $ SubPlan $ M.fromList rs
+    where
+        items = M.toList ts1'
+        mergeBinds :: (Int, AlgRes) -> GraphM (Int, AlgRes)
+        mergeBinds (i, (q1, cs1, ts1)) = do
+                                            let (q2, _cs2, ts2) = ts2' M.! i
+                                            q <- flip union q2 
+                                                    =<< attach ordCol natT (nat $ toInteger n) q1
+                                            ts <- mergeTableStructureSeq n ts1 ts2
+                                            return (i, (q, cs1, ts))
+
+-- Compilation for the first element of a list.
+-- For optimisation purposes we distinguish three cases:
+-- Singleton lists: compile these if they were just single values
+-- A list where the second element is also created through a list constructor
+--      that particular case allows for optimising on the rank operator, it is
+--      compiled to algebra in the listSequence function that does not perform rank.
+-- A list where the tail is the result of a computation, the tail is compiled as a
+--      normal expression. The result get an ord column attached and the is unified
+--      with the head of the list and then ranked.    
+listFirst :: CoreExpr -> GraphM AlgRes
+listFirst (Cons _ e1 (Nil _)) = coreToAlgebra e1
+listFirst (Cons _ e1 e2@(Cons _ _ _)) = do
+                                         (q1, cs1, ts1) <- coreToAlgebra e1
+                                         (q2, _cs2, ts2) <- listSequence e2 2
+                                         let cols = leafNames cs1
+                                         let ks = keys ts1
+                                         let colsDiff = cols L.\\ ks
+                                         let projPairs = (zip colsDiff colsDiff) ++ (zip ks $ repeat iterPrime) 
+                                         q' <- rownum iterPrime ["iter", ordCol, "pos"] Nothing
+                                                 =<< rank posPrime [(ordCol, Asc), ("pos", Asc)] 
+                                                     =<< flip union q2 =<< attach ordCol natT (nat 1) q1
+                                         q <- proj (("iter", "iter"):("pos", posPrime) : projPairs) q'
+                                         ts <- mergeTableStructureFirst q' ts1 ts2
+                                         return (q, cs1, ts) 
+listFirst (Cons _ e1 e2) = do
+                            (q1, cs1, ts1) <- coreToAlgebra e1
+                            (q2, _cs2, ts2) <- coreToAlgebra e2
+                            let cols = leafNames cs1
+                            let ks = keys ts1
+                            let colsDiff = cols L.\\ ks
+                            let projPairs = (zip colsDiff colsDiff) ++ (zip ks $ repeat iterPrime)
+                            n1 <- attach ordCol natT (nat 1) q1
+                            q' <- rownum iterPrime ["iter", ordCol, "pos"] Nothing
+                                    =<< rank posPrime [(ordCol, Asc), ("pos", Asc)]
+                                        =<< union n1 
+                                            =<< attach ordCol natT (nat 2) q2
+                            qr <- proj ((iterPrime, iterPrime):(ordCol, ordCol):(zip cols cols)) q'
+                            q <- proj (("iter", "iter"):("pos", posPrime):projPairs) q'
+                            ts <- mergeTableStructure qr ts1 ts2
+                            return (q, cs1, ts)
+listFirst _ = $impossible
+
+
+-- List sequence, doesn't perform the rank operation, that is carried out by listFirst.
+--  Three cases with similar motivation as listFirst.
+listSequence :: CoreExpr -> Int -> GraphM AlgRes
+listSequence (Cons _ e1 (Nil _)) n = do
+                                      (q1, cs1, ts1) <- coreToAlgebra e1
+                                      n1 <- attach ordCol natT (nat $ toEnum n) q1
+                                      ts <- mergeTableStructureLast n ts1
+                                      return (n1, cs1, ts)
+listSequence (Cons _ e1 e2@(Cons _ _ _)) n = do
+                                                (q1, cs1, ts1) <- coreToAlgebra e1
+                                                (q2, _cs2, ts2) <- listSequence e2 $ n + 1
+                                                n1 <- attach ordCol natT (nat $ toEnum n) q1
+                                                n2 <- union n1 q2
+                                                ts <- mergeTableStructureSeq n ts1 ts2
+                                                return (n2, cs1, ts)
+listSequence c@(Cons _ _ _) n = do
+                                 (q, cs, ts) <- listFirst c
+                                 n1 <- attach ordCol natT (nat $ toEnum n) q
+                                 ts' <- mergeTableStructureLast n ts
+                                 return (n1, cs, ts')
+listSequence _ _ = $impossible
+                                    
+-- Transform a record element into algebraic plan                             
+recElemToAlgebra :: RecElem -> GraphM AlgRes
+recElemToAlgebra (RecElem _ n e) = do
+                                     (q1, cs1, ts1) <- coreToAlgebra e
+                                     return (q1, [NCol n cs1], ts1)
+
+-- Transform a record into an algebraic plan                                     
+recElemsToAlgebra :: GraphM AlgRes -> RecElem -> GraphM AlgRes
+recElemsToAlgebra alg2 el = do
+                                (q1, cs1, (SubPlan ts1)) <- alg2
+                                (q2, cs2, (SubPlan ts2)) <- recElemToAlgebra el
+                                let offSet = colSize cs1
+                                let cs2' = incrCols offSet cs2
+                                let projPairs = zip (leafNames cs2') (leafNames cs2)
+                                let ts = SubPlan $ M.union ts1 $ M.mapKeysMonotonic (+ offSet) ts2
+                                n1 <- proj ((mkPrefixIter 1, "iter"):projPairs) q2
+                                n2 <- eqJoin "iter" (mkPrefixIter 1) q1 n1
+                                let projPairs' = zip (leafNames cs1) (leafNames cs1) ++ zip (leafNames cs2') (leafNames cs2')
+                                n3 <- proj (("iter", "iter"):("pos", "pos"):projPairs') n2
+                                return (n3, cs1 ++ cs2', ts)
+
+-- map forward transforms the environment etc into the versions needed to compute in
+-- a loop context. The result is (qv', qv, mapv, loopv, Gamv)
+mapForward :: Gam -> AlgNode -> Columns -> GraphM (AlgNode, AlgNode, AlgNode, AlgNode, Gam)
+mapForward gam q cs = do
+                          let csProj = zip (leafNames cs) (leafNames cs)
+                          qv' <- rownum inner ["iter", "pos"] Nothing q
+                          qv  <- proj (("iter", inner):("pos", posPrime):csProj)
+                                      =<< attach posPrime natT (nat 1) qv'
+                          mapv <- proj [(outer, "iter"), (inner, inner), (posPrime, "pos")] qv'
+                          loopv <- proj [("iter",inner)] qv'
+                          gamV <- transformGam algResv mapv gam
+                          return (qv', qv, mapv, loopv, gamV)
+
+-- clean innerPlans
+cleanInner :: AlgNode -> SubPlan -> GraphM SubPlan
+cleanInner q (SubPlan ps) = do 
+                             ps' <- sequence 
+                                [ do 
+                                    let item = "item" ++ show c
+                                    qo <- proj [(resCol, item)] q
+                                    let projPairs = zip (leafNames cs') (leafNames cs')
+                                    q'' <- proj (("iter", "iter"):("pos","pos"):projPairs)
+                                        =<< eqJoin resCol item qo q' 
+                                    ts'' <- cleanInner q'' ts'
+                                    return (c, (q'', cs', ts'')) | (c, (q', cs', ts')) <- M.toList ps]
+                             return (SubPlan $ M.fromList ps')
+ 
+-- Recalculate the position column, making it densely populated after this operation
+absPos :: AlgNode -> Columns -> GraphM AlgNode
+absPos q cs = let projPairs = zip (leafNames cs) (leafNames cs)
+               in proj (("iter", "iter"):("pos", "pos"):projPairs) 
+                    =<< rownum "pos" [posPrime] (Just "iter")
+                        =<< proj (("iter", "iter"):(posPrime, "pos"):projPairs) q
+                         
+-- Function to transform the column structure
+
+--From a typedcore column list to algebraic columns
+coreCol2AlgCol :: [T.Column] -> Columns
+coreCol2AlgCol cols = map (\(Column s t, i) -> NCol s $ fst $ typeToCols t i) cols'
+    where
+      cols' = zip cols [1..]
+
+--Translate core keys to algebraic keys
+key2Key :: Columns -> [Key] -> KeyInfos
+key2Key cs ks = map (\(Key k) -> map (\ki -> case getCol ki cs of
+                                                [(Col i _)] -> "item" ++ show i
+                                                [] -> $impossible
+                                                (NCol _ _) : _ -> $impossible
+                                                (Col _ _) : (_ : _) -> $impossible) k ) ks
+
+-- Get all the column names from the structure                                    
+leafNames :: Columns -> [String]
+leafNames cs = map (\c -> case c of
+                            (Col i _) -> "item" ++ show i
+                            _         -> error "Named column not allowed in leafNames") $ colLeafs cs
+
+leafNumbers :: Columns -> [Int]
+leafNumbers cs = map (\c -> case c of
+                            (Col i _) -> i
+                            _         -> error "Named column not allowed in LeafNumbers") $ colLeafs cs
+
+-- Get all the leaf columns, that is the columns that are actually a column
+colLeafs :: Columns -> Columns
+colLeafs (c@(Col _ _):xs) = (:) c $ colLeafs xs
+colLeafs ((NCol _ cs):xs) = colLeafs cs ++ colLeafs xs
+colLeafs []               = []
+
+-- Count the number of columns
+colSize :: Columns -> Int
+colSize = length . colLeafs
+
+-- Increment the column numbers by a given amount
+incrCols :: Int -> Columns -> Columns
+incrCols inc ((Col i t):xs)    = (Col (i + inc) t):(incrCols inc xs)
+incrCols inc ((NCol x i):xs) = (NCol x (incrCols inc i)):(incrCols inc xs)
+incrCols _   []              = [] 
+
+-- Find the lowest column number
+minCol :: Columns -> Int
+minCol c = minimum $ map (\c' -> case c' of
+                                    (Col i _) -> i
+                                    _         -> error "Named column not expected in minCol") $ colLeafs c
+
+-- Decrement the column numbers so that the lowest column number is 1 after applying
+decrCols :: Columns -> (Columns, Int)
+decrCols cols = let minV = minCol cols
+                 in (decr' (minV - 1) cols, minV  - 1)
+    where
+     decr' :: Int -> Columns -> Columns
+     decr' decr ((Col i t):xs)    = (flip Col t $ i - decr) : (decr' decr xs)
+     decr' decr ((NCol x i):xs) = (NCol x $ decr' decr i) : (decr' decr xs)
+     decr' _    []              = []
+
+-- Find the columns associated with a record label
+getCol :: String -> Columns -> Columns
+getCol n cs = getCol' cs
+    where
+     getCol' :: Columns -> Columns
+     getCol' ((Col _ _):xs)              = getCol' xs
+     getCol' ((NCol x i):xs) | x == n    = i
+                             | otherwise = getCol' xs
+     getCol' []                          = error $ show n ++ " in " ++ show cs --[]
+
+-- Transform Columns info into schema info for algebraic compilation
+colsToSchema :: Columns -> SchemaInfos
+colsToSchema ((Col i t):xs) = (:)("item" ++ show i, t) $ colsToSchema xs
+colsToSchema ((NCol _ cs):xs) = colsToSchema cs ++ colsToSchema xs
+colsToSchema [] = []
+
+-- Transform a type to columns structure
+typeToCols :: FType -> Int -> (Columns, Int)
+typeToCols (FRec recs) i = recsToCols recs i
+typeToCols FInt i = ([Col i AInt], i + 1)
+typeToCols FBool i = ([Col i ABool], i + 1)
+typeToCols FFloat i = ([Col i ADouble], i + 1)
+typeToCols FString i = ([Col i AStr], i + 1)
+typeToCols FUnit i = ([Col i AInt], i + 1)
+typeToCols (FList _) i = ([Col i ASur], i + 1)
+typeToCols (FVar _) i = ([Col i ANat], i + 1)
+typeToCols _ _ = $impossible
+
+-- Compile a record type to a column structure
+recsToCols :: [(RLabel, FType)] -> Int -> (Columns, Int)
+recsToCols ((RLabel s, ty):xs) i = let (cs, i') = typeToCols ty i
+                                       (cs', i'') = recsToCols xs i'
+                                    in ((NCol s cs):cs',  i'')
+recsToCols [] i = ([], i)
+recsToCols ((RGen _, _) : _) _ = $impossible
+recsToCols ((RVar _, _) : _) _ = $impossible
diff --git a/src/Database/Ferry/TypedCore/Convert/Specialize.hs b/src/Database/Ferry/TypedCore/Convert/Specialize.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Convert/Specialize.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-| Provides a function that can replace groupByN occurences by a more specific one-}
+module Database.Ferry.TypedCore.Convert.Specialize where
+
+import Database.Ferry.TypedCore.Convert.Traverse
+import Database.Ferry.TypedCore.Data.TypedCore
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.Impossible
+
+groupNSpecialize :: CoreExpr -> CoreExpr
+groupNSpecialize = traverse f
+    where
+        f :: FoldCore CoreExpr Param RecElem
+        f = idFoldCore {varF = fnS}
+        fnS :: Qual FType -> String -> CoreExpr
+        fnS t s = case s of
+                   "groupByN" -> case typeSize t of
+                                     n | 0 < n && n <= 6 -> Var t $ "groupBy" ++ (show n)
+                                       | otherwise       -> Var t "groupByN"
+                   _  -> (Var t s)
+        typeSize :: Qual FType -> Int
+        typeSize (_ :=> (FFn (FFn _ t2) _)) = case t2 of
+                                               (FRec r) -> length r
+                                               _        -> 0
+        typeSize _ = $impossible
diff --git a/src/Database/Ferry/TypedCore/Convert/Traverse.hs b/src/Database/Ferry/TypedCore/Convert/Traverse.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Convert/Traverse.hs
@@ -0,0 +1,65 @@
+{- | Provides a traverse method that given functions for parts of the AST traverses the AST and applies the function where appropriate -}
+module Database.Ferry.TypedCore.Convert.Traverse where
+    
+import Database.Ferry.TypedCore.Data.TypedCore
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.Common.Data.Base
+import Control.Monad
+
+-- | Datatype that contains the functions that are needed for a traversal
+data FoldCore b p r = FoldCore {binOpF :: Qual FType -> Op -> b -> b -> b
+                             ,constantF :: Qual FType -> Const -> b
+                             ,varF :: Qual FType -> String -> b
+                             ,appF :: Qual FType -> b -> p -> b
+                             ,letF :: Qual FType -> String -> b -> b -> b
+                             ,recF :: Qual FType -> [r] -> b
+                             ,consF :: Qual FType -> b -> b -> b
+                             ,nilF :: Qual FType -> b
+                             ,elemF :: Qual FType -> b -> String -> b
+                             ,tableF :: Qual FType -> String -> [Column] -> [Key] -> b
+                             ,ifF :: Qual FType -> b -> b -> b -> b
+                             ,pExprF :: Qual FType -> b -> p
+                             ,pAbstrF :: Qual FType -> [String] -> b -> p
+                             ,rRecEF :: Qual FType -> String -> b -> r}
+
+-- | Identity traversel
+idFoldCore :: FoldCore CoreExpr Param RecElem
+idFoldCore = FoldCore BinOp Constant Var App Let Rec Cons Nil Elem Table If ParExpr ParAbstr RecElem  
+
+-- | Monadic traversal
+mFoldCore :: Monad m => FoldCore (m CoreExpr) (m Param) (m RecElem)
+mFoldCore = FoldCore (\t o -> liftM2 (BinOp t o))
+                      (\t c -> return $ Constant t c)
+                      (\t s -> return $ Var t s)
+                      (\t -> liftM2 $ App t)
+                      (\t s -> liftM2 $ Let t s)
+                      (\t rs -> do
+                                 rs' <- sequence rs
+                                 return $ Rec t rs')
+                      (\t -> liftM2 $ Cons t)
+                      (\t -> return $ Nil t)
+                      (\t e s -> do
+                                  e' <- e
+                                  return $ Elem t e' s)
+                      (\t s c k -> return $ Table t s c k)
+                      (\t -> liftM3 $ If t)
+                      (\t -> liftM $ ParExpr t)
+                      (\t p -> liftM $ ParAbstr t p)
+                      (\t s -> liftM $ RecElem t s)
+                     
+
+-- | This function traverses the whole CoreExpr tree and applies the given function at every node after
+-- | that the function is applied to all its children.
+traverse :: (FoldCore b p r) -> CoreExpr -> b
+traverse f (BinOp t o e1 e2)              = (binOpF f) t o (traverse f e1) $ traverse f e2
+traverse f (Constant t c)                 = (constantF f) t c
+traverse f (Var t s)                      = (varF f) t s
+traverse f (App t e1 (ParExpr t2 e2))     = (appF f) t (traverse f e1) $ (pExprF f) t2 $ traverse f e2
+traverse f (App t e1 (ParAbstr t2 p e))   = (appF f) t (traverse f e1) $ (pAbstrF f) t2 p $ traverse f e
+traverse f (Let t s e1 e2)                = (letF f) t s (traverse f e1) $ traverse f e2
+traverse f (Rec t els)                    = (recF f) t $ map (\(RecElem t' s e) -> (rRecEF f) t' s $ traverse f e) els
+traverse f (Cons t e1 e2)                 = (consF f) t (traverse f e1) $ traverse f e2
+traverse f (Nil t)                        = (nilF f) t
+traverse f (Elem t e s)                   = (elemF f) t (traverse f e) s
+traverse f (If t e1 e2 e3)                = (ifF f) t (traverse f e1) (traverse f e2) $ traverse f e3
+traverse f (Table t s c k)                = (tableF f) t s c k
diff --git a/src/Database/Ferry/TypedCore/Data/Instances.hs b/src/Database/Ferry/TypedCore/Data/Instances.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Data/Instances.hs
@@ -0,0 +1,155 @@
+{- | Some typeclass instances belonging to the datatypes associated with typed core -}
+{-# LANGUAGE TypeSynonymInstances #-}
+module Database.Ferry.TypedCore.Data.Instances where
+    
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.TypedCore.Data.Substitution
+import Database.Ferry.TypedCore.Data.TypedCore
+import Database.Ferry.TypedCore.Data.TypeFunction
+
+import qualified Data.Set as S
+import qualified Data.Map as M
+
+{- | Run a substitution over a simple type-}
+instance Substitutable FType where
+  apply s (FList t)             = FList $ apply s t 
+  apply s (FFn t1 t2)           = FFn (apply s t1) (apply s t2)
+  apply s (FRec rs)             = FRec $ map (\(n, t) -> (apply s n, apply s t)) rs
+  apply s (FTF f t)             = evalTy $ FTF f $ apply s t
+  apply (t, _) v@(FVar _) = case M.notMember v t of
+                                    True -> v
+                                    False -> t M.! v
+  apply (t, _) v@(FGen _) = case M.notMember v t of
+                                True -> v
+                                False -> t M.! v
+  apply _    t                  = t -- If the substitution is not applied to a container type or variable just stop primitives cannot be substituted
+
+{- | Run a substitution over a qualified type -}
+instance Substitutable t => Substitutable (Qual t) where
+  apply s (preds:=> t) = (map (apply s) preds) :=> apply s t
+
+{- | Run a substitution over a predicate -}  
+instance Substitutable Pred where
+  apply s (IsIn c t) = IsIn c $ apply s t
+  apply s (Has r n t) = Has (apply s r) n (apply s t)  
+
+{- | Run a substitution over a typescheme, note that bound
+variables are *NOT* touched by a substitution -}                          
+instance Substitutable TyScheme where
+  apply s (Forall i r t) = Forall i r $ apply s t
+
+{- | Run a substitution over all types in the type environment -}    
+instance Substitutable TyEnv where
+  apply s m = M.map (apply s) m
+
+{- | Run a substitution over a list of substituable structures -}  
+instance Substitutable a => Substitutable [a] where
+  apply s m = map (apply s) m
+
+{- | Run a substitution over a typed AST -}  
+instance Substitutable CoreExpr where
+  apply s (BinOp t o c1 c2) = BinOp (apply s t) o (apply s c1) (apply s c2)
+--  apply s (UnaOp t o c)      = UnaOp (apply s t) o (apply s c)
+  apply s (Constant t c)    = Constant (apply s t) c
+  apply s (Var t x)         = Var (apply s t) x
+  apply s (App t c a)       = App (apply s t) (apply s c) (apply s a)
+  apply s (Let t x c1 c2)   = Let (apply s t) x (apply s c1) (apply s c2)
+  apply s (Rec t es)        = Rec (apply s t) $ map (apply s) es
+  apply s (Cons t c1 c2)    = Cons (apply s t) (apply s c1) (apply s c2)
+  apply s (Nil t)           = Nil (apply s t)
+  apply s (Elem t c f)      = Elem (apply s t) (apply s c) f
+  apply s (Table t n c k)   = Table (apply s t) n c k
+  apply s (If t c1 c2 c3)   = If (apply s t) (apply s c1) (apply s c2) (apply s c3)
+
+instance Substitutable Param where
+    apply s (ParExpr t c) = ParExpr (apply s t) (apply s c)
+    apply s (ParAbstr t pa c) = ParAbstr (apply s t) pa (apply s c)
+        
+instance Substitutable RecElem where
+    apply s (RecElem t x c) = RecElem (apply s t) x (apply s c)
+
+instance Substitutable RLabel where
+    apply (_, r) v = case M.notMember v r of
+                                      True -> v
+                                      False -> r M.! v
+    
+{- * Instances of VarContainer class-}
+  
+instance VarContainer FType where
+  ftv (FVar a)    = S.singleton a
+  ftv (FList t)   = ftv t
+  ftv (FRec s)    = S.unions $ map (ftv . snd) s
+  ftv (FFn t1 t2) = ftv t1 `S.union` ftv t2
+  ftv _           = S.empty
+  frv (FList t)   = frv t
+  frv (FRec s)    = S.unions $ map (\(r,t) -> S.union (frv r) (frv t)) s
+  frv (FFn t1 t2) = frv t1 `S.union` frv t2
+  frv _           = S.empty 
+  hasQVar (FList t) = hasQVar t
+  hasQVar (FRec s)  = and $ map (hasQVar . snd) s
+  hasQVar (FFn t1 t2) = hasQVar t1 && hasQVar t2
+  hasQVar (FGen _) = True
+  hasQVar _        = False
+  
+instance VarContainer TyScheme where
+  ftv (Forall _ _ t)  = ftv t 
+  frv (Forall _ _ t)  = frv t
+  hasQVar (Forall i _ _) = if i > 0 then True else False
+
+instance VarContainer t => VarContainer (Qual t) where
+  ftv (preds :=> t) = S.unions $ (ftv t):(map ftv preds)
+  frv (preds :=> t) = S.unions $ (frv t):(map frv preds)
+  hasQVar (preds :=> t) = (&&) (hasQVar t) $ and $ map hasQVar preds 
+
+instance VarContainer Pred where
+  ftv (IsIn _ t) = ftv t
+  ftv (Has t _ t2) = ftv t `S.union` ftv t2
+  frv (IsIn _ t) = frv t
+  frv (Has t _ t2) = frv t `S.union` frv t2
+  hasQVar (IsIn _ t) = hasQVar t
+  hasQVar (Has t _ t2) = hasQVar t && hasQVar t2
+
+instance VarContainer TyEnv where
+  ftv m = S.unions $ M.elems $ M.map ftv m
+  frv m = S.unions $ M.elems $ M.map frv m
+  hasQVar m = and $ map (hasQVar . snd) $ M.assocs m
+  
+instance VarContainer RLabel where
+  ftv _ = S.empty
+  frv (RVar i) = S.singleton i
+  frv _        = S.empty
+  hasQVar (RGen _) = True
+  hasQVar _        = False
+  
+instance HasType CoreExpr where
+  typeOf (BinOp t _ _ _) = t
+--  typeOf (UnaOp t o c)     = t
+  typeOf (Constant t _)    = t
+  typeOf (Var t _)         = t
+  typeOf (App t _ _)       = t
+  typeOf (Let t _ _ _)   = t
+  typeOf (Rec t _)        = t
+  typeOf (Cons t _ _)    = t
+  typeOf (Nil t)           = t
+  typeOf (Elem t _ _)      = t
+  typeOf (Table t _ _ _)   = t
+  typeOf (If t _ _ _)   = t
+  setType t (BinOp _ o c1 c2) = BinOp t o c1 c2
+--  setType t (UnaOp _ o c)     = UnaOp t o c
+  setType t (Constant _ c)    = Constant t c
+  setType t (Var _ x)         = Var t x    
+  setType t (App _ c a)       = App t c a  
+  setType t (Let _ x c1 c2)   = Let t x c1 c2
+  setType t (Rec _ es)        = Rec t es
+  setType t (Cons _ c1 c2)    = Cons t c1 c2
+  setType t (Nil _)           = Nil t
+  setType t (Elem _ c f)      = Elem t c f
+  setType t (Table _ n c k)   = Table t n c k
+  setType t (If _ c1 c2 c3)   = If t c1 c2 c3
+  
+  
+instance HasType Param where
+    typeOf (ParExpr t _) = t
+    typeOf (ParAbstr t _ _) = t
+    setType t (ParExpr _ e) = ParExpr t e
+    setType t (ParAbstr _ p e) = ParAbstr t p e
diff --git a/src/Database/Ferry/TypedCore/Data/Substitution.hs b/src/Database/Ferry/TypedCore/Data/Substitution.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Data/Substitution.hs
@@ -0,0 +1,19 @@
+{- | Defines substitutions -}
+{-# LANGUAGE TypeSynonymInstances #-}
+module Database.Ferry.TypedCore.Data.Substitution where
+    
+import Database.Ferry.TypedCore.Data.Type
+
+import qualified Data.Map as M
+
+-- | A substitution is either a substitution over a type or over a label
+type Subst = (TSubst, RSubst)
+-- | A substitution is a mapping from a record label to a new record label
+type RSubst = M.Map RLabel RLabel
+-- | A substitution is a mapping from a type variable to a type
+type TSubst = M.Map FType FType
+
+-- | The class substitutable exposes a function that applies a substitution to
+-- datatypes that are an instance of it.
+class Substitutable a where
+    apply :: Subst -> a -> a
diff --git a/src/Database/Ferry/TypedCore/Data/Type.hs b/src/Database/Ferry/TypedCore/Data/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Data/Type.hs
@@ -0,0 +1,106 @@
+{-| Type language -}
+{-# LANGUAGE GADTs, TypeSynonymInstances #-}
+module Database.Ferry.TypedCore.Data.Type where
+
+import qualified Data.Set as S
+import qualified Data.Map as M
+
+type Ident = String
+
+-- | Type environment is a mapping from identifiers to type schemes
+type TyEnv = M.Map Ident TyScheme
+
+type TyGens = Int
+type RecGens = Int
+
+-- | A type scheme represents a quantified type
+data TyScheme where
+    Forall :: TyGens -> RecGens -> Qual FType -> TyScheme
+ deriving Show
+
+infix 5 :=> 
+
+-- | A qualified type is a type with some predicates ([predicates] :=> type)
+data Qual t where
+  (:=>) :: [Pred] -> t -> Qual t
+   deriving Show
+
+-- | Predicates relating to records
+data Pred where
+ IsIn :: String -> FType -> Pred -- | name `IsIn` t -> t is a record (or type variable) that contains at least a field name
+ Has :: FType -> RLabel -> FType -> Pred -- | Similaar to IsIn but now with a type for the name
+  deriving (Show, Eq)
+
+-- | Type language 
+data FType where
+    FGen :: Int -> FType -- | Generalised type variable
+    FUnit :: FType -- | ()
+    FInt :: FType -- | Int
+    FFloat :: FType -- | Float
+    FString :: FType -- | String
+    FBool :: FType -- | Bool
+    FList :: FType -> FType -- | [a]
+    FVar :: Ident -> FType -- | a
+    FRec :: [(RLabel, FType)] -> FType -- | {x1 :: t1, ..., xn :: tn} 
+    FFn :: FType -> FType -> FType -- | t1 -> t2
+    FTF :: FTFn -> FType -> FType -- | f t1
+ deriving (Show, Eq, Ord)
+
+-- | Is t a primitive type? 
+isPrim :: FType -> Bool
+isPrim FInt = True
+isPrim FFloat = True
+isPrim FString = True
+isPrim FBool = True
+isPrim (FRec ls) = and $ map (isPrim . snd) ls
+isPrim _ = False
+
+-- | Language for record labels
+data RLabel where
+    RLabel :: String -> RLabel
+    RGen :: Int -> RLabel -- | Generalised record label
+    RVar :: String -> RLabel
+ deriving (Show, Eq, Ord)
+
+-- | Type functions 
+data FTFn where
+    Tr :: FTFn
+    Tr' :: FTFn
+ deriving (Show, Eq, Ord)
+
+-- * Function used to construct types 
+int :: FType
+int = FInt
+float :: FType
+float = FFloat
+string :: FType
+string = FString
+bool ::  FType
+bool = FBool
+list :: FType -> FType
+list t = FList t
+var :: Ident -> FType
+var i = FVar i
+rec :: [(RLabel, FType)] -> FType
+rec s = FRec s
+fn :: FType -> FType -> FType
+fn t1 t2 = FFn t1 t2
+genT :: Int -> FType
+genT i = FGen i  
+
+infixr 6 .->
+
+(.->) :: FType -> FType -> FType 
+t1 .-> t2 = fn t1 t2
+
+-- | A varcontainer can contain type variables, or record variables
+class VarContainer a where
+   ftv :: a -> S.Set Ident
+   frv :: a -> S.Set Ident
+   hasQVar :: a -> Bool
+
+-- | Everything that contains a type.   
+class HasType a where
+  typeOf :: a -> Qual FType
+  setType :: Qual FType -> a -> a
+  
diff --git a/src/Database/Ferry/TypedCore/Data/TypeClasses.hs b/src/Database/Ferry/TypedCore/Data/TypeClasses.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Data/TypeClasses.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Database.Ferry.TypedCore.Data.TypeClasses where
+    
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.Compiler.Error.Error
+import Database.Ferry.Impossible
+
+import qualified Data.Map as M
+
+-- Type Class stuff (based on M. P. Jones Typing Haskell in Haskell)
+
+type Class = ([Ident], [Inst])
+type Inst  = Qual Pred
+
+type ClassEnv = M.Map Ident Class
+
+type ClassEnvTransformer = ClassEnv -> Either FerryError ClassEnv
+
+infixr 5 <:>
+(<:>) :: ClassEnvTransformer -> ClassEnvTransformer -> ClassEnvTransformer
+(f <:> g) ce = do
+                ce' <- f ce
+                g ce'
+                
+defined :: Ident -> ClassEnv -> Bool
+defined = M.member
+
+addClass :: Ident -> [Ident] -> ClassEnvTransformer
+addClass c sc ce
+    | defined c ce    = Left $ ClassAlreadyDefinedError c
+    | any (not . flip defined ce) sc = Left $ SuperClassNotDefined c sc
+    | otherwise = Right $ M.insert c (sc, []) ce
+    
+addInstance :: [Pred] -> Pred -> ClassEnvTransformer
+addInstance ps p@(IsIn i _) ce | not (defined i ce) = Left $ ClassNotDefined i
+                               | otherwise          = Right $ M.insert i (c, inst:is) ce 
+                                 where 
+                                  (c, is) = getClass i ce
+                                  inst = ps :=> p 
+addInstance _ (Has _ _ _) _ = $impossible
+                                      
+getClass :: Ident -> ClassEnv -> Class
+getClass i m = m M.! i
+
+emptyClassEnv :: ClassEnv
+emptyClassEnv = M.empty
diff --git a/src/Database/Ferry/TypedCore/Data/TypeFunction.hs b/src/Database/Ferry/TypedCore/Data/TypeFunction.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Data/TypeFunction.hs
@@ -0,0 +1,31 @@
+{-| Handle the type functions related to records-}
+module Database.Ferry.TypedCore.Data.TypeFunction where
+
+import Database.Ferry.TypedCore.Data.Type
+
+-- | Evaluate the type function application to a type that doesn't contain a function    
+evalTy :: FType -> FType
+evalTy o@(FTF fn' t) = case applyTyFn fn' t of
+                        Right t' -> evalTy t'
+                        Left _  -> o
+evalTy (FList t) = FList $ evalTy t
+evalTy (FRec t) = FRec $ map (\(i,t') -> (i, evalTy t')) t
+evalTy (FFn t1 t2) = FFn (evalTy t1) $ evalTy t2
+evalTy t = t
+
+-- | Apply a type function to a type
+applyTyFn :: FTFn -> FType -> Either FType FType
+applyTyFn Tr (FList t) = Right $ FList $ FList t
+applyTyFn Tr (FRec ts) = Right $ FRec $ map (\(l, t) -> (l, FList t)) ts 
+applyTyFn Tr (FTF Tr' t) = Right $ t
+applyTyFn Tr (FTF Tr t) = case applyTyFn Tr t of
+                            Right t' -> applyTyFn Tr t'
+                            Left t' -> Left $ FTF Tr t'
+applyTyFn Tr (FVar v) = Left $ FTF Tr $ FVar v
+applyTyFn Tr t        = Left $ FTF Tr t
+applyTyFn Tr' (FList (FList t)) = Right $ FList t
+applyTyFn Tr' (FRec ts) = Right $ FRec $ map (\(l, t) -> (l, case t of 
+                                                              FList t' -> t'
+                                                              _       -> error "Not a list")) ts
+applyTyFn Tr' (FTF Tr t) = Right t 
+applyTyFn Tr' _ = error "Cannot apply Tr'"
diff --git a/src/Database/Ferry/TypedCore/Data/TypedCore.hs b/src/Database/Ferry/TypedCore/Data/TypedCore.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Data/TypedCore.hs
@@ -0,0 +1,52 @@
+{- | Datatypes describing typed AST -}
+{-# LANGUAGE GADTs #-}
+module Database.Ferry.TypedCore.Data.TypedCore where
+    
+import Database.Ferry.Common.Data.Base(Const)
+import Database.Ferry.TypedCore.Data.Type
+
+type Ident = String
+
+data Op where
+    Op :: String -> Op
+        deriving (Show)
+
+data CoreExpr where
+    BinOp :: (Qual FType) -> Op -> CoreExpr -> CoreExpr -> CoreExpr
+--    UnaOp :: (Qual FType) -> Op -> CoreExpr -> CoreExpr
+    Constant :: (Qual FType) -> Const -> CoreExpr
+    Var  :: (Qual FType) -> String -> CoreExpr
+    App :: (Qual FType) -> CoreExpr -> Param -> CoreExpr
+    Let :: (Qual FType) -> String -> CoreExpr -> CoreExpr -> CoreExpr
+    Rec :: (Qual FType) -> [RecElem] -> CoreExpr
+    Cons :: (Qual FType) -> CoreExpr -> CoreExpr -> CoreExpr
+    Nil :: (Qual FType) -> CoreExpr
+    Elem :: (Qual FType) -> CoreExpr -> String -> CoreExpr
+    Table :: (Qual FType) -> String -> [Column] -> [Key] -> CoreExpr
+    If :: (Qual FType) -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
+    deriving (Show)
+
+data RecElem where
+    RecElem :: (Qual FType) -> String -> CoreExpr -> RecElem
+    deriving (Show)
+
+data Param where
+     ParExpr :: (Qual FType) -> CoreExpr -> Param
+     ParAbstr :: (Qual FType) -> [String] -> CoreExpr -> Param
+         deriving (Show)
+
+{-
+data Pattern where
+    PVar :: String -> Pattern
+    Pattern :: [String] -> Pattern
+        deriving (Show)
+-}
+
+data Column where
+     Column :: String -> FType -> Column
+         deriving (Show)
+
+data Key where
+    Key :: [String] -> Key
+        deriving (Show)
+
diff --git a/src/Database/Ferry/TypedCore/Render/Dot.hs b/src/Database/Ferry/TypedCore/Render/Dot.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Render/Dot.hs
@@ -0,0 +1,122 @@
+{- | Transform a typed core AST into a dot graph -}
+module Database.Ferry.TypedCore.Render.Dot where
+
+import Database.Ferry.Common.Render.Dot
+import Database.Ferry.Common.Render.Pretty    
+import Database.Ferry.TypedCore.Data.TypedCore
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.Common.Data.Base
+import Database.Ferry.TypedCore.Render.Pretty()
+
+import qualified Data.List as L
+
+instance Dotify CoreExpr where
+    dot e = runDot $ toDot e
+
+toDot :: CoreExpr -> Dot Id
+toDot (BinOp t o e1 e2) = do
+                           let o' = (\(Op op) -> op) o  
+                           nId <- node [Label $ SLabel o', Color Green, Shape Circle]
+                           tId <- typeToDot t
+                           id1 <- toDot e1
+                           id2 <- toDot e2
+                           edge nId [id1, id2, tId]
+                           return nId
+toDot (Constant t c) = do
+                      let s = toString c
+                      nId <- node [Label $ SLabel s, Color Yellow, Shape Triangle]
+                      tId <- typeToDot t
+                      edge nId [tId]
+                      return nId
+toDot (Var t i) = do
+                    nId <- node [Label $ SLabel i, Color Red, Shape Triangle]
+                    tId <- typeToDot t
+                    edge nId [tId]
+                    return nId
+toDot (App t c ps) = do
+                     nId <- node [Label $ SLabel "$", Color Green, Shape Circle]
+                     tId <- typeToDot t
+                     fId <- toDot c
+                     pIds <- paramToDot ps
+                     edge nId [fId, pIds, tId]
+                     return nId
+toDot (Let t s e1 e2) = do
+                       nId <- node [Label $ SLabel "Let", Color Blue, Shape Rect]
+                       tId <- typeToDot t
+                       id0 <- node [Label $ SLabel s, Color Red, Shape Rect, TextColor White]
+                       id1 <- toDot e1
+                       id2 <- toDot e2
+                       edge nId [id0, id1, id2, tId]
+                       return nId
+toDot (Rec t es) = do
+                  nId <- node [Label $ SLabel "Rec", Color Blue, Shape Oval]
+                  tId <- typeToDot t
+                  eIds <- mapM recToDot es
+                  edge nId (eIds ++ [tId])
+                  return nId
+toDot (Cons t e1 e2) = do
+                     nId <- node [Label $ SLabel "Cons", Color Blue, Shape Oval]
+                     tId <- typeToDot t
+                     eIdh <- toDot e1
+                     eIdt <- toDot e2
+                     edge nId [eIdh, eIdt, tId]
+                     return nId
+toDot (Nil t)      = do
+                    nId <- node [Label $ SLabel "Nil", Color Blue, Shape Oval]
+                    tId <- typeToDot t
+                    edge nId [tId]
+                    return nId
+toDot (Elem t c s) = do
+                    nId <- node [Label $ SLabel ".", Color Green, Shape Circle]
+                    sId <- node [Label $ SLabel s, Color Red, Shape Triangle]
+                    tId <- typeToDot t
+                    cId <- toDot c
+                    edge nId [cId, sId, tId]
+                    return nId
+toDot (Table ty n cs ks) = do
+                         let label = VLabel $ ((HLabel [SLabel "Table:", SLabel n])
+                                            : [HLabel [SLabel $ n' ++ "::", SLabel $ prettyPrint t ] | (Column n' t) <- cs])
+                                            ++ [SLabel $ keyToString k | k <- ks]
+                         nId <- node [Shape Rect, Label label, Color Yellow]
+                         tId <- typeToDot ty
+                         edge nId [tId]
+                         return nId
+toDot (If t e1 e2 e3) = do
+                        nId <- node [Label $ SLabel "If", Color Blue, Shape Circle]
+                        tId <- typeToDot t
+                        eId1 <- toDot e1
+                        eId2 <- toDot e2
+                        eId3 <- toDot e3
+                        edge nId [eId1, eId2, eId3, tId]
+                        return nId
+                        
+
+paramToDot :: Param -> Dot Id
+paramToDot (ParExpr _ e) = toDot e
+paramToDot (ParAbstr t p e) = do
+                             nId <- node [Label $ SLabel "\\   ->", Color Blue, Shape Circle]
+                             tId <- typeToDot t
+                             pId <- node [Label $ SLabel (show p), Color Red, Shape Triangle]
+                             eId <- toDot e
+                             edge nId [pId, eId, tId]
+                             return nId
+
+{-                             
+patToDot :: Pattern -> Dot Id
+patToDot (PVar s) = node [Label $ SLabel s, Color Red, Shape Triangle]
+patToDot (Pattern s) = node [Label $ SLabel $  "(" ++ (concat $ L.intersperse ", " s) ++ ")", Color Red, Shape Triangle]
+-}
+                      
+recToDot :: RecElem -> Dot Id
+recToDot (RecElem t s e) = do
+                          nId <- node [Label $ SLabel s, Color Red, Shape Oval]
+                          tId <- typeToDot t
+                          eId <- toDot e
+                          edge nId [eId, tId]
+                          return nId
+
+keyToString :: Key -> String
+keyToString (Key ks) = "(" ++ (concat $ L.intersperse ", " ks) ++ ")"
+
+typeToDot :: Qual FType -> Dot Id
+typeToDot t = node [Label $ SLabel $ prettyPrint t, Color Gray, Shape Rect]
diff --git a/src/Database/Ferry/TypedCore/Render/Pretty.hs b/src/Database/Ferry/TypedCore/Render/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Render/Pretty.hs
@@ -0,0 +1,44 @@
+{- | Pretty print a type -}
+{-# LANGUAGE FlexibleInstances #-}
+module Database.Ferry.TypedCore.Render.Pretty where
+
+import Char    
+import Database.Ferry.Common.Render.Pretty
+import Database.Ferry.TypedCore.Data.Type
+
+instance Pretty FType where
+  pretty FUnit     _ = "()"
+  pretty FInt      _ = "Int"
+  pretty FFloat    _ = "Float"
+  pretty FString   _ = "String"
+  pretty FBool     _ = "Bool"
+  pretty (FList a) _ = "[" ++ pretty a 0 ++ "]"
+  pretty (FVar a)  _ = "a" ++ a
+  pretty (FRec a)  _ = case fst $ head a of
+                        RLabel r -> case and $ map isDigit $ r of
+                                    True -> "(" ++ mapIntersperseConcat (flip pretty 1) ", " (map snd a) ++ ")"
+                                    False -> "{" ++ mapIntersperseConcat (flip pretty 1) ", " a ++ "}"
+                        _ -> "{" ++ mapIntersperseConcat (flip pretty 1) ", " a ++ "}"
+  pretty (FFn t1 t2) _ = "(" ++ pretty t1 0 ++ ") -> " ++ pretty t2 0
+  pretty (FGen i) _ = "a" ++ show i
+  pretty (FTF f t) _ = "(" ++ pretty f 1 ++ " " ++ pretty t 0 ++ ")"
+  
+instance Pretty FTFn where
+  pretty Tr _ = "Tr"
+  pretty Tr' _ = "Tr'"
+  
+instance (Pretty a) => Pretty (Qual a) where
+    pretty (ps :=> t) _ = (mapIntersperseConcat (flip pretty 1) ", " ps) ++ " => " ++ pretty t 1   
+    
+instance Pretty Pred where
+    pretty (IsIn s t) _ = s ++ " " ++ pretty t 1
+    pretty (Has r f t) _ = pretty r 1 ++ " <: {" ++ pretty f 1 ++ " ::" ++ pretty t 1 ++ "}"
+
+instance Pretty (RLabel, FType) where
+   pretty (n, t) i = pretty n i ++ " :: " ++ pretty t i
+
+instance Pretty RLabel where
+    pretty (RLabel n) _ = n
+    pretty (RGen n) _ = "f" ++ show n
+    pretty (RVar n) _ = "f" ++ show n 
+    
diff --git a/src/Database/Ferry/TypedCore/Rewrite/Combinators.hs b/src/Database/Ferry/TypedCore/Rewrite/Combinators.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Rewrite/Combinators.hs
@@ -0,0 +1,75 @@
+{- | Helper functions to construct a typed AST -}
+{-# LANGUAGE TemplateHaskell #-}
+module Database.Ferry.TypedCore.Rewrite.Combinators where
+
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.TypedCore.Data.TypedCore
+import Database.Ferry.TypedCore.Data.Instances()
+import Database.Ferry.Impossible
+
+import qualified Data.List as L
+    
+-- | Count variable node, needs a specialized type in the AST and therefore still expects the type of the list
+countF :: Qual FType -> CoreExpr
+countF (q :=> t) = Var (q :=> t .-> int) "count"  
+
+-- | Wrap an expression that is to be passed as an argument to a function
+wrapArg :: CoreExpr -> Param
+wrapArg e = ParExpr (typeOf e) e
+
+-- | Apply equality operator to two expressions
+eq :: CoreExpr -> CoreExpr -> CoreExpr
+eq e1 e2 = BinOp ([] :=> FBool) (Op "==") e1 e2
+
+-- | Apply negation to expression
+notF :: CoreExpr -> CoreExpr
+notF e = App ([] :=> FBool) (Var ([] :=> FBool .-> FBool) "not") (ParExpr (typeOf e) e)    
+
+-- | Apply length function to expression
+lengthF :: CoreExpr -> CoreExpr
+lengthF e = let (q :=> t) = typeOf e
+            in App ([] :=> FInt) (Var (q :=> t .-> FInt) "length") (ParExpr (typeOf e) e)
+
+minPF :: CoreExpr -> CoreExpr -> CoreExpr
+minPF e1 e2 = let (q1 :=> t1) = typeOf e1
+                  (q2 :=> t2) = typeOf e2
+                  fn' = Var (q1 `L.union` q2 :=> t1 .-> t2 .-> FInt) "minP"
+                  app1 = App (q2 :=> t2 .-> FInt) fn' (ParExpr (typeOf e1) e1)
+               in App ([] :=> FInt) app1 (ParExpr (typeOf e2) e2)
+               
+-- | Create the zip variable node with specialized function type
+zipF :: Qual FType -> Qual FType -> CoreExpr
+zipF (q1 :=> FList t1) (q2 :=> FList t2) = Var ((q1 `L.union` q2) :=> FList t1 .-> FList t2 .-> (FList $ rec [(RLabel "1", t1), (RLabel "2", t2)])) "zip"
+zipF _ _ = $impossible
+
+-- | Create a typed let binding node                                          
+binding :: String -> CoreExpr -> CoreExpr -> CoreExpr
+binding s e eb = Let (typeOf eb) s e eb
+
+-- | Zip two list
+zipC :: CoreExpr -> CoreExpr -> CoreExpr
+zipC e1 e2 = let ty1 = typeOf e1
+                 ty2@(_ :=> t2) = typeOf e2
+                 zipV = zipF ty1 ty2
+                 (q :=> zipT) = zippedTy ty1 ty2 
+                 app1T = q :=> t2 .-> zipT
+              in App (q :=> zipT) (App app1T zipV (ParExpr ty1 e1)) (ParExpr ty2 e2)
+              
+-- | All variable node                   
+allN :: CoreExpr
+allN = Var ([] :=> list FBool .-> FBool) "all"
+
+mapN :: Qual FType -> Qual FType -> CoreExpr
+mapN (q1 :=> t1) (q2 :=> t2) = Var (q1 `L.union` q2 :=> t1 .-> t2 .-> list FBool) "map"
+
+-- | Chain two boolean expression together in an and relation    
+andExpr :: CoreExpr -> CoreExpr -> CoreExpr
+andExpr = BinOp ([] :=> FBool) (Op "&&")
+
+orExpr :: CoreExpr -> CoreExpr -> CoreExpr
+orExpr = BinOp ([] :=> FBool) (Op "||")
+
+-- | Return the type that two lists that are zipped would result in
+zippedTy :: Qual FType -> Qual FType -> Qual FType
+zippedTy (q1 :=> (FList t1)) (q2 :=> (FList t2)) = (q1 `L.union` q2) :=> (FList $ rec [(RLabel "1", t1), (RLabel "2", t2)])
+zippedTy _ _ = $impossible
diff --git a/src/Database/Ferry/TypedCore/Rewrite/OpRewrite.hs b/src/Database/Ferry/TypedCore/Rewrite/OpRewrite.hs
new file mode 100644
--- /dev/null
+++ b/src/Database/Ferry/TypedCore/Rewrite/OpRewrite.hs
@@ -0,0 +1,175 @@
+{-| Rewrite operators. 
+This means that operators on structures are expanded and applied to their individual components. -}
+{-# LANGUAGE TemplateHaskell #-}
+module Database.Ferry.TypedCore.Rewrite.OpRewrite where
+    
+import Database.Ferry.TypedCore.Data.Type
+import Database.Ferry.TypedCore.Data.TypedCore
+import Database.Ferry.TypedCore.Convert.Traverse
+import Database.Ferry.TypedCore.Data.Instances()
+import Database.Ferry.TypedCore.Rewrite.Combinators
+
+import Database.Ferry.Impossible
+
+import Control.Monad.State
+
+type Rewrite = State Int
+
+getFreshIdentifier :: Rewrite String
+getFreshIdentifier = do
+                        n <- get
+                        put $ n + 1
+                        return $ "_rw" ++ show n
+
+getFreshVar :: Rewrite (Qual FType -> CoreExpr)
+getFreshVar = do
+                i <- getFreshIdentifier
+                return (\t -> Var t i)
+                
+runRewrite :: Rewrite a -> a
+runRewrite i = fst $ runState i 1
+                
+rewrite :: CoreExpr -> CoreExpr
+rewrite = runRewrite . rewrite' 
+
+rewrite' :: CoreExpr -> Rewrite CoreExpr
+rewrite' = traverse rules
+    where
+     rules = mFoldCore {binOpF = opRewrite, appF = appRewrite}
+
+appRewrite :: Qual FType -> Rewrite CoreExpr -> Rewrite Param -> Rewrite CoreExpr
+appRewrite qt e arg = do
+                        e' <- e
+                        arg' <- arg
+                        case (e', arg') of
+                            (App _ (Var _ "concatMap") f, e2) -> return $ concatMapR qt f e2
+                            (Var _ "fst", ParExpr _ e2) -> return $ Elem qt e2 "1"
+                            (Var _ "snd", ParExpr _ e2) -> return $ Elem qt e2 "2"
+                            _                           -> return $ App qt e' arg'
+
+opRewrite :: Qual FType -> Op -> Rewrite CoreExpr -> Rewrite CoreExpr -> Rewrite CoreExpr
+opRewrite qt (Op op) e1 e2 = do
+                              e1' <- e1
+                              e2' <- e2
+                              v1 <- getFreshIdentifier
+                              v2 <- getFreshIdentifier
+                              let (_ :=> ty1) = typeOf e1'
+                              case (ty1, op) of
+                                  (FList _t, "==") -> liftM (addBindings v1 v2 e1' e2') $ eqListExpr v1 v2 e1' e2'
+                                  (FRec _t, "==") -> liftM (addBindings v1 v2 e1' e2') $ eqRecExpr v1 v2 e1' e2'
+                                  (_ty, "!=") -> liftM (addBindings v1 v2 e1' e2') $ notEq e1' e2'
+                                  (FList _t, "<") -> liftM (addBindings v1 v2 e1' e2') $ ordList v1 v2 e1' e2' 
+                                  (FRec _t, "<") -> liftM (addBindings v1 v2 e1' e2') $ ordRec "<" v1 v2 e1' e2'
+                                  (FList _t, ">") -> liftM (addBindings v1 v2 e1' e2') $ ordList v2 v1 e2' e1' 
+                                  (FRec _t, ">") -> liftM (addBindings v1 v2 e1' e2') $ ordRec ">" v1 v2 e1' e2'
+                                  (_t, "<=") -> liftM (addBindings v1 v2 e1' e2') $ opOrEq "<" v1 v2 e1' e2'
+                                  (_t, ">=") -> liftM (addBindings v1 v2 e1' e2') $ opOrEq ">" v1 v2 e1' e2'
+                                  (_t, o) -> return $ BinOp qt (Op o) e1' e2'
+
+concatMapR :: Qual FType -> Param -> Param -> CoreExpr
+concatMapR qt@(q :=> rt) f e = let (_ :=> mft) = typeOf f
+                                   (_ :=> lt) = typeOf e
+                                in App qt (Var (q :=> (list rt .-> rt)) "concat")
+                                         (ParExpr (q :=> list rt) (App (q :=> rt) 
+                                                                    (App (q :=> (lt .-> rt))  (Var (q :=> (mft .-> lt .-> rt)) "map") f) e))
+
+addBindings :: String -> String -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
+addBindings v1 v2 val1 val2 val3 = Let ([] :=> FBool) v1 val1 
+                                    $ Let ([] :=> FBool) v2 val2 val3
+                                    
+
+opOrEq :: String -> String -> String -> CoreExpr -> CoreExpr -> Rewrite CoreExpr
+opOrEq op id1 id2 v1 v2 = let var1 = Var (typeOf v1) id1
+                              var2 = Var (typeOf v2) id2
+                           in rewrite' $ BinOp ([] :=> FBool) (Op "||") 
+                                            (BinOp ([] :=> FBool) (Op op) var1 var2) 
+                                            (BinOp ([] :=> FBool) (Op "==") var1 var2)
+
+ordRec :: String -> String -> String -> CoreExpr -> CoreExpr -> Rewrite CoreExpr
+ordRec op id1 id2 v1 v2 = let (q :=> FRec ls) = typeOf v1
+                              var1 = Var (typeOf v1) id1
+                              var2 = Var (typeOf v2) id2
+                              els = [(Elem (q :=> t) var1 l, Elem (q :=> t) var2 l) | (RLabel l, t) <- ls]
+                           in rewrite' $ recCompExpr op els
+
+recCompExpr :: String -> [(CoreExpr, CoreExpr)] -> CoreExpr
+recCompExpr op [(v1, v2)] = BinOp ([] :=> FBool) (Op op) v1 v2
+recCompExpr op ((v1, v2):vs) = let opE = BinOp ([] :=> FBool) (Op op) v1 v2
+                                   eqE = BinOp ([] :=> FBool) (Op "==") v1 v2
+                                in BinOp ([] :=> FBool) (Op "||") opE 
+                                    $ BinOp ([] :=> FBool) (Op "&&") eqE 
+                                      $ recCompExpr op vs
+recCompExpr _ [] = $impossible
+
+ordList :: String -> String -> CoreExpr -> CoreExpr -> Rewrite CoreExpr
+ordList id1 id2 val1 val2 = let t1@(_ :=> (FList _)) = typeOf val1
+                                t2@(_ :=> (FList _)) = typeOf val2
+                                var1 = Var t1 id1
+                                var2 = Var t2 id2
+                                lens = BinOp ([] :=> FBool) (Op "<") (lengthF var1) (lengthF var2)
+                                eqMinPf = (minPF var1 var2) `eq` (minPF var2 var1)
+                                ltMinPf = BinOp ([] :=> FBool) (Op "<") (minPF var1 var2) $ minPF var2 var1
+                             in rewrite' $ flip orExpr ltMinPf $ andExpr lens eqMinPf
+                         
+eqRecExpr :: String -> String -> CoreExpr -> CoreExpr -> Rewrite CoreExpr
+eqRecExpr id1 id2 val1 val2 = do
+                                let t1@(q1 :=> (FRec ls1)) = typeOf val1
+                                let t2@(_ :=> (FRec _)) = typeOf val2
+                                let var1 = Var t1 id1
+                                let var2 = Var t2 id2
+                                let eqs = [recElemEq l (q1 :=> ty) var1 var2 | (RLabel l, ty) <- ls1]
+                                eqs' <- sequence $ map rewrite' eqs
+                                return $ foldl1 andExpr eqs'
+                                
+recElemEq :: String -> Qual FType -> CoreExpr -> CoreExpr -> CoreExpr
+recElemEq lab (q :=> t) v1 v2 = let el1 = Elem (q :=> t) v1 lab
+                                    el2 = Elem (q :=> t) v2 lab
+                                 in el1 `eq` el2
+                                    
+    
+                                    
+-- | Rewrite of list equality
+eqListExpr :: String -> String -> CoreExpr -> CoreExpr -> Rewrite CoreExpr
+eqListExpr id1 id2 val1 val2 = do
+                                let t1 = typeOf val1
+                                let t2 = typeOf val2
+                                let var1 = Var t1 id1
+                                let var2 = Var t2 id2
+                                elEq <- elemEq var1 var2
+                                return $ andExpr (eqLength var1 var2) elEq
+    
+-- | Given two list expressions returns an expression that checks that they have equal length
+eqLength :: CoreExpr -> CoreExpr -> CoreExpr
+eqLength e1 e2 = let (q1 :=> t1) = typeOf e1
+                     (q2 :=> t2) = typeOf e2
+                     count1 = App ([] :=> FInt) (countF (q1 :=> t1 .-> FInt)) $ wrapArg e1
+                     count2 = App ([] :=> FInt) (countF (q2 :=> t2 .-> FInt)) $ wrapArg e2
+                  in BinOp ([] :=> FBool) (Op "==") count1 count2
+
+-- | Given two lists of equal length compute elementwise equality
+elemEq :: CoreExpr -> CoreExpr -> Rewrite CoreExpr
+elemEq e1 e2 = do
+                let t1 = typeOf e1
+                let t2 = typeOf e2
+                let zipE = zipC e1 e2
+                eqA  <- eqAbstr t1 t2
+                let (qE :=> tE) = typeOf zipE
+                let mapNode = mapN (typeOf eqA) (qE :=> tE)
+                let app1 = App (qE :=> tE .-> list FBool) mapNode eqA
+                let app2 = App ([] :=> list FBool) app1 (ParExpr (qE :=> tE) zipE)
+                return $ App ([] :=> FBool) allN (ParExpr (typeOf app2) app2) 
+
+eqAbstr :: Qual FType -> Qual FType -> Rewrite Param
+eqAbstr ty1@(q1 :=> FList t1) ty2@(q2 :=> FList t2) = 
+          do
+            f <- getFreshIdentifier
+            let ty@(q :=> t) = zippedTy ty1 ty2
+            let fV = Var ty f
+            let el1 = Elem (q1 :=> t1) fV "1"
+            let el2 = Elem (q2 :=> t2) fV "2"
+            eqE <- rewrite' $ BinOp ([] :=> FBool) (Op "==") el1 el2
+            return $ ParAbstr (q :=> t .-> FBool) [f] eqE    
+eqAbstr _ _ = $impossible
+
+notEq :: CoreExpr -> CoreExpr -> Rewrite CoreExpr
+notEq e1 e2 = rewrite' $ notF (BinOp ([] :=> FBool) (Op "==") e1 e2)