Skip to content

Instantly share code, notes, and snippets.

@MonoidMusician
Created October 31, 2021 04:59
Show Gist options
  • Save MonoidMusician/9bee19403323873ee9a7e62682acd08a to your computer and use it in GitHub Desktop.
Save MonoidMusician/9bee19403323873ee9a7e62682acd08a to your computer and use it in GitHub Desktop.
Validation example
module Main where
import Prelude
import Effect (Effect)
import Effect.Class (class MonadEffect)
import Halogen as H
import Halogen.Aff (awaitBody, runHalogenAff)
import Halogen.HTML as HH
import Halogen.HTML.Properties as HP
import Halogen.HTML.Events as HE
import Halogen.VDom.Driver (runUI)
import Control.Monad.Free (Free, resume)
import Control.Monad.Free as Free
import Control.Plus (empty)
import Data.Array as Array
import Data.Array.NonEmpty (NonEmptyArray)
import Data.Bifoldable (bifoldMap)
import Data.Bifunctor (class Bifunctor, bimap)
import Data.Either (Either(..), either)
import Data.FoldableWithIndex (foldMapWithIndex, traverseWithIndex_)
import Data.Int as Int
import Data.List (List, (:))
import Data.List as List
import Data.Map (SemigroupMap(..))
import Data.Map as Map
import Data.Maybe (Maybe(..), maybe)
import Data.Monoid.Disj (Disj(..))
import Data.String as String
import Data.These (These(..), theseLeft, theseRight)
import Data.Traversable (foldMap)
import Data.Tuple (Tuple(..))
import Effect (Effect)
import Effect.Console (log)
import Unsafe.Coerce (unsafeCoerce)
main :: Effect Unit
main = runHalogenAff do
body <- awaitBody
runUI component unit body
type HState = String
data Action = Set String
component :: forall query input output m. MonadEffect m => H.Component query input output m
component =
H.mkComponent
{ initialState
, render
, eval: H.mkEval $ H.defaultEval { handleAction = handleAction }
}
initialState :: forall input. input -> HState
initialState _ = parseValidateAndShow "v = 4, v = 5 ; k = 1, k = 2"
render :: forall m. HState -> H.ComponentHTML Action () m
render state = do
HH.div_
[ HH.p_ [ HH.text "Enter statements `variable = value` separated by `,` or `;` or `!`"]
, HH.textarea
[ HE.onValueInput Set, HP.prop (H.PropName "defaultValue") "v = 4, v = 5 ; k = 1, k = 2" ]
, HH.pre_ [ HH.text state ]
]
handleAction :: forall output m. MonadEffect m => Action -> H.HalogenM HState Action () output m Unit
handleAction = case _ of
Set s -> do
H.put (parseValidateAndShow s)
-- Here's the application:
-- We have a set of constraints that appear in our sourcecode and we need them to be consistent
-- For concreteness it's just going to be `varName = intVal`
-- With two caveats:
-- While we're running it, we want to validate that the strings are nonempty
-- And we want to parse the values into integer values
type Constrain = { name :: String, value :: String }
constrainS :: String -> String -> Source
constrainS name value = pure { name, value }
infix 1 constrainS as :=$
constrainI :: String -> Int -> Source
constrainI name value = pure { name, value: show value }
infix 1 constrainI as :=%
-- Pretend we have a tree structure to our source, for fun :)
type Source = Free Array Constrain
mkSource :: Array Source -> Source
mkSource = Free.wrap
flatSource :: Array Constrain -> Source
flatSource = mkSource <<< map pure
-- A location looks like a list of indices into the arrays
-- (It is treated like a snoc list, the order is reverse of what you expect)
type SourceLoc = List Int
-- This is a parsing/validation error:
-- Left s means s is a bad variable name
-- Right s means s is not an integer
type Message = Either String String
-- An error will be a map of inconsistencies:
-- 2 or more values (tagged with locations!) that did not agree
type Error = SemigroupMap String (InconsistencyWithInfos SourceLoc Int)
-- A pure result will be a map of values, with the locations they occurred
type Result = SemigroupMap String (DiscreteWithInfos SourceLoc Int)
-- The monoidal state underlying this all is a map to occurrences (1 or more)
type State = SemigroupMap String (OccurrencesWithInfos SourceLoc Int)
parse :: String -> Source
parse = trySplit "!" >=> trySplit ";" >=> trySplit "," >>> map splitValue
where
trySplit s v = case String.split (String.Pattern s) v of
[ _ ] -> pure v
vs -> Free.wrap (map pure vs)
splitValue v = case String.trim <$> String.split (String.Pattern "=") v of
[ name, value ] -> { name, value }
_ -> { name: "", value: String.trim v }
parseValidateAndShow :: String -> String
parseValidateAndShow = parse >>> validateAndShow
parseValidateAndPrint :: String -> Effect Unit
parseValidateAndPrint = parse >>> validateAndPrint
validateAndShow :: Source -> String
validateAndShow = validate >>> \{ errors, state } ->
let
shown = state # foldMapWithIndex \k (Tuple (Total locs) (Discrete value)) ->
" " <> show k <> " = " <> show value <> " at " <> showLocs locs <> "\n"
in errors <> if String.null shown then "" else "Results:\n" <> shown
validateAndPrint :: Source -> Effect Unit
validateAndPrint = validateAndShow >>> log
showLoc :: SourceLoc -> String
showLoc List.Nil = "top"
showLoc as = String.joinWith "." $ Array.reverse $ Array.fromFoldable $ map show as
showLocs :: NonEmptyArray SourceLoc -> String
showLocs = String.joinWith ", " <<< Array.fromFoldable <<< map showLoc
validate :: Source -> { errors :: String, state :: Result }
validate top = case provideLoc empty (validateFrom top) of
Success st (_ :: Unit) -> { errors: "", state: unStateOf st }
Error es st (mu :: Maybe Unit) ->
{ errors: maybe "Fatal errors!\n" mempty mu <>
bifoldMap (renderError <<< unErrorOf) (foldMap renderMessage) es
, state: unStateOf st
}
where
renderMessage (Tuple loc e) = case e of
Left (s :: String) -> "Invalid name " <> show s <> " at " <> showLoc loc <> "\n"
Right (s :: String) -> "Invalid int value " <> show s <> " at " <> showLoc loc <> "\n"
renderError :: Error -> String
renderError = foldMapWithIndex \k is ->
"Variable " <> show k <> " had conflicting values assigned:" <>
renderInconsistencies is <> "\n"
renderInconsistencies (Inconsistent l0 a0 l1 a1) =
renderInconsistency l0 a0 <> renderInconsistency l1 a1
renderInconsistencies (Additional is l a) =
renderInconsistencies is <> renderInconsistency l a
renderInconsistency l a =
"\n " <> show (a :: Int) <> " at locations " <> showLocs l
type M = LocSE SourceLoc State Message
validateFrom :: Source -> LocSE SourceLoc State Message Unit
validateFrom top =
let
-- Sometimes we parse and validate :)
-- https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/
-- For the names, we want to ensure they are nonempty
validateName :: String -> Boolean
validateName = not String.null
-- We can continue easily on failure
validateNameAnd :: forall a. String -> M a -> M a
validateNameAnd s = if validateName s then identity else
\act -> recoverLocSE unit (throwLocSE (Left s)) *> act
-- For the values, we want to extract an integer value
parseValue :: String -> Maybe Int
parseValue = Int.fromString
-- But if we fail to do so, we cannot really recover
parseValueAnd :: forall a. String -> (Int -> M a) -> M a
parseValueAnd s f = case parseValue s of
Nothing -> throwLocSE (Right s)
Just v -> f v
writeValue :: { name :: String, value :: Int } -> M Unit
writeValue { name, value } =
askLocSE >>= \l ->
writeLocSE (SemigroupMap $ Map.singleton name (Tuple (Total (pure l)) (Discrete value)))
in case resume top of
Right { name, value } ->
validateNameAnd name $
parseValueAnd value \parsed ->
writeValue { name, value: parsed }
Left layer -> traverseWithIndex_ (\i -> localLocSE (\loc -> i : loc) <<< validateFrom) layer
newtype Total m = Total m
type Gracefail o m = Tuple (Maybe o) m
-- Split a monoid `w` into a subsemigroup `o` that represents errors
-- (it should not contain the identity) and a subset `m` that represents a
-- partial monoid of success cases that may fail to combine.
class (Monoid w, ErrorSemigroup o m w) <= ErrorMonoid o m w | w -> o m where
emempty :: w -> m
class (Semigroup w, Semigroup o) <= ErrorSemigroup o m w | w -> o m where
split :: w -> These o m
ocomb :: o -> w
mcomb :: m -> w
foreign import data ErrorOf :: Type -> Type
mkErrorOf :: forall o m w. ErrorSemigroup o m w => o -> ErrorOf w
mkErrorOf = unsafeCoerce
unErrorOf :: forall o m w. ErrorSemigroup o m w => ErrorOf w -> o
unErrorOf = unsafeCoerce
upErrorOf :: forall o m w. ErrorSemigroup o m w => ErrorOf w -> w
upErrorOf = ocomb <<< unErrorOf
instance ErrorSemigroup o m w => Semigroup (ErrorOf w) where
append o1 o2 = mkErrorOf (unErrorOf o1 <> unErrorOf o2)
foreign import data StateOf :: Type -> Type
mkStateOf :: forall o m w. ErrorSemigroup o m w => m -> StateOf w
mkStateOf = unsafeCoerce
unStateOf :: forall o m w. ErrorSemigroup o m w => StateOf w -> m
unStateOf = unsafeCoerce
upStateOf :: forall o m w. ErrorSemigroup o m w => StateOf w -> w
upStateOf = mcomb <<< unStateOf
zeroState :: forall o m w. ErrorMonoid o m w => StateOf w
zeroState = mkStateOf (emempty (mempty :: w))
type GracefailOfs w = Gracefail (ErrorOf w) (StateOf w)
eappend :: forall o m w. ErrorSemigroup o m w => StateOf w -> StateOf w -> These (ErrorOf w) (StateOf w)
eappend m1 m2 = bimap mkErrorOf mkStateOf (split (mcomb (unStateOf m1) <> mcomb (unStateOf m2) :: w))
emappend :: forall o m w. ErrorMonoid o m w => StateOf w -> StateOf w -> Gracefail (ErrorOf w) (StateOf w)
emappend m1 m2 = mollify zeroState (eappend m1 m2)
mollify :: forall o m. m -> These o m -> Gracefail o m
mollify m0 = case _ of
This o -> Tuple (Just o) m0
That m -> Tuple Nothing m
Both o m -> Tuple (Just o) m
splitGrace :: forall o m w. ErrorMonoid o m w => w -> Gracefail (ErrorOf w) (StateOf w)
splitGrace = mollify zeroState <<< bimap mkErrorOf mkStateOf <<< split
instance (Ord k, ErrorSemigroup o m w) =>
ErrorSemigroup (SemigroupMap k o) (SemigroupMap k m) (SemigroupMap k w) where
split = map split >>> \(SemigroupMap together) ->
Both (SemigroupMap (Map.mapMaybe theseLeft together)) (SemigroupMap (Map.mapMaybe theseRight together))
ocomb = map ocomb
mcomb = map mcomb
instance (Ord k, ErrorSemigroup o m w) =>
ErrorMonoid (SemigroupMap k o) (SemigroupMap k m) (SemigroupMap k w) where
emempty = pure (SemigroupMap Map.empty)
newtype Discrete a = Discrete a
-- TODO: generalize to non-discrete orders
data InconsistencyWithInfo l a = Inconsistent l a l a | Additional (InconsistencyWithInfo l a) l a
derive instance Functor (InconsistencyWithInfo l)
addInconsistencyWithInfo :: forall l a. Semigroup l => Eq a => InconsistencyWithInfo l a -> l -> a -> InconsistencyWithInfo l a
addInconsistencyWithInfo as' l' a' =
let Tuple (Disj v) r = go as' in if v then r else Additional r l' a'
where
merge (Tuple l0 a0) = if a0 == a'
then Tuple (Disj true) (Tuple (l0 <> l') a0)
else pure (Tuple l0 a0)
go (Inconsistent l0 a0 l1 a1) = ado
Tuple l0' a0' <- merge (Tuple l0 a0)
Tuple l1' a1' <- merge (Tuple l1 a1)
in Inconsistent l0' a0' l1' a1'
go (Additional as l a) = ado
as' <- go as
Tuple l' a' <- merge (Tuple l a)
in Additional as' l' a'
instance (Semigroup l, Eq a) => Semigroup (InconsistencyWithInfo l a) where
append as (Inconsistent l0 a0 l1 a1) =
addInconsistencyWithInfo (addInconsistencyWithInfo as l0 a0) l1 a1
append as0 (Additional as1 l a) =
addInconsistencyWithInfo (as0 <> as1) l a
data OccurrencesWithInfo l a = Occurrence l a | Again (OccurrencesWithInfo l a) l a
derive instance Functor (OccurrencesWithInfo l)
addOccurrencesWithInfo :: forall l a. Semigroup l => Eq a => OccurrencesWithInfo l a -> l -> a -> OccurrencesWithInfo l a
addOccurrencesWithInfo as' l' a' =
let Tuple (Disj v) r = go as' in if v then r else Again r l' a'
where
merge (Tuple l0 a0) = if a0 == a'
then Tuple (Disj true) (Tuple (l0 <> l') a0)
else pure (Tuple l0 a0)
go (Occurrence l0 a0) = ado
Tuple l0' a0' <- merge (Tuple l0 a0)
in Occurrence l0' a0'
go (Again as l a) = ado
as' <- go as
Tuple l' a' <- merge (Tuple l a)
in Again as' l' a'
instance (Semigroup l, Eq a) => Semigroup (OccurrencesWithInfo l a) where
append as (Occurrence l0 a0) =
addOccurrencesWithInfo as l0 a0
append as0 (Again as1 l a) =
addOccurrencesWithInfo (as0 <> as1) l a
isConsistent :: forall l a. OccurrencesWithInfo l a -> Either (InconsistencyWithInfo l a) (DiscreteWithInfo l a)
isConsistent (Occurrence l a) = Right (Tuple (Total l) (Discrete a))
isConsistent (Again as0 l0 a0) = Left (mkInconsistent as0 l0 a0)
where
mkInconsistent (Occurrence l1 a1) = Inconsistent l1 a1
mkInconsistent (Again as l1 a1) = Additional (mkInconsistent as l1 a1)
type DiscreteWithInfo l a = Tuple (Total l) (Discrete a)
type OccurrencesWithInfos l a = OccurrencesWithInfo (NonEmptyArray l) a
type InconsistencyWithInfos l a = InconsistencyWithInfo (NonEmptyArray l) a
type DiscreteWithInfos l a = DiscreteWithInfo (NonEmptyArray l) a
instance (Semigroup l, Eq a) => ErrorSemigroup (InconsistencyWithInfo l a) (DiscreteWithInfo l a) (OccurrencesWithInfo l a) where
split = either This That <<< isConsistent
ocomb (Inconsistent l0 a0 l1 a1) = Again (Occurrence l0 a0) l1 a1
ocomb (Additional as l a) = Again (ocomb as) l a
mcomb (Tuple (Total l) (Discrete a)) = Occurrence l a
data SE w e a
= Success (StateOf w) a
| Error (These (ErrorOf w) (NonEmptyArray e)) (StateOf w) (Maybe a)
derive instance Functor (SE w e)
instance Bifunctor (SE w) where
bimap _ g (Success s a) = Success s (g a)
bimap f g (Error es s ma) = Error (map (map f) es) s (map g ma)
acc :: forall o e. Semigroup o => Semigroup e =>
These o e -> Maybe o -> These o e
acc = flip case _ of
Nothing -> identity
Just o2 -> case _ of
This _ -> This o2
That e1 -> Both o2 e1
Both _ e1 -> Both o2 e1
eths :: forall o e. Semigroup o => Semigroup e =>
These o e -> These o e -> These o e
eths = case _ of
This o1 -> case _ of
This o2 -> This (o1 <> o2)
That e2 -> Both o1 e2
Both o2 e2 -> Both (o1 <> o2) e2
That e1 -> case _ of
This o2 -> Both o2 e1
That e2 -> That (e1 <> e2)
Both o2 e2 -> Both o2 (e1 <> e2)
Both o1 e1 -> case _ of
This o2 -> Both (o1 <> o2) e1
That e2 -> Both o1 (e1 <> e2)
Both o2 e2 -> Both (o1 <> o2) (e1 <> e2)
exErrorOf :: forall o m w e. ErrorMonoid o m w => These (ErrorOf w) e -> w
exErrorOf = bifoldMap upErrorOf mempty
instance (ErrorMonoid o m w) => Apply (SE w e) where
apply (Success m1 f) (Success m2 a) = case emappend m1 m2 of
Tuple (Just o) m3 -> Error (This o) m3 (Just (f a))
Tuple Nothing m3 -> Success m3 (f a)
apply (Error e1 m1 mf) (Success m2 a) =
case splitGrace (exErrorOf e1 <> upStateOf m1 <> upStateOf m2) of
Tuple os m3 -> Error (acc e1 os) m3 (mf <#> (_ $ a))
apply (Success m1 f) (Error e2 m2 ma) =
case splitGrace (upStateOf m1 <> exErrorOf e2 <> upStateOf m2) of
Tuple os m3 -> Error (acc e2 os) m3 ((f $ _) <$> ma)
apply (Error e1 m1 mf) (Error e2 m2 ma) =
case splitGrace (exErrorOf e1 <> upStateOf m1 <> exErrorOf e2 <> upStateOf m2) of
Tuple os m3 -> Error (acc (eths e1 e2) os) m3 (mf <*> ma)
instance (ErrorMonoid o m w) => Applicative (SE w e) where
pure = Success zeroState
instance (ErrorMonoid o m w) => Bind (SE w e) where
bind (Success m1 a) f = case f a of
Success m2 b -> case emappend m1 m2 of
Tuple (Just o) m3 -> Error (This o) m3 (Just b)
Tuple Nothing m3 -> Success m3 b
Error e2 m2 mb ->
case splitGrace (upStateOf m1 <> exErrorOf e2 <> upStateOf m2) of
Tuple os m3 -> Error (acc e2 os) m3 mb
bind (Error e1 m1 (Just a)) f = case f a of
Success m2 b -> case splitGrace (exErrorOf e1 <> upStateOf m1 <> upStateOf m2) of
Tuple os m3 -> Error (acc e1 os) m3 (Just b)
Error e2 m2 mb -> case splitGrace (exErrorOf e1 <> upStateOf m1 <> exErrorOf e2 <> upStateOf m2) of
Tuple os m3 -> Error (acc (eths e1 e2) os) m3 mb
bind (Error e1 m1 Nothing) _ = Error e1 m1 Nothing
recoverSE :: forall o m w e a. ErrorMonoid o m w => a -> SE w e a -> SE w e a
recoverSE a (Error es s Nothing) = Error es s (Just a)
recoverSE _ v = v
newtype LocSE l w e a =
LocSE (l -> SE w (Tuple l e) a)
derive instance Functor (LocSE l w e)
instance (ErrorMonoid o m w) => Apply (LocSE l w e) where
apply (LocSE mf) (LocSE ma) = LocSE \l ->
mf l <*> ma l
instance (ErrorMonoid o m w) => Applicative (LocSE l w e) where
pure = LocSE <<< pure <<< pure
instance (ErrorMonoid o m w) => Bind (LocSE l w e) where
bind (LocSE ma) f = LocSE \l ->
ma l >>= \a -> case f a of LocSE mb -> mb l
provideLoc :: forall l w e a. l -> LocSE l w e a -> SE w (Tuple l e) a
provideLoc l (LocSE f) = f l
writeLocSE :: forall l o m w e. ErrorMonoid o m w => m -> LocSE l w e Unit
writeLocSE m = LocSE \_ ->
Success (mkStateOf m) unit
throwLocSE :: forall l o m w e a. ErrorMonoid o m w => e -> LocSE l w e a
throwLocSE e = LocSE \l ->
Error (That (pure (Tuple l e))) zeroState Nothing
recoverLocSE :: forall l o m w e a. ErrorMonoid o m w => a -> LocSE l w e a -> LocSE l w e a
recoverLocSE a (LocSE f) = LocSE \l ->
recoverSE a (f l)
localLocSE :: forall l o m w e a. ErrorMonoid o m w => (l -> l) -> LocSE l w e a -> LocSE l w e a
localLocSE ll (LocSE f) = LocSE \l0 -> f (ll l0)
askLocSE :: forall l o m w e. ErrorMonoid o m w => LocSE l w e l
askLocSE = LocSE \l -> Success zeroState l
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment