Merge pull request #554 from Sventimir/validation

Input validation

libs/base/Data/Nat.idr

@@ -58,6 +58,11 @@ data NotBothZero : (n, m : Nat) -> Type where
   LeftIsNotZero  : NotBothZero (S n) m
   RightIsNotZero : NotBothZero n     (S m)
 
+export
+Uninhabited (NotBothZero 0 0) where
+  uninhabited LeftIsNotZero impossible
+  uninhabited RightIsNotZero impossible
+
 public export
 data LTE  : (n, m : Nat) -> Type where
   LTEZero : LTE Z    right

libs/contrib/Control/Arrow.idr

@@ -0,0 +1,124 @@
+module Control.Arrow
+
+import Control.Category
+import Data.Either
+import Data.Morphisms
+
+
+infixr 5 <++>
+infixr 3 ***
+infixr 3 &&&
+infixr 2 +++
+infixr 2 \|/
+
+public export
+interface Category arr => Arrow (0 arr : Type -> Type -> Type) where
+  arrow  : (a -> b) -> arr a b
+  first  : arr a b -> arr (a, c) (b, c)
+
+  second : arr a b -> arr (c, a) (c, b)
+  second f = arrow {arr = arr} swap >>> first f >>> arrow {arr = arr} swap
+    where
+    swap : (x, y) -> (y, x)
+    swap (a, b) = (b, a)
+
+  (***)  : arr a b -> arr a' b' -> arr (a, a') (b, b')
+  f *** g = first f >>> second g
+
+  (&&&)  : arr a b -> arr a b' -> arr a (b, b')
+  f &&& g = arrow dup >>> f *** g
+    where
+    dup : x -> (x,x)
+    dup x = (x,x)
+
+public export
+implementation Arrow Morphism where
+  arrow  f            = Mor f
+  first  (Mor f)      = Mor $ \(a, b) => (f a, b)
+  second (Mor f)      = Mor $ \(a, b) => (a, f b)
+  (Mor f) *** (Mor g) = Mor $ \(a, b) => (f a, g b)
+  (Mor f) &&& (Mor g) = Mor $ \a => (f a, g a)
+
+public export
+implementation Monad m => Arrow (Kleislimorphism m) where
+  arrow f = Kleisli (pure . f)
+  first (Kleisli f) =  Kleisli $ \(a, b) => do x <- f a
+                                               pure (x, b)
+
+  second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b
+                                               pure (a, x)
+
+  (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
+                                                        y <- g b
+                                                        pure (x, y)
+
+  (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
+                                                   y <- g a
+                                                   pure (x, y)
+
+public export
+interface Arrow arr => ArrowZero (0 arr : Type -> Type -> Type) where
+  zeroArrow : arr a b
+
+public export
+interface ArrowZero arr => ArrowPlus (0 arr : Type -> Type -> Type) where
+  (<++>) : arr a b -> arr a b -> arr a b
+
+public export
+interface Arrow arr => ArrowChoice (0 arr : Type -> Type -> Type) where
+  left  : arr a b -> arr (Either a c) (Either b c)
+
+  right : arr a b -> arr (Either c a) (Either c b)
+  right f = arrow mirror >>> left f >>> arrow mirror
+
+
+  (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
+  f +++ g = left f >>> right g
+
+  (\|/) : arr a b -> arr c b -> arr (Either a c) b
+  f \|/ g = f +++ g >>> arrow fromEither
+    where
+    fromEither : Either b b -> b
+    fromEither (Left b) = b
+    fromEither (Right b) = b
+
+public export
+implementation Monad m => ArrowChoice (Kleislimorphism m) where
+  left f                      = f          +++ (arrow id)
+  right f                     = (arrow id) +++ f
+  f           +++ g           = (f >>> (arrow Left)) \|/ (g >>> (arrow Right))
+  (Kleisli f) \|/ (Kleisli g) = Kleisli (either f g)
+
+public export
+interface Arrow arr => ArrowApply (0 arr : Type -> Type -> Type) where
+  app : arr (arr a b, a) b
+
+public export
+implementation Monad m => ArrowApply (Kleislimorphism m) where
+  app = Kleisli $ \(Kleisli f, x) => f x
+
+public export
+data ArrowMonad : (Type -> Type -> Type) -> Type -> Type where
+  MkArrowMonad : (runArrowMonad : arr (the Type ()) a) -> ArrowMonad arr a
+
+public export
+runArrowMonad : ArrowMonad arr a -> arr (the Type ()) a
+runArrowMonad (MkArrowMonad a) = a
+
+public export
+implementation Arrow a => Functor (ArrowMonad a) where
+  map f (MkArrowMonad m) = MkArrowMonad $ m >>> arrow f
+
+public export
+implementation Arrow a => Applicative (ArrowMonad a) where
+  pure x = MkArrowMonad $ arrow $ \_ => x
+  (MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
+
+public export
+implementation ArrowApply a => Monad (ArrowMonad a) where
+  (MkArrowMonad m) >>= f =
+    MkArrowMonad $ m >>> (arrow $ \x => (runArrowMonad (f x), ())) >>> app
+
+public export
+interface Arrow arr => ArrowLoop (0 arr : Type -> Type -> Type) where
+  loop : arr (Pair a c) (Pair b c) -> arr a b

libs/contrib/Control/Category.idr

@@ -0,0 +1,27 @@
+module Control.Category
+
+import Data.Morphisms
+
+
+public export
+interface Category (0 cat : Type -> Type -> Type) where
+  id  : cat a a
+  (.) : cat b c -> cat a b -> cat a c
+
+public export
+Category Morphism where
+  id                = Mor id
+  -- disambiguation needed below, because unification can now get further
+  -- here with Category.(.) and it's only interface resolution that fails!
+  (Mor f) . (Mor g) = Mor $ Basics.(.) f g
+
+public export
+Monad m => Category (Kleislimorphism m) where
+  id                        = Kleisli (pure . id)
+  (Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f
+
+infixr 1 >>>
+
+public export
+(>>>) : Category cat => cat a b -> cat b c -> cat a c
+f >>> g = g . f

libs/contrib/Control/Monad/Trans/Either.idr

@@ -0,0 +1,55 @@
+module Control.Monad.Trans.Either
+
+%default total
+
+
+public export
+record EitherT m a b where
+    constructor MkEitherT
+    runEitherT : m (Either a b)
+
+export
+Functor m => Functor (EitherT m a) where
+    map f (MkEitherT runEitherT) = MkEitherT (map (map f) runEitherT)
+
+export
+Monad m => Applicative (EitherT m a) where
+    pure = MkEitherT . pure . Right
+    (MkEitherT left) <*> (MkEitherT right) = MkEitherT $ do
+        l <- left
+        r <- right
+        pure (l <*> r)
+
+export
+Monad m => Monad (EitherT m a) where
+    join (MkEitherT runEitherT) = MkEitherT $ do
+        case !runEitherT of
+            Left l => pure (Left l)
+            Right (MkEitherT inner) => inner
+
+
+export
+eitherT : Monad m => (a -> m c) -> (b -> m c) -> EitherT m a b -> m c
+eitherT f g (MkEitherT runEitherT) = case !runEitherT of
+    Left l => f l
+    Right r => g r
+
+export
+bimapEitherT : Functor m => (a -> c) -> (b -> d) -> EitherT m a b -> EitherT m c d
+bimapEitherT f g (MkEitherT runEitherT) = MkEitherT (map m runEitherT)
+    where
+    m : Either a b -> Either c d
+    m (Left l) = Left (f l)
+    m (Right r) = Right (g r)
+
+export
+mapEitherT : (m (Either a b) -> n (Either c d)) -> EitherT m a b -> EitherT n c d
+mapEitherT f (MkEitherT runEitherT) = MkEitherT $ f runEitherT
+
+export
+hoist : Applicative m => Either a b -> EitherT m a b
+hoist e = MkEitherT $ pure e
+
+export
+fail : Applicative m => a -> EitherT m a b
+fail = MkEitherT . pure . Left

libs/contrib/Control/Validation.idr

@@ -0,0 +1,209 @@
+module Control.Validation
+
+-- Main purpose of this module is verifying programmer's assumptions about
+-- user input. On one hand we want to write precisely typed programs, including
+-- assumptions about input expressed in types and prove correctness of these
+-- programs. On the other we get an unstructured user input as a string or even
+-- a raw sequence of bytes.
+
+-- This module intends to provide a framework for verifying our assumptions
+-- about user input and constructing proofs that input is indeed valid or
+-- failing early with a nice error message if it isn't.
+
+import Control.Monad.Identity
+import Control.Monad.Syntax
+import Control.Monad.Trans.Either
+import Data.Nat
+import Data.Strings
+import Data.Vect
+import Decidable.Equality
+
+%default total
+
+
+public export
+Result : (Type -> Type) -> Type -> Type
+Result m = EitherT m String
+
+||| Validators in this module come in two flavours: Structural Validators and
+||| Property Validators. They are both wrappers around functions which take
+||| some input and confirm that it's valid (returning some witness of its
+||| validity) or fail with an error described by a string.
+export
+data ValidatorT : (Type -> Type) -> Type -> Type -> Type where
+    MkValidator : (a -> Result m b) -> ValidatorT m a b
+
+||| A type of validator trying to prove properties of values. It's type is
+||| significantly different than that of an ordinary validator and cannot be
+||| made an instance of Monad interface, because it's last parameter is
+||| (t -> Type) instead of just Type. Therefore it must be explicitly turned
+||| into an ordinary validator using the prop function below.
+data PropValidator : (Type -> Type) -> (t : Type) -> (t -> Type) -> Type where
+    MkPropValidator : ((x : t) -> Result m (p x)) -> PropValidator m t p
+
+public export
+Validator : Type -> Type -> Type
+Validator = ValidatorT Identity
+
+
+||| Run validation on given input, returning (Right refinedInput) if everything
+||| is all right or (Left errorMessage) if it's not.
+export
+validateT : ValidatorT m a b -> a -> Result m b
+validateT (MkValidator v) = v
+
+||| Run validation within the Identity monad and unwrap result immediately.
+export
+validate : Validator a b -> a -> Either String b
+validate v = runIdentity . runEitherT . validateT v
+
+||| Given a function from input to Either String output, make a validator.
+export
+validator : (a -> Result m b) -> ValidatorT m a b
+validator = MkValidator
+
+export
+Functor m => Functor (ValidatorT m a) where
+    map f v = MkValidator (map f . validateT v)
+
+export
+Monad m => Applicative (ValidatorT m a) where
+    pure a = MkValidator (const $ pure a)
+    f <*> a = MkValidator (\x => validateT f x <*> validateT a x)
+
+export
+Monad m => Monad (ValidatorT m a) where
+    v >>= f = MkValidator $ \x => do
+        r <- validateT v x
+        validateT (f r) x
+
+||| Plug a property validator into the chain of other validators. The value
+||| under validation will be ignored and the value whose property is going to
+||| be checked must be supplied manually. Otherwise Idris won;t be able to
+||| unify.
+prop : PropValidator m t p -> (x : t) -> ValidatorT m a (p x)
+prop (MkPropValidator v) x = MkValidator (const $ v x)
+
+replaceError : Monad m => String -> Result m a -> Result m a
+replaceError e = bimapEitherT (const e) id
+
+||| Replace validator's default error message.
+export
+withError : Monad m => String -> ValidatorT m a b -> ValidatorT m a b
+withError e (MkValidator f) = MkValidator (replaceError e . f)
+
+||| A validator which always fails with a given message.
+export
+fail : Applicative m => String -> ValidatorT m a b
+fail s = MkValidator $ \_ => fail s
+
+infixl 2 >>>
+
+||| Compose two validators so that the second validates the output of the first.
+export
+(>>>) : Monad m => ValidatorT m a b -> ValidatorT m b c -> ValidatorT m a c
+left >>> right = MkValidator (validateT left >=> validateT right)
+
+Monad m => Alternative (ValidatorT m a) where
+    left <|> right = MkValidator \x => MkEitherT $ do
+        case !(runEitherT $ validateT left x) of
+            (Right r) => pure $ Right r
+            (Left e) => case !(runEitherT $ validateT right x) of
+                (Right r) => pure $ Right r
+                (Left e') => pure $ Left (e <+> " / " <+> e')
+
+||| Alter the input before validation using given function.
+export
+contramap : (a -> b) -> ValidatorT m b c -> ValidatorT m a c
+contramap f v = MkValidator (validateT v . f)
+
+
+||| Given a value x and a decision procedure for property p, validateT if p x
+||| holds, returning a proof if it does. The procedure also has access to the
+||| raw input in case it was helpful.
+export
+decide : Monad m => (t -> String) -> ((x : t) -> Dec (p x)) -> PropValidator m t p
+decide msg dec = MkPropValidator \x => case dec x of
+    Yes prf => pure prf
+    No _ => fail (msg x)
+
+||| Given a function converting a into Maybe b, build a Validator of a
+||| converting it into b.
+export
+fromMaybe : Monad m => (a -> String) -> (a -> Maybe b) -> ValidatorT m a b
+fromMaybe e f = MkValidator \a => case f a of
+    Nothing => fail $ e a
+    Just b => pure b
+
+||| Verify whether a String represents a natural number.
+export
+natural : Monad m => ValidatorT m String Nat
+natural = fromMaybe mkError parsePositive
+    where
+    mkError : String -> String
+    mkError s = "'" <+> s <+> "' is not a natural number."
+
+||| Verify whether a String represents an Integer
+export
+integral : (Num a, Neg a, Monad m) => ValidatorT m String a
+integral = fromMaybe mkError parseInteger
+    where
+    mkError : String -> String
+    mkError s = "'" <+> s <+> "' is not an integer."
+
+||| Verify that a string represents a decimal fraction.
+export
+double : Monad m => ValidatorT m String Double
+double = fromMaybe mkError parseDouble
+    where
+    mkError : String -> String
+    mkError s = "'" <+> s <+> "is not a decimal."
+
+
+||| Verify whether a list has a desired length.
+export
+length : Monad m => (l : Nat) -> ValidatorT m (List a) (Vect l a)
+length l = MkValidator (validateVector l)
+    where
+    validateVector : (l : Nat) -> List a -> Result m (Vect l a)
+    validateVector Z [] = pure []
+    validateVector (S _) [] = fail "Missing list element."
+    validateVector Z (_ :: _) = fail "Excessive list element."
+    validateVector (S k) (x :: xs) = do
+        ys <- validateVector k xs
+        pure (x :: ys)
+
+||| Verify that certain values are equal.
+export
+equal : (DecEq t, Monad m) => (a : t) -> PropValidator m t (\b => a = b)
+equal a = MkPropValidator \b => case decEq a b of
+    Yes prf => pure prf
+    No _ => fail "Values are not equal."
+
+||| Verify that a Nat is less than or equal to  certain bound.
+export
+lteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LTE bound)
+lteNat bound = decide
+    (\n => show n <+> " is not lower or equal to " <+> show bound)
+    (\n => isLTE n bound)
+
+||| Verify that a Nat is greater than or equal to certain bound.
+export
+gteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GTE bound)
+gteNat bound = decide
+    (\n => show n <+> " is not greater or equal to " <+> show bound)
+    (isLTE bound)
+
+||| Verify that a Nat is strictly less than a certain bound.
+export
+ltNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LT bound)
+ltNat bound = decide
+    (\n => show n <+> " is not strictly lower than " <+> show bound)
+    (\n => isLTE (S n) bound)
+
+||| Verify that a Nat is strictly greate than a certain bound.
+export
+gtNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GT bound)
+gtNat bound = decide
+    (\n => show n <+> " is not strictly greater than " <+> show bound)
+    (isLTE (S bound))

libs/contrib/contrib.ipkg

@@ -10,11 +10,17 @@ modules = Control.ANSI,
 
           Control.Monad.Algebra,
           Control.Monad.Syntax,
+          Control.Monad.Trans.Either,
 
           Control.Algebra,
           Control.Algebra.Laws,
           Control.Algebra.Implementations,
 
+          Control.Arrow,
+          Control.Category,
+
+          Control.Validation,
+
           Data.Bool.Algebra,
           Data.Bool.Decidable,