diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c)2012, Jeremy Shaw
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * 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.
+
+    * Neither the name of Jeremy Shaw nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS 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 COPYRIGHT
+OWNER 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,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/ditto.cabal b/ditto.cabal
new file mode 100644
--- /dev/null
+++ b/ditto.cabal
@@ -0,0 +1,41 @@
+Name:          ditto
+Version:       0.0.1.0
+Synopsis:      ditto is a type-safe HTML form generation and validation library
+Description:   ditto follows in the footsteps of formlets and
+               digestive-functors <= 0.2. It provides a
+               type-safe and composable method for generating
+               an HTML form that includes validation.
+License:       BSD3
+License-file:  LICENSE
+Author:        Jeremy Shaw, Jasper Van der Jeugt <m@jaspervdj.be>
+Maintainer:    Zachary Churchill <zacharyachurchill@gmail.com>
+Copyright:     2012 Jeremy Shaw, Jasper Van der Jeugt, SeeReason Partners LLC
+               2019 Zachary Churchill
+Category:      Web
+Build-type:    Simple
+Cabal-version: >=1.6
+tested-with:   GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.3, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.6.3
+
+source-repository head
+    type:     git
+    location: https://github.com/Happstack/ditto.git
+
+library
+  ghc-options: -Wall
+  exposed-modules: 
+    Ditto
+    Ditto.Backend
+    Ditto.Core
+    Ditto.Generalized
+    Ditto.Generalized.Named
+    Ditto.Proof
+    Ditto.Result
+  build-depends:       
+      base             >= 4    && < 5
+    , containers       >= 0.4  && < 0.7
+    , mtl              >= 2.0  && < 2.3
+    , semigroups       >= 0.16 && < 0.20
+    , text             >= 0.11 && < 1.3
+    , bifunctors       >= 5.5  && < 5.7
+  hs-source-dirs:      src
+
diff --git a/src/Ditto.hs b/src/Ditto.hs
new file mode 100644
--- /dev/null
+++ b/src/Ditto.hs
@@ -0,0 +1,14 @@
+module Ditto
+    ( module Data.Monoid
+    , module Ditto.Backend
+    , module Ditto.Core
+    , module Ditto.Result
+    , module Ditto.Proof
+    )
+    where
+
+import Data.Monoid
+import Ditto.Backend
+import Ditto.Core
+import Ditto.Result
+import Ditto.Proof
diff --git a/src/Ditto/Backend.hs b/src/Ditto/Backend.hs
new file mode 100644
--- /dev/null
+++ b/src/Ditto/Backend.hs
@@ -0,0 +1,89 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+
+{- |
+This module contains two classes. 'FormInput' is a class which is parameterized over the @input@ type used to represent form data in different web frameworks. There should be one instance for each framework, such as Happstack, Snap, WAI, etc.
+
+The 'FormError' class is used to map error messages into an application specific error type.
+
+-}
+module Ditto.Backend where
+
+import Data.Text (Text)
+import Ditto.Result (FormId)
+import qualified Data.Text as T
+
+-- | an error type used to represent errors that are common to all backends
+--
+-- These errors should only occur if there is a bug in the ditto-*
+-- packages. Perhaps we should make them an 'Exception' so that we can
+-- get rid of the 'FormError' class.
+data CommonFormError input
+  = InputMissing FormId
+  | NoStringFound input
+  | NoFileFound input
+  | MultiFilesFound input
+  | MultiStringsFound input
+  | MissingDefaultValue
+  deriving (Eq, Ord, Show)
+
+-- | some default error messages for 'CommonFormError'
+commonFormErrorStr
+  :: (input -> String) -- ^ show 'input' in a format suitable for error messages
+  -> CommonFormError input -- ^ a 'CommonFormError'
+  -> String
+commonFormErrorStr showInput cfe =
+  case cfe of
+    (InputMissing formId) -> "Input field missing for " ++ show formId
+    (NoStringFound input) -> "Could not extract a string value from: " ++ showInput input
+    (NoFileFound input) -> "Could not find a file associated with: " ++ showInput input
+    (MultiFilesFound input) -> "Found multiple files associated with: " ++ showInput input
+    (MultiStringsFound input) -> "Found multiple strings associated with: " ++ showInput input
+    MissingDefaultValue -> "Missing default value."
+
+-- | A Class to lift a 'CommonFormError' into an application-specific error type
+class FormError e where
+
+  type ErrorInputType e
+
+  commonFormError :: (CommonFormError (ErrorInputType e)) -> e
+
+-- | Class which all backends should implement.
+--
+class FormInput input where
+
+  -- |@input@ is here the type that is used to represent a value
+  -- uploaded by the client in the request.
+  type FileType input
+
+  -- | Parse the input into a string. This is used for simple text fields
+  -- among other things
+  --
+  getInputString :: (FormError error, ErrorInputType error ~ input) => input -> Either error String
+  getInputString input =
+    case getInputStrings input of
+      [] -> Left (commonFormError $ NoStringFound input)
+      [s] -> Right s
+      _ -> Left (commonFormError $ MultiStringsFound input)
+
+  -- | Should be implemented
+  --
+  getInputStrings :: input -> [String]
+
+  -- | Parse the input value into 'Text'
+  --
+  getInputText :: (FormError error, ErrorInputType error ~ input) => input -> Either error Text
+  getInputText input =
+    case getInputTexts input of
+      [] -> Left (commonFormError $ NoStringFound input)
+      [s] -> Right s
+      _ -> Left (commonFormError $ MultiStringsFound input)
+
+  -- | Can be overriden for efficiency concerns
+  --
+  getInputTexts :: input -> [Text]
+  getInputTexts = map T.pack . getInputStrings
+
+  -- | Get a file descriptor for an uploaded file
+  --
+  getInputFile :: (FormError error, ErrorInputType error ~ input) => input -> Either error (FileType input)
diff --git a/src/Ditto/Core.hs b/src/Ditto/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/Ditto/Core.hs
@@ -0,0 +1,413 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+{- |
+This module defines the 'Form' type, its instances, core manipulation functions, and a bunch of helper utilities.
+-}
+module Ditto.Core where
+
+import Control.Applicative (Applicative ((<*>), pure))
+import Control.Monad.Reader (MonadReader (ask), ReaderT, runReaderT)
+import Control.Monad.State (MonadState (get, put), StateT, evalStateT)
+import Control.Monad.Trans (lift)
+import Data.Biapplicative (Biapplicative ((<<*>>), bipure))
+import Data.Bifunctor (Bifunctor (..))
+import Data.Monoid (Monoid (mappend, mempty))
+import qualified Data.Semigroup as SG
+import Data.Text.Lazy (Text, unpack)
+import Ditto.Result (FormId (..), FormRange (..), Result (..), unitRange, zeroId)
+
+------------------------------------------------------------------------------
+-- * Proved
+------------------------------------------------------------------------------
+
+-- | Proved records a value, the location that value came from, and something that was proved about the value.
+data Proved proofs a
+  = Proved
+      { proofs :: proofs
+      , pos :: FormRange
+      , unProved :: a
+      }
+  deriving Show
+
+instance Functor (Proved ()) where
+  fmap f (Proved () posi a) = Proved () posi (f a)
+
+-- | Utility Function: trivially prove nothing about ()
+unitProved :: FormId -> Proved () ()
+unitProved formId =
+  Proved
+    { proofs = ()
+    , pos = unitRange formId
+    , unProved = ()
+    }
+
+------------------------------------------------------------------------------
+-- * FormState
+------------------------------------------------------------------------------
+
+-- | inner state used by 'Form'.
+type FormState m input = ReaderT (Environment m input) (StateT FormRange m)
+
+-- | used to represent whether a value was found in the form
+-- submission data, missing from the form submission data, or expected
+-- that the default value should be used
+data Value a
+  = Default
+  | Missing
+  | Found a
+
+-- | Utility function: Get the current input
+--
+getFormInput :: Monad m => FormState m input (Value input)
+getFormInput = getFormId >>= getFormInput'
+
+-- | Utility function: Gets the input of an arbitrary 'FormId'.
+--
+getFormInput' :: Monad m => FormId -> FormState m input (Value input)
+getFormInput' id' = do
+  env <- ask
+  case env of
+    NoEnvironment -> pure Default
+    Environment f ->
+      lift $ lift $ f id'
+
+-- | Utility function: Get the current range
+--
+getFormRange :: Monad m => FormState m i FormRange
+getFormRange = get
+
+-- | The environment is where you get the actual input per form.
+--
+-- The 'NoEnvironment' constructor is typically used when generating a
+-- view for a GET request, where no data has yet been submitted. This
+-- will cause the input elements to use their supplied default values.
+--
+-- Note that 'NoEnviroment' is different than supplying an empty environment.
+data Environment m input
+  = Environment (FormId -> m (Value input))
+  | NoEnvironment
+
+instance (SG.Semigroup input, Monad m) => SG.Semigroup (Environment m input) where
+
+  NoEnvironment <> x = x
+  x <> NoEnvironment = x
+  (Environment env1) <> (Environment env2) =
+    Environment $ \id' ->
+      do
+        r1 <- (env1 id')
+        r2 <- (env2 id')
+        case (r1, r2) of
+          (Missing, Missing) -> pure Missing
+          (Default, Missing) -> pure Default
+          (Missing, Default) -> pure Default
+          (Default, Default) -> pure Default
+          (Found x, Found y) -> pure $ Found (x SG.<> y)
+          (Found x, _) -> pure $ Found x
+          (_, Found y) -> pure $ Found y
+
+-- | Not quite sure when this is useful and so hard to say if the rules for combining things with Missing/Default are correct
+instance (SG.Semigroup input, Monad m) => Monoid (Environment m input) where
+
+  mempty = NoEnvironment
+
+  mappend = (SG.<>)
+
+-- | Utility function: returns the current 'FormId'. This will only make sense
+-- if the form is not composed
+--
+getFormId :: Monad m => FormState m i FormId
+getFormId = do
+  FormRange x _ <- get
+  pure x
+
+-- | Utility function: increment the current 'FormId'.
+incFormId :: Monad m => FormState m i ()
+incFormId = do
+  FormRange _ endF1 <- get
+  put $ unitRange endF1
+
+-- | A view represents a visual representation of a form. It is composed of a
+-- function which takes a list of all errors and then produces a new view
+--
+newtype View error v
+  = View
+      { unView :: [(FormRange, error)] -> v
+      }
+  deriving (SG.Semigroup, Monoid)
+
+instance Functor (View e) where
+  fmap f (View g) = View $ f . g
+
+------------------------------------------------------------------------------
+-- * Form
+------------------------------------------------------------------------------
+
+-- | a 'Form' contains a 'View' combined with a validation function
+-- which will attempt to extract a value from submitted form data.
+--
+-- It is highly parameterized, allowing it work in a wide variety of
+-- different configurations. You will likely want to make a type alias
+-- that is specific to your application to make type signatures more
+-- manageable.
+--
+--   [@m@] A monad which can be used by the validator
+--
+--   [@input@] A framework specific type for representing the raw key/value pairs from the form data
+--
+--   [@error@] A application specific type for error messages
+--
+--   [@view@] The type of data being generated for the view (HSP, Blaze Html, Heist, etc)
+--
+--   [@proof@] A type which names what has been proved about the pure value. @()@ means nothing has been proved.
+--
+--   [@a@] Value pure by form when it is successfully decoded, validated, etc.
+--
+--
+-- This type is very similar to the 'Form' type from
+-- @digestive-functors <= 0.2@. If @proof@ is @()@, then 'Form' is an
+-- applicative functor and can be used almost exactly like
+-- @digestive-functors <= 0.2@.
+newtype Form m input error view proof a = Form {unForm :: FormState m input (View error view, m (Result error (Proved proof a)))}
+
+instance (Monad m) => Bifunctor (Form m input view error) where
+  bimap f g (Form frm) =
+    Form $ do
+      (view1, mval) <- frm
+      val <- lift $ lift $ mval
+      case val of
+        (Ok (Proved p posi a)) -> pure (view1, pure $ Ok (Proved (f p) posi (g a)))
+        (Error errs) -> pure (view1, pure $ Error errs)
+
+instance (Monoid view, Monad m) => Biapplicative (Form m input error view) where
+  bipure p a =
+    Form $ do
+      i <- getFormId
+      pure (mempty, pure $ Ok (Proved p (unitRange i) a))
+
+  (Form frmF) <<*>> (Form frmA) =
+    Form $ do
+      ((view1, mfok), (view2, maok)) <-
+        bracketState $ do
+          res1 <- frmF
+          incFormId
+          res2 <- frmA
+          pure (res1, res2)
+      fok <- lift $ lift $ mfok
+      aok <- lift $ lift $ maok
+      case (fok, aok) of
+        (Error errs1, Error errs2) -> pure (view1 `mappend` view2, pure $ Error $ errs1 ++ errs2)
+        (Error errs1, _) -> pure (view1 `mappend` view2, pure $ Error $ errs1)
+        (_, Error errs2) -> pure (view1 `mappend` view2, pure $ Error $ errs2)
+        (Ok (Proved p (FormRange x _) f), Ok (Proved q (FormRange _ y) a)) ->
+          pure
+            ( view1 `mappend` view2
+            , pure $ Ok $ Proved
+              { proofs = p q
+              , pos = FormRange x y
+              , unProved = f a
+              }
+            )
+
+bracketState :: Monad m => FormState m input a -> FormState m input a
+bracketState k = do
+  FormRange startF1 _ <- get
+  res <- k
+  FormRange _ endF2 <- get
+  put $ FormRange startF1 endF2
+  pure res
+
+instance (Functor m) => Functor (Form m input error view ()) where
+  fmap f form =
+    Form $ fmap (second (fmap (fmap (fmap f)))) (unForm form)
+
+instance (Functor m, Monoid view, Monad m) => Applicative (Form m input error view ()) where
+  pure a =
+    Form $ do
+      i <- getFormId
+      pure
+        ( View $ const $ mempty
+        , pure $ Ok $ Proved
+          { proofs = ()
+          , pos = FormRange i i
+          , unProved = a
+          }
+        )
+
+  -- this coud be defined in terms of <<*>> if we just changed the proof of frmF to (() -> ())
+  (Form frmF) <*> (Form frmA) =
+    Form $ do
+      ((view1, mfok), (view2, maok)) <-
+        bracketState $ do
+          res1 <- frmF
+          incFormId
+          res2 <- frmA
+          pure (res1, res2)
+      fok <- lift $ lift $ mfok
+      aok <- lift $ lift $ maok
+      case (fok, aok) of
+        (Error errs1, Error errs2) -> pure (view1 `mappend` view2, pure $ Error $ errs1 ++ errs2)
+        (Error errs1, _) -> pure (view1 `mappend` view2, pure $ Error $ errs1)
+        (_, Error errs2) -> pure (view1 `mappend` view2, pure $ Error $ errs2)
+        (Ok (Proved _ (FormRange x _) f), Ok (Proved _ (FormRange _ y) a)) ->
+          pure
+            ( view1 `mappend` view2
+            , pure $ Ok $ Proved
+              { proofs = ()
+              , pos = FormRange x y
+              , unProved = f a
+              }
+            )
+
+-- ** Ways to evaluate a Form
+
+-- | Run a form
+--
+runForm
+  :: (Monad m)
+  => Environment m input
+  -> Text
+  -> Form m input error view proof a
+  -> m (View error view, m (Result error (Proved proof a)))
+runForm env prefix' form =
+  evalStateT (runReaderT (unForm form) env) (unitRange (zeroId $ unpack prefix'))
+
+-- | Run a form
+--
+runForm'
+  :: (Monad m)
+  => Environment m input
+  -> Text
+  -> Form m input error view proof a
+  -> m (view, Maybe a)
+runForm' env prefix form =
+  do
+    (view', mresult) <- runForm env prefix form
+    result <- mresult
+    pure $ case result of
+      Error e -> (unView view' e, Nothing)
+      Ok x -> (unView view' [], Just (unProved x))
+
+-- | Just evaluate the form to a view. This usually maps to a GET request in the
+-- browser.
+--
+viewForm
+  :: (Monad m)
+  => Text -- ^ form prefix
+  -> Form m input error view proof a -- ^ form to view
+  -> m view
+viewForm prefix form =
+  do
+    (v, _) <- runForm NoEnvironment prefix form
+    pure (unView v [])
+
+-- | Evaluate a form
+--
+-- Returns:
+--
+-- [@Left view@] on failure. The @view@ will have already been applied to the errors.
+--
+-- [@Right a@] on success.
+--
+eitherForm
+  :: (Monad m)
+  => Environment m input -- ^ Input environment
+  -> Text -- ^ Identifier for the form
+  -> Form m input error view proof a -- ^ Form to run
+  -> m (Either view a) -- ^ Result
+eitherForm env id' form = do
+  (view', mresult) <- runForm env id' form
+  result <- mresult
+  pure $ case result of
+    Error e -> Left $ unView view' e
+    Ok x -> Right (unProved x)
+
+-- | create a 'Form' from some @view@.
+--
+-- This is typically used to turn markup like @\<br\>@ into a 'Form'.
+view
+  :: (Monad m)
+  => view -- ^ View to insert
+  -> Form m input error view () () -- ^ Resulting form
+view view' =
+  Form $ do
+    i <- getFormId
+    pure
+      ( View (const view')
+      , pure
+        ( Ok
+          ( Proved
+            { proofs = ()
+            , pos = FormRange i i
+            , unProved = ()
+            }
+          )
+        )
+      )
+
+-- | Append a unit form to the left. This is useful for adding labels or error
+-- fields.
+--
+-- The 'Forms' on the left and right hand side will share the same
+-- 'FormId'. This is useful for elements like @\<label
+-- for=\"someid\"\>@, which need to refer to the id of another
+-- element.
+(++>)
+  :: (Monad m, Monoid view)
+  => Form m input error view () ()
+  -> Form m input error view proof a
+  -> Form m input error view proof a
+f1 ++> f2 =
+  Form $ do
+    -- Evaluate the form that matters first, so we have a correct range set
+    (v2, r) <- unForm f2
+    (v1, _) <- unForm f1
+    pure (v1 `mappend` v2, r)
+
+infixl 6 ++>
+
+-- | Append a unit form to the right. See '++>'.
+--
+(<++)
+  :: (Monad m, Monoid view)
+  => Form m input error view proof a
+  -> Form m input error view () ()
+  -> Form m input error view proof a
+f1 <++ f2 =
+  Form $ do
+    -- Evaluate the form that matters first, so we have a correct range set
+    (v1, r) <- unForm f1
+    (v2, _) <- unForm f2
+    pure (v1 `mappend` v2, r)
+
+infixr 5 <++
+
+-- | Change the view of a form using a simple function
+--
+-- This is useful for wrapping a form inside of a \<fieldset\> or other markup element.
+mapView
+  :: (Monad m, Functor m)
+  => (view -> view') -- ^ Manipulator
+  -> Form m input error view proof a -- ^ Initial form
+  -> Form m input error view' proof a -- ^ Resulting form
+mapView f = Form . fmap (first $ fmap f) . unForm
+
+-- | Utility Function: turn a view and pure value into a successful 'FormState'
+mkOk
+  :: (Monad m)
+  => FormId
+  -> view
+  -> a
+  -> FormState m input (View error view, m (Result error (Proved () a)))
+mkOk i view' val =
+  pure
+    ( View $ const $ view'
+    , pure $
+      Ok
+        ( Proved
+          { proofs = ()
+          , pos = unitRange i
+          , unProved = val
+          }
+        )
+    )
diff --git a/src/Ditto/Generalized.hs b/src/Ditto/Generalized.hs
new file mode 100644
--- /dev/null
+++ b/src/Ditto/Generalized.hs
@@ -0,0 +1,473 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DoAndIfThenElse #-}
+
+-- This module provides helper functions for HTML input elements. These helper functions are not specific to any particular web framework or html library.
+
+module Ditto.Generalized where
+
+import Control.Applicative ((<$>))
+import Control.Monad (foldM)
+import Control.Monad.Trans (lift)
+import Data.Bifunctor
+import Numeric (readDec)
+import Ditto.Backend
+import Ditto.Core
+import Ditto.Result
+import qualified Data.IntSet as IS
+
+-- | used for constructing elements like @\<input type=\"text\"\>@, which pure a single input value.
+input
+  :: (Monad m, FormError err)
+  => (input -> Either err a)
+  -> (FormId -> a -> view)
+  -> a
+  -> Form m input err view () a
+input fromInput toView initialValue =
+  Form $ do
+    i <- getFormId
+    v <- getFormInput' i
+    case v of
+      Default ->
+        pure
+          ( View $ const $ toView i initialValue
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = initialValue
+                }
+              )
+          )
+      Found x -> case fromInput x of 
+        Right a -> pure
+          ( View $ const $ toView i a
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = a
+                }
+              )
+          )
+        Left err -> pure
+          ( View $ const $ toView i initialValue
+          , pure $ Error [(unitRange i, err)]
+          )
+      Missing -> pure
+        ( View $ const $ toView i initialValue
+        , pure $ Error [(unitRange i, commonFormError (InputMissing i))]
+        )
+
+-- | used for elements like @\<input type=\"submit\"\>@ which are not always present in the form submission data.
+inputMaybe
+  :: (Monad m, FormError err)
+  => (input -> Either err a)
+  -> (FormId -> a -> view)
+  -> a
+  -> Form m input err view () (Maybe a)
+inputMaybe fromInput toView initialValue =
+  Form $ do
+    i <- getFormId
+    v <- getFormInput' i
+    case v of
+      Default -> pure
+          ( View $ const $ toView i initialValue
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = Just initialValue
+                }
+              )
+          )
+      Found x -> case fromInput x of
+        Right a -> pure
+          ( View $ const $ toView i a
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = (Just a)
+                }
+              )
+          )
+        Left err -> pure
+          ( View $ const $ toView i initialValue
+          , pure $ Error [(unitRange i, err)]
+          )
+      Missing -> pure
+          ( View $ const $ toView i initialValue
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = Nothing
+                }
+              )
+          )
+
+-- | used for elements like @\<input type=\"reset\"\>@ which take a value, but are never present in the form data set.
+inputNoData
+  :: (Monad m)
+  => (FormId -> a -> view)
+  -> a
+  -> Form m input err view () ()
+inputNoData toView a =
+  Form $ do
+    i <- getFormId
+    pure
+      ( View $ const $ toView i a
+      , pure $
+        Ok
+          ( Proved
+            { proofs = ()
+            , pos = unitRange i
+            , unProved = ()
+            }
+          )
+      )
+
+-- | used for @\<input type=\"file\"\>@
+inputFile
+  :: forall m input err view. (Monad m, FormInput input, FormError err, ErrorInputType err ~ input)
+  => (FormId -> view)
+  -> Form m input err view () (FileType input)
+inputFile toView =
+  Form $ do
+    i <- getFormId
+    v <- getFormInput' i
+    case v of
+      Default ->
+        pure
+          ( View $ const $ toView i
+          , pure $ Error [(unitRange i, commonFormError (InputMissing i))]
+          )
+      Found x -> case getInputFile' x of
+        Right a -> pure
+          ( View $ const $ toView i
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = a
+                }
+              )
+          )
+        Left err -> pure
+          ( View $ const $ toView i
+          , pure $ Error [(unitRange i, err)]
+          )
+      Missing ->
+        pure
+          ( View $ const $ toView i
+          , pure $ Error [(unitRange i, commonFormError (InputMissing i))]
+          )
+  where
+    -- just here for the type-signature to make the type-checker happy
+    getInputFile' :: (FormError err, ErrorInputType err ~ input) => input -> Either err (FileType input)
+    getInputFile' = getInputFile
+
+-- | used for groups of checkboxes, @\<select multiple=\"multiple\"\>@ boxes
+inputMulti
+  :: forall m input err view a lbl. (Functor m, FormError err, ErrorInputType err ~ input, FormInput input, Monad m)
+  => [(a, lbl)] -- ^ value, label, initially checked
+  -> (FormId -> [(FormId, Int, lbl, Bool)] -> view) -- ^ function which generates the view
+  -> (a -> Bool) -- ^ isChecked/isSelected initially
+  -> Form m input err view () [a]
+inputMulti choices mkView isSelected =
+  Form $ do
+    i <- getFormId
+    inp <- getFormInput' i
+    case inp of
+      Default ->
+        do
+          let (choices', vals) =
+                foldr
+                  ( \(a, lbl) (cs, vs) ->
+                    if isSelected a
+                    then ((a, lbl, True) : cs, a : vs)
+                    else ((a, lbl, False) : cs, vs)
+                  )
+                  ([], [])
+                  choices
+          view' <- mkView i <$> augmentChoices choices'
+          mkOk i view' vals
+      Missing ->
+        -- just means that no checkboxes were checked
+        do
+          view' <- mkView i <$> augmentChoices (map (\(x, y) -> (x, y, False)) choices)
+          mkOk i view' []
+      Found v -> do
+        let readDec' str = case readDec str of
+              [(n, [])] -> n
+              _ -> (-1) -- FIXME: should probably pure an internal err?
+            keys = IS.fromList $ map readDec' $ getInputStrings v
+            (choices', vals) =
+              foldr
+                ( \(i0, (a, lbl)) (c, v0) ->
+                  if IS.member i0 keys
+                  then ((a, lbl, True) : c, a : v0)
+                  else ((a, lbl, False) : c, v0)
+                )
+                ([], []) $
+                zip [0..] choices
+        view' <- mkView i <$> augmentChoices choices'
+        mkOk i view' vals
+  where
+    augmentChoices :: (Monad m) => [(a, lbl, Bool)] -> FormState m input [(FormId, Int, lbl, Bool)]
+    augmentChoices choices' = mapM augmentChoice (zip [0..] choices')
+    augmentChoice :: (Monad m) => (Int, (a, lbl, Bool)) -> FormState m input (FormId, Int, lbl, Bool)
+    augmentChoice (vl, (_, lbl, checked)) =
+      do
+        incFormId
+        i <- getFormId
+        pure (i, vl, lbl, checked)
+
+-- | radio buttons, single @\<select\>@ boxes
+inputChoice
+  :: forall a m err input lbl view. (Functor m, FormError err, ErrorInputType err ~ input, FormInput input, Monad m)
+  => (a -> Bool) -- ^ is default
+  -> [(a, lbl)] -- ^ value, label
+  -> (FormId -> [(FormId, Int, lbl, Bool)] -> view) -- ^ function which generates the view
+  -> Form m input err view () a
+inputChoice isDefault choices mkView =
+  Form $ do
+    i <- getFormId
+    inp <- getFormInput' i
+    case inp of
+      Default ->
+        do
+          let (choices', def) = markSelected choices
+          view' <- mkView i <$> augmentChoices choices'
+          mkOk' i view' def
+      Missing ->
+        -- can happen if no choices where checked
+        do
+          let (choices', def) = markSelected choices
+          view' <- mkView i <$> augmentChoices choices'
+          mkOk' i view' def
+      Found v ->
+        do
+          let readDec' :: String -> Int
+              readDec' str' = case readDec str' of
+                [(n, [])] -> n
+                _ -> (-1) -- FIXME: should probably pure an internal err?
+              estr = getInputString v :: Either err String
+              key = second readDec' estr
+              (choices', mval) =
+                foldr
+                  ( \(i0, (a, lbl)) (c, v0) ->
+                    if either (const False) (==i0) key
+                    then ((a, lbl, True) : c, Just a)
+                    else ((a, lbl, False) : c, v0)
+                  )
+                  ([], Nothing) $
+                  zip [0..] choices
+          view' <- mkView i <$> augmentChoices choices'
+          case mval of
+            Nothing ->
+              pure
+                ( View $ const view'
+                , pure $ Error [(unitRange i, commonFormError (InputMissing i))]
+                )
+            (Just val) -> mkOk i view' val
+  where
+    mkOk' i view' (Just val) = mkOk i view' val
+    mkOk' i view' Nothing =
+      pure
+        ( View $ const $ view'
+        , pure $ Error [(unitRange i, commonFormError MissingDefaultValue)]
+        )
+    markSelected :: [(a, lbl)] -> ([(a, lbl, Bool)], Maybe a)
+    markSelected cs =
+      foldr
+        ( \(a, lbl) (vs, ma) ->
+          if isDefault a
+          then ((a, lbl, True) : vs, Just a)
+          else ((a, lbl, False) : vs, ma)
+        )
+        ([], Nothing)
+        cs
+    augmentChoices :: (Monad m) => [(a, lbl, Bool)] -> FormState m input [(FormId, Int, lbl, Bool)]
+    augmentChoices choices' = mapM augmentChoice (zip [0..] choices')
+    augmentChoice :: (Monad m) => (Int, (a, lbl, Bool)) -> FormState m input (FormId, Int, lbl, Bool)
+    augmentChoice (vl, (_a, lbl, selected)) =
+      do
+        incFormId
+        i <- getFormId
+        pure (i, vl, lbl, selected)
+
+-- | radio buttons, single @\<select\>@ boxes
+inputChoiceForms
+  :: forall a m err input lbl view proof. (Functor m, Monad m, FormError err, ErrorInputType err ~ input, FormInput input)
+  => a
+  -> [(Form m input err view proof a, lbl)] -- ^ value, label
+  -> (FormId -> [(FormId, Int, FormId, view, lbl, Bool)] -> view) -- ^ function which generates the view
+  -> Form m input err view proof a
+inputChoiceForms def choices mkView =
+  Form $ do
+    i <- getFormId -- id used for the 'name' attribute of the radio buttons
+    inp <- getFormInput' i
+    case inp of
+      Default ->
+        -- produce view for GET request
+        do
+          choices' <- mapM viewSubForm =<< augmentChoices (selectFirst choices)
+          let view' = mkView i choices'
+          mkOk' i view' def
+      Missing ->
+        -- shouldn't ever happen...
+        do
+          choices' <- mapM viewSubForm =<< augmentChoices (selectFirst choices)
+          let view' = mkView i choices'
+          mkOk' i view' def
+      (Found v) ->
+        do
+          let readDec' str' = case readDec str' of
+                [(n, [])] -> n
+                _ -> (-1) -- FIXME: should probably pure an internal err?
+              estr = getInputString v :: Either err String
+              key = second readDec' estr
+          choices' <- augmentChoices $ markSelected key (zip [0..] choices)
+          (choices'', mres) <-
+            foldM
+              ( \(views, res) (fid, val, iview, frm, lbl, selected) -> do
+                incFormId
+                if selected
+                then do
+                    (v0, mres) <- unForm frm
+                    res' <- lift $ lift mres
+                    case res' of
+                      Ok{} -> do
+                        pure (((fid, val, iview, unView v0 [], lbl, selected) : views), pure res')
+                      Error errs -> do
+                        pure (((fid, val, iview, unView v0 errs, lbl, selected) : views), pure res')
+                else do
+                    (v0, _) <- unForm frm
+                    pure ((fid, val, iview, unView v0 [], lbl, selected) : views, res)
+              )
+              ([], pure $ Error [(unitRange i, commonFormError (InputMissing i))])
+              (choices')
+          let view' = mkView i (reverse choices'')
+          pure (View (const view'), mres)
+  where
+    -- | Utility Function: turn a view and pure value into a successful 'FormState'
+    mkOk'
+      :: (Monad m)
+      => FormId
+      -> view
+      -> a
+      -> FormState m input (View err view, m (Result err (Proved proof a)))
+    mkOk' _ view' _ =
+      pure
+        ( View $ const view'
+        , pure $ Error []
+        )
+    selectFirst :: [(Form m input err view proof a, lbl)] -> [(Form m input err view proof a, lbl, Bool)]
+    selectFirst ((frm, lbl) : fs) = (frm, lbl, True) : map (\(frm', lbl') -> (frm', lbl', False)) fs
+    selectFirst [] = []
+    markSelected :: Either e Int -> [(Int, (Form m input err view proof a, lbl))] -> [(Form m input err view proof a, lbl, Bool)]
+    markSelected en choices' =
+      map (\(i, (f, lbl)) -> (f, lbl, either (const False) (==i) en)) choices'
+    viewSubForm :: (FormId, Int, FormId, Form m input err view proof a, lbl, Bool) -> FormState m input (FormId, Int, FormId, view, lbl, Bool)
+    viewSubForm (fid, vl, iview, frm, lbl, selected) =
+      do
+        incFormId
+        (v, _) <- unForm frm
+        pure (fid, vl, iview, unView v [], lbl, selected)
+    augmentChoices :: (Monad m) => [(Form m input err view proof a, lbl, Bool)] -> FormState m input [(FormId, Int, FormId, Form m input err view proof a, lbl, Bool)]
+    augmentChoices choices' = mapM augmentChoice (zip [0..] choices')
+    augmentChoice :: (Monad m) => (Int, (Form m input err view proof a, lbl, Bool)) -> FormState m input (FormId, Int, FormId, Form m input err view proof a, lbl, Bool)
+    augmentChoice (vl, (frm, lbl, selected)) =
+      do
+        incFormId
+        i <- getFormId
+        incFormId
+        iview <- getFormId
+        pure (i, vl, iview, frm, lbl, selected)
+
+{-
+              case inp of
+                (Found v) ->
+                    do let readDec' str = case readDec str of
+                                            [(n,[])] -> n
+                                            _ -> (-1) -- FIXME: should probably pure an internal err?
+                           (Right str) = getInputString v :: Either err String -- FIXME
+                           key = readDec' str
+                           (choices', mval) =
+                               foldr (\(i, (a, lbl)) (c, v) ->
+                                          if i == key
+                                          then ((a,lbl,True) : c, Just a)
+                                          else ((a,lbl,False): c,     v))
+                                     ([], Nothing) $
+                                     zip [0..] choices
+
+
+-}
+-- | used to create @\<label\>@ elements
+label
+  :: Monad m
+  => (FormId -> view)
+  -> Form m input err view () ()
+label f =
+  Form $ do
+    id' <- getFormId
+    pure
+      ( View (const $ f id')
+      , pure
+        ( Ok $ Proved
+          { proofs = ()
+          , pos = unitRange id'
+          , unProved = ()
+          }
+        )
+      )
+
+-- | used to add a list of err messages to a 'Form'
+--
+-- This function automatically takes care of extracting only the
+-- errors that are relevent to the form element it is attached to via
+-- '<++' or '++>'.
+errors
+  :: Monad m
+  => ([err] -> view) -- ^ function to convert the err messages into a view
+  -> Form m input err view () ()
+errors f =
+  Form $ do
+    range <- getFormRange
+    pure
+      ( View (f . retainErrors range)
+      , pure
+        ( Ok $ Proved
+          { proofs = ()
+          , pos = range
+          , unProved = ()
+          }
+        )
+      )
+
+-- | similar to 'errors' but includes err messages from children of the form as well.
+childErrors
+  :: Monad m
+  => ([err] -> view)
+  -> Form m input err view () ()
+childErrors f =
+  Form $ do
+    range <- getFormRange
+    pure
+      ( View (f . retainChildErrors range)
+      , pure
+        ( Ok $ Proved
+          { proofs = ()
+          , pos = range
+          , unProved = ()
+          }
+        )
+      )
diff --git a/src/Ditto/Generalized/Named.hs b/src/Ditto/Generalized/Named.hs
new file mode 100644
--- /dev/null
+++ b/src/Ditto/Generalized/Named.hs
@@ -0,0 +1,480 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DoAndIfThenElse #-}
+
+-- This module provides helper functions for HTML input elements. These helper functions are not specific to any particular web framework or html library.
+
+module Ditto.Generalized.Named where
+
+import Control.Applicative ((<$>))
+import Control.Monad (foldM)
+import Control.Monad.Trans (lift)
+import Data.Bifunctor
+import Numeric (readDec)
+import Ditto.Backend
+import Ditto.Core
+import Ditto.Result
+import qualified Data.IntSet as IS
+
+-- | used for constructing elements like @\<input type=\"text\"\>@, which pure a single input value.
+input
+  :: (Monad m, FormError err)
+  => (input -> Either err a)
+  -> (FormId -> a -> view)
+  -> a
+  -> String
+  -> Form m input err view () a
+input fromInput toView initialValue name =
+  Form $ do
+    let i = FormIdCustom name
+    v <- getFormInput' i
+    case v of
+      Default ->
+        pure
+          ( View $ const $ toView i initialValue
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = initialValue
+                }
+              )
+          )
+      Found x -> case fromInput x of 
+        Right a -> pure
+          ( View $ const $ toView i a
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = a
+                }
+              )
+          )
+        Left err -> pure
+          ( View $ const $ toView i initialValue
+          , pure $ Error [(unitRange i, err)]
+          )
+      Missing -> pure
+        ( View $ const $ toView i initialValue
+        , pure $ Error [(unitRange i, commonFormError (InputMissing i))]
+        )
+
+-- | used for elements like @\<input type=\"submit\"\>@ which are not always present in the form submission data.
+inputMaybe
+  :: (Monad m, FormError err)
+  => (input -> Either err a)
+  -> (FormId -> a -> view)
+  -> a
+  -> String
+  -> Form m input err view () (Maybe a)
+inputMaybe fromInput toView initialValue name =
+  Form $ do
+    let i = FormIdCustom name
+    v <- getFormInput' i
+    case v of
+      Default -> pure
+          ( View $ const $ toView i initialValue
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = Just initialValue
+                }
+              )
+          )
+      Found x -> case fromInput x of
+        Right a -> pure
+          ( View $ const $ toView i a
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = (Just a)
+                }
+              )
+          )
+        Left err -> pure
+          ( View $ const $ toView i initialValue
+          , pure $ Error [(unitRange i, err)]
+          )
+      Missing -> pure
+          ( View $ const $ toView i initialValue
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = Nothing
+                }
+              )
+          )
+
+-- | used for elements like @\<input type=\"reset\"\>@ which take a value, but are never present in the form data set.
+inputNoData
+  :: (Monad m)
+  => (FormId -> a -> view)
+  -> a
+  -> String
+  -> Form m input err view () ()
+inputNoData toView a name =
+  Form $ do
+    let i = FormIdCustom name
+    pure
+      ( View $ const $ toView i a
+      , pure $
+        Ok
+          ( Proved
+            { proofs = ()
+            , pos = unitRange i
+            , unProved = ()
+            }
+          )
+      )
+
+-- | used for @\<input type=\"file\"\>@
+inputFile
+  :: forall m input err view. (Monad m, FormInput input, FormError err, ErrorInputType err ~ input)
+  => (FormId -> view)
+  -> String
+  -> Form m input err view () (FileType input)
+inputFile toView name =
+  Form $ do
+    let i = FormIdCustom name
+    v <- getFormInput' i
+    case v of
+      Default ->
+        pure
+          ( View $ const $ toView i
+          , pure $ Error [(unitRange i, commonFormError (InputMissing i))]
+          )
+      Found x -> case getInputFile' x of
+        Right a -> pure
+          ( View $ const $ toView i
+          , pure $
+            Ok
+              ( Proved
+                { proofs = ()
+                , pos = unitRange i
+                , unProved = a
+                }
+              )
+          )
+        Left err -> pure
+          ( View $ const $ toView i
+          , pure $ Error [(unitRange i, err)]
+          )
+      Missing ->
+        pure
+          ( View $ const $ toView i
+          , pure $ Error [(unitRange i, commonFormError (InputMissing i))]
+          )
+  where
+    -- just here for the type-signature to make the type-checker happy
+    getInputFile' :: (FormError err, ErrorInputType err ~ input) => input -> Either err (FileType input)
+    getInputFile' = getInputFile
+
+-- | used for groups of checkboxes, @\<select multiple=\"multiple\"\>@ boxes
+inputMulti
+  :: forall m input err view a lbl. (Functor m, FormError err, ErrorInputType err ~ input, FormInput input, Monad m)
+  => [(a, lbl)] -- ^ value, label, initially checked
+  -> (FormId -> [(FormId, Int, lbl, Bool)] -> view) -- ^ function which generates the view
+  -> (a -> Bool) -- ^ isChecked/isSelected initially
+  -> String
+  -> Form m input err view () [a]
+inputMulti choices mkView isSelected name =
+  Form $ do
+    let i = FormIdCustom name
+    inp <- getFormInput' i
+    case inp of
+      Default ->
+        do
+          let (choices', vals) =
+                foldr
+                  ( \(a, lbl) (cs, vs) ->
+                    if isSelected a
+                    then ((a, lbl, True) : cs, a : vs)
+                    else ((a, lbl, False) : cs, vs)
+                  )
+                  ([], [])
+                  choices
+          view' <- mkView i <$> augmentChoices choices'
+          mkOk i view' vals
+      Missing ->
+        -- just means that no checkboxes were checked
+        do
+          view' <- mkView i <$> augmentChoices (map (\(x, y) -> (x, y, False)) choices)
+          mkOk i view' []
+      Found v -> do
+        let readDec' str = case readDec str of
+              [(n, [])] -> n
+              _ -> (-1) -- FIXME: should probably pure an internal err?
+            keys = IS.fromList $ map readDec' $ getInputStrings v
+            (choices', vals) =
+              foldr
+                ( \(i0, (a, lbl)) (c, v0) ->
+                  if IS.member i0 keys
+                  then ((a, lbl, True) : c, a : v0)
+                  else ((a, lbl, False) : c, v0)
+                )
+                ([], []) $
+                zip [0..] choices
+        view' <- mkView i <$> augmentChoices choices'
+        mkOk i view' vals
+  where
+    augmentChoices :: (Monad m) => [(a, lbl, Bool)] -> FormState m input [(FormId, Int, lbl, Bool)]
+    augmentChoices choices' = mapM augmentChoice (zip [0..] choices')
+    augmentChoice :: (Monad m) => (Int, (a, lbl, Bool)) -> FormState m input (FormId, Int, lbl, Bool)
+    augmentChoice (vl, (_, lbl, checked)) =
+      do
+        incFormId
+        let i = FormIdCustom name
+        pure (i, vl, lbl, checked)
+
+-- | radio buttons, single @\<select\>@ boxes
+inputChoice
+  :: forall a m err input lbl view. (Functor m, FormError err, ErrorInputType err ~ input, FormInput input, Monad m)
+  => (a -> Bool) -- ^ is default
+  -> [(a, lbl)] -- ^ value, label
+  -> (FormId -> [(FormId, Int, lbl, Bool)] -> view) -- ^ function which generates the view
+  -> String
+  -> Form m input err view () a
+inputChoice isDefault choices mkView name =
+  Form $ do
+    let i = FormIdCustom name
+    inp <- getFormInput' i
+    case inp of
+      Default ->
+        do
+          let (choices', def) = markSelected choices
+          view' <- mkView i <$> augmentChoices choices'
+          mkOk' i view' def
+      Missing ->
+        -- can happen if no choices where checked
+        do
+          let (choices', def) = markSelected choices
+          view' <- mkView i <$> augmentChoices choices'
+          mkOk' i view' def
+      Found v ->
+        do
+          let readDec' :: String -> Int
+              readDec' str' = case readDec str' of
+                [(n, [])] -> n
+                _ -> (-1) -- FIXME: should probably pure an internal err?
+              estr = getInputString v :: Either err String
+              key = second readDec' estr
+              (choices', mval) =
+                foldr
+                  ( \(i0, (a, lbl)) (c, v0) ->
+                    if either (const False) (==i0) key
+                    then ((a, lbl, True) : c, Just a)
+                    else ((a, lbl, False) : c, v0)
+                  )
+                  ([], Nothing) $
+                  zip [0..] choices
+          view' <- mkView i <$> augmentChoices choices'
+          case mval of
+            Nothing ->
+              pure
+                ( View $ const view'
+                , pure $ Error [(unitRange i, commonFormError (InputMissing i))]
+                )
+            (Just val) -> mkOk i view' val
+  where
+    mkOk' i view' (Just val) = mkOk i view' val
+    mkOk' i view' Nothing =
+      pure
+        ( View $ const $ view'
+        , pure $ Error [(unitRange i, commonFormError MissingDefaultValue)]
+        )
+    markSelected :: [(a, lbl)] -> ([(a, lbl, Bool)], Maybe a)
+    markSelected cs =
+      foldr
+        ( \(a, lbl) (vs, ma) ->
+          if isDefault a
+          then ((a, lbl, True) : vs, Just a)
+          else ((a, lbl, False) : vs, ma)
+        )
+        ([], Nothing)
+        cs
+    augmentChoices :: (Monad m) => [(a, lbl, Bool)] -> FormState m input [(FormId, Int, lbl, Bool)]
+    augmentChoices choices' = mapM augmentChoice (zip [0..] choices')
+    augmentChoice :: (Monad m) => (Int, (a, lbl, Bool)) -> FormState m input (FormId, Int, lbl, Bool)
+    augmentChoice (vl, (_a, lbl, selected)) =
+      do
+        incFormId
+        let i = FormIdCustom name
+        pure (i, vl, lbl, selected)
+
+-- | radio buttons, single @\<select\>@ boxes
+inputChoiceForms
+  :: forall a m err input lbl view proof. (Functor m, Monad m, FormError err, ErrorInputType err ~ input, FormInput input)
+  => a
+  -> [(Form m input err view proof a, lbl)] -- ^ value, label
+  -> (FormId -> [(FormId, Int, FormId, view, lbl, Bool)] -> view) -- ^ function which generates the view
+  -> String
+  -> Form m input err view proof a
+inputChoiceForms def choices mkView name =
+  Form $ do
+    let i = FormIdCustom name -- id used for the 'name' attribute of the radio buttons
+    inp <- getFormInput' i
+    case inp of
+      Default ->
+        -- produce view for GET request
+        do
+          choices' <- mapM viewSubForm =<< augmentChoices (selectFirst choices)
+          let view' = mkView i choices'
+          mkOk' i view' def
+      Missing ->
+        -- shouldn't ever happen...
+        do
+          choices' <- mapM viewSubForm =<< augmentChoices (selectFirst choices)
+          let view' = mkView i choices'
+          mkOk' i view' def
+      (Found v) ->
+        do
+          let readDec' str' = case readDec str' of
+                [(n, [])] -> n
+                _ -> (-1) -- FIXME: should probably pure an internal err?
+              estr = getInputString v :: Either err String
+              key = second readDec' estr
+          choices' <- augmentChoices $ markSelected key (zip [0..] choices)
+          (choices'', mres) <-
+            foldM
+              ( \(views, res) (fid, val, iview, frm, lbl, selected) -> do
+                incFormId
+                if selected
+                then do
+                    (v0, mres) <- unForm frm
+                    res' <- lift $ lift mres
+                    case res' of
+                      Ok{} -> do
+                        pure (((fid, val, iview, unView v0 [], lbl, selected) : views), pure res')
+                      Error errs -> do
+                        pure (((fid, val, iview, unView v0 errs, lbl, selected) : views), pure res')
+                else do
+                    (v0, _) <- unForm frm
+                    pure ((fid, val, iview, unView v0 [], lbl, selected) : views, res)
+              )
+              ([], pure $ Error [(unitRange i, commonFormError (InputMissing i))])
+              (choices')
+          let view' = mkView i (reverse choices'')
+          pure (View (const view'), mres)
+  where
+    -- | Utility Function: turn a view and pure value into a successful 'FormState'
+    mkOk'
+      :: (Monad m)
+      => FormId
+      -> view
+      -> a
+      -> FormState m input (View err view, m (Result err (Proved proof a)))
+    mkOk' _ view' _ =
+      pure
+        ( View $ const view'
+        , pure $ Error []
+        )
+    selectFirst :: [(Form m input err view proof a, lbl)] -> [(Form m input err view proof a, lbl, Bool)]
+    selectFirst ((frm, lbl) : fs) = (frm, lbl, True) : map (\(frm', lbl') -> (frm', lbl', False)) fs
+    selectFirst [] = []
+    markSelected :: Either e Int -> [(Int, (Form m input err view proof a, lbl))] -> [(Form m input err view proof a, lbl, Bool)]
+    markSelected en choices' =
+      map (\(i, (f, lbl)) -> (f, lbl, either (const False) (==i) en)) choices'
+    viewSubForm :: (FormId, Int, FormId, Form m input err view proof a, lbl, Bool) -> FormState m input (FormId, Int, FormId, view, lbl, Bool)
+    viewSubForm (fid, vl, iview, frm, lbl, selected) =
+      do
+        incFormId
+        (v, _) <- unForm frm
+        pure (fid, vl, iview, unView v [], lbl, selected)
+    augmentChoices :: (Monad m) => [(Form m input err view proof a, lbl, Bool)] -> FormState m input [(FormId, Int, FormId, Form m input err view proof a, lbl, Bool)]
+    augmentChoices choices' = mapM augmentChoice (zip [0..] choices')
+    augmentChoice :: (Monad m) => (Int, (Form m input err view proof a, lbl, Bool)) -> FormState m input (FormId, Int, FormId, Form m input err view proof a, lbl, Bool)
+    augmentChoice (vl, (frm, lbl, selected)) =
+      do
+        incFormId
+        let i = FormIdCustom name
+        incFormId
+        iview <- getFormId
+        pure (i, vl, iview, frm, lbl, selected)
+
+{-
+              case inp of
+                (Found v) ->
+                    do let readDec' str = case readDec str of
+                                            [(n,[])] -> n
+                                            _ -> (-1) -- FIXME: should probably pure an internal err?
+                           (Right str) = getInputString v :: Either err String -- FIXME
+                           key = readDec' str
+                           (choices', mval) =
+                               foldr (\(i, (a, lbl)) (c, v) ->
+                                          if i == key
+                                          then ((a,lbl,True) : c, Just a)
+                                          else ((a,lbl,False): c,     v))
+                                     ([], Nothing) $
+                                     zip [0..] choices
+
+
+-}
+-- | used to create @\<label\>@ elements
+label
+  :: Monad m
+  => (FormId -> view)
+  -> Form m input err view () ()
+label f =
+  Form $ do
+    id' <- getFormId
+    pure
+      ( View (const $ f id')
+      , pure
+        ( Ok $ Proved
+          { proofs = ()
+          , pos = unitRange id'
+          , unProved = ()
+          }
+        )
+      )
+
+-- | used to add a list of err messages to a 'Form'
+--
+-- This function automatically takes care of extracting only the
+-- errors that are relevent to the form element it is attached to via
+-- '<++' or '++>'.
+errors
+  :: Monad m
+  => ([err] -> view) -- ^ function to convert the err messages into a view
+  -> Form m input err view () ()
+errors f =
+  Form $ do
+    range <- getFormRange
+    pure
+      ( View (f . retainErrors range)
+      , pure
+        ( Ok $ Proved
+          { proofs = ()
+          , pos = range
+          , unProved = ()
+          }
+        )
+      )
+
+-- | similar to 'errors' but includes err messages from children of the form as well.
+childErrors
+  :: Monad m
+  => ([err] -> view)
+  -> Form m input err view () ()
+childErrors f =
+  Form $ do
+    range <- getFormRange
+    pure
+      ( View (f . retainChildErrors range)
+      , pure
+        ( Ok $ Proved
+          { proofs = ()
+          , pos = range
+          , unProved = ()
+          }
+        )
+      )
diff --git a/src/Ditto/Proof.hs b/src/Ditto/Proof.hs
new file mode 100644
--- /dev/null
+++ b/src/Ditto/Proof.hs
@@ -0,0 +1,152 @@
+{- |
+This module defines the 'Proof' type, some proofs, and some helper functions.
+
+A 'Proof' does three things:
+
+ - verifies that the input value meets some criteria
+ - optionally transforms the input value to another value while preserving that criteria
+ - puts the proof name in type-signature where the type-checker can use it
+-}
+module Ditto.Proof where
+
+import Control.Monad.Trans (lift)
+import Data.Bifunctor (Bifunctor (bimap))
+import Numeric (readDec, readFloat, readSigned)
+import Ditto.Core (Form (..), Proved (..))
+import Ditto.Result (Result (..))
+
+-- | A 'Proof' attempts to prove something about a value.
+--
+-- If successful, it can also transform the value to a new value. The
+-- proof should hold for the new value as well.
+--
+-- Generally, each 'Proof' has a unique data-type associated with it
+-- which names the proof, such as:
+--
+-- > data NotNull = NotNull
+--
+data Proof m error proof a b
+  = Proof
+      { proofName :: proof -- ^ name of the thing to prove
+      , proofFunction :: a -> m (Either error b) -- ^ function which provides the proof
+      }
+
+-- | apply a 'Proof' to a 'Form'
+prove
+  :: (Monad m)
+  => Form m input error view q a
+  -> Proof m error proof a b
+  -> Form m input error view proof b
+prove (Form frm) (Proof p f) =
+  Form $ do
+    (xml, mval) <- frm
+    val <- lift $ lift $ mval
+    case val of
+      (Error errs) -> pure (xml, pure $ Error errs)
+      (Ok (Proved _ posi a)) ->
+        do
+          r <- lift $ lift $ f a
+          case r of
+            (Left err) -> pure (xml, pure $ Error [(posi, err)])
+            (Right b) ->
+              pure
+                ( xml
+                , pure $
+                  Ok
+                    ( Proved
+                      { proofs = p
+                      , pos = posi
+                      , unProved = b
+                      }
+                    )
+                )
+
+-- * transformations (proofs minus the proof).
+
+-- | transform a 'Form' using a 'Proof', and the replace the proof with @()@.
+--
+-- This is useful when you want just want classic digestive-functors behaviour.
+transform
+  :: (Monad m)
+  => Form m input error view anyProof a
+  -> Proof m error proof a b
+  -> Form m input error view () b
+transform frm proof = bimap (const ()) id (frm `prove` proof)
+
+-- | transform the 'Form' result using a monadic 'Either' function.
+transformEitherM
+  :: (Monad m)
+  => Form m input error view anyProof a
+  -> (a -> m (Either error b))
+  -> Form m input error view () b
+transformEitherM frm func = frm `transform` (Proof () func)
+
+-- | transform the 'Form' result using an 'Either' function.
+transformEither
+  :: (Monad m)
+  => Form m input error view anyProof a
+  -> (a -> Either error b)
+  -> Form m input error view () b
+transformEither frm func = transformEitherM frm (pure . func)
+
+-- * Various Proofs
+
+-- | proof that a list is not empty
+data NotNull = NotNull
+
+-- | prove that a list is not empty
+notNullProof :: (Monad m) => error -> Proof m error NotNull [a] [a]
+notNullProof errorMsg = Proof NotNull (pure . check)
+  where
+    check list =
+      if null list
+      then (Left errorMsg)
+      else (Right list)
+
+-- | proof that a 'String' is a decimal number
+data Decimal = Decimal
+
+-- | proof that a 'String' is a Real/Fractional number
+data RealFractional = RealFractional
+
+-- | proof that a number is also (allowed to be) signed
+data Signed a = Signed a
+
+-- | read an unsigned number in decimal notation
+decimal
+  :: (Monad m, Eq i, Num i)
+  => (String -> error) -- ^ create an error message ('String' is the value that did not parse)
+  -> Proof m error Decimal String i
+decimal mkError = Proof Decimal (pure . toDecimal)
+  where
+    toDecimal str =
+      case readDec str of
+        [(d, [])] -> (Right d)
+        _ -> (Left $ mkError str)
+
+-- | read signed decimal number
+signedDecimal :: (Monad m, Eq i, Real i) => (String -> error) -> Proof m error (Signed Decimal) String i
+signedDecimal mkError = Proof (Signed Decimal) (pure . toDecimal)
+  where
+    toDecimal str =
+      case (readSigned readDec) str of
+        [(d, [])] -> (Right d)
+        _ -> (Left $ mkError str)
+
+-- | read 'RealFrac' number
+realFrac :: (Monad m, RealFrac a) => (String -> error) -> Proof m error RealFractional String a
+realFrac mkError = Proof RealFractional (pure . toRealFrac)
+  where
+    toRealFrac str =
+      case readFloat str of
+        [(f, [])] -> (Right f)
+        _ -> (Left $ mkError str)
+
+-- | read a signed 'RealFrac' number
+realFracSigned :: (Monad m, RealFrac a) => (String -> error) -> Proof m error (Signed RealFractional) String a
+realFracSigned mkError = Proof (Signed RealFractional) (pure . toRealFrac)
+  where
+    toRealFrac str =
+      case (readSigned readFloat) str of
+        [(f, [])] -> (Right f)
+        _ -> (Left $ mkError str)
diff --git a/src/Ditto/Result.hs b/src/Ditto/Result.hs
new file mode 100644
--- /dev/null
+++ b/src/Ditto/Result.hs
@@ -0,0 +1,136 @@
+-- | Module for the core result type, and related functions
+--
+module Ditto.Result
+  ( Result (..)
+  , getResult
+  , FormId (..)
+  , zeroId
+  , mapId
+  , FormRange (..)
+  , incrementFormId
+  , unitRange
+  , isInRange
+  , isSubRange
+  , retainErrors
+  , retainChildErrors
+  )
+where
+
+import Data.List (intercalate)
+import Control.Applicative (Applicative (..))
+import Data.List.NonEmpty (NonEmpty(..))
+import qualified Data.List.NonEmpty as NE
+-- import Data.List (intercalate)
+
+-- | Type for failing computations
+--
+data Result e ok
+  = Error [(FormRange, e)]
+  | Ok ok
+  deriving (Show, Eq)
+
+instance Functor (Result e) where
+
+  fmap _ (Error x) = Error x
+  fmap f (Ok x) = Ok (f x)
+
+instance Monad (Result e) where
+
+  return = Ok
+
+  Error x >>= _ = Error x
+  Ok x >>= f = f x
+
+instance Applicative (Result e) where
+
+  pure = Ok
+
+  Error x <*> Error y = Error $ x ++ y
+  Error x <*> Ok _ = Error x
+  Ok _ <*> Error y = Error y
+  Ok x <*> Ok y = Ok $ x y
+
+-- | convert a 'Result' to 'Maybe' discarding the error message on 'Error'
+getResult :: Result e ok -> Maybe ok
+getResult (Error _) = Nothing
+getResult (Ok r) = Just r
+
+-- | An ID used to identify forms
+--
+data FormId
+  = FormId
+      { -- | Global prefix for the form
+        formPrefix :: String
+      , -- | Stack indicating field. Head is most specific to this item
+        formIdList :: NonEmpty Integer
+      }
+  | FormIdCustom String
+  deriving (Eq, Ord)
+
+-- | The zero ID, i.e. the first ID that is usable
+--
+zeroId :: String -> FormId
+zeroId p = FormId
+  { formPrefix = p
+  , formIdList = pure 0
+  }
+
+-- | map a function over the @NonEmpty Integer@ inside a 'FormId'
+mapId :: (NonEmpty Integer -> NonEmpty Integer) -> FormId -> FormId
+mapId f (FormId p is) = FormId p $ f is
+mapId _ x = x
+
+instance Show FormId where
+  show (FormId p xs) =
+    p ++ "-fval[" ++ (intercalate "." $ reverse $ map show $ NE.toList xs) ++ "]"
+  show (FormIdCustom x) = x
+
+-- | get the head 'Integer' from a 'FormId'
+formId :: FormId -> Integer
+formId = NE.head . formIdList
+
+-- | A range of ID's to specify a group of forms
+--
+data FormRange
+  = FormRange FormId FormId
+  deriving (Eq, Show)
+
+-- | Increment a form ID
+--
+incrementFormId :: FormId -> FormId
+incrementFormId (FormId p (x :| xs)) = FormId p $ (x + 1) :| xs
+incrementFormId x@FormIdCustom{} = x
+
+-- | create a 'FormRange' from a 'FormId'
+unitRange :: FormId -> FormRange
+unitRange i = FormRange i $ incrementFormId i
+
+-- | Check if a 'FormId' is contained in a 'FormRange'
+--
+isInRange
+  :: FormId -- ^ Id to check for
+  -> FormRange -- ^ Range
+  -> Bool -- ^ If the range contains the id
+isInRange a (FormRange b c) = formId a >= formId b && formId a < formId c
+
+-- | Check if a 'FormRange' is contained in another 'FormRange'
+--
+isSubRange
+  :: FormRange -- ^ Sub-range
+  -> FormRange -- ^ Larger range
+  -> Bool -- ^ If the sub-range is contained in the larger range
+isSubRange (FormRange a b) (FormRange c d) =
+  formId a >= formId c &&
+    formId b <=
+    formId d
+
+-- | Select the errors for a certain range
+--
+retainErrors :: FormRange -> [(FormRange, e)] -> [e]
+retainErrors range = map snd . filter ((== range) . fst)
+
+-- | Select the errors originating from this form or from any of the children of
+-- this form
+--
+retainChildErrors :: FormRange -> [(FormRange, e)] -> [e]
+retainChildErrors range = map snd . filter ((`isSubRange` range) . fst)