diff --git a/docs/DesignPrinciples.md b/docs/DesignPrinciples.md index ddbb287..126303a 100644 --- a/docs/DesignPrinciples.md +++ b/docs/DesignPrinciples.md @@ -1,23 +1,17 @@ # Design Principles of the Constrained Generators System -This document describes the design of the internals of the Constrained Generators System. -It attempts to explain how the system works. +This document describes the design of the internals of the Constrained +Generators System and attempts to explain how the system works. -There is another document -*Constrained Generators Manual* that can be found +There is another document *Constrained Generators Manual* that can be found [here](https://github.com/input-output-hk/constrained-generators/blob/master/docs/DesignPrinciples.md). -This explains the user facing API, and teaches users to write specifications. It is -deliberately silent about the internals of the system. - -In this document we explore the principles that make the system work. To do that we deliberately omit some of the advanced -features having to do with explanations, interfacing with advanced features of Test.QuickCheck, existentials, reifications, -hints, and Generics. We expect another document to deal with those features, which add considerable complexity to the code base. -So we use a much simplified system to describe just the basic principles of how one can add logical properties to -a simple typed lambda calculus, to build a first order logic with typed functions. +This explains the user facing API, and teaches users to write specifications. +It is deliberately (mostly) silent about the internals of the system. ## Constrained Generators is a First-Order Logic -A First-order typed logic (FOTL) has 4 components, where each component uses types to ensure well-formedness. +A First-order typed logic (FOTL) has 4 components, where each component uses +types to ensure well-formedness. 1. **Terms** consisting of - Variables: `x`, `y` . @@ -76,13 +70,12 @@ more detail. Once we have written a `Specification` what can we do with it? Specifications have two interpretations. -1. We can interpret them as a generator of values the meet all the constraints inside the specification. -2. We can interpret them as a function that checks if a given value meets all the constraints inside the specification. - +1. We can interpret them as a generator of values the meet all the constraints inside the specification. +2. We can interpret them as a function that checks if a given value meets all the constraints inside the specification. The first interpretation of the specification is the function `genFromSpec` -``` +```haskell --| Generate a value from the spec in the QuickCheck 'Gen' monad genFromSpec:: (HasCallStack, HasSpec a) => Specification a -> QuickCheck.Gen a ``` @@ -96,7 +89,7 @@ Consider a system of 4 objects, named by the variables, _w,x,y,z_ where we want `(w < x && x < y && y < z) ==> property (w < z)` We might write a QuickCheck property like this -``` +```haskell prop1 :: Gen Property prop1 = do (w,x,y,z) <- arbitrary :: Gen (Int,Int,Int,Int) @@ -118,7 +111,7 @@ then use `genFromSpec` to get the constrained set of random values. We do this i First write a specification that expresses the constraint `(w < x && x < y && y < z)`, then second, embed the call to `genFromSpec` in a QuickCheck property. -``` +```haskell spec4 :: Spec (Integer, Integer, Integer, Integer) spec4 = constrained $ \x -> match x $ \a b c d -> And [Assert $ a <=. b, Assert $ b <=. c, Assert $ c <=. d] @@ -140,7 +133,7 @@ ghci> quickCheck prop2 Now this isn't a very good test either, since the precedent is alway true. A better solution would be to generate a mix, where the precedent is True most of the time, but sometimes False. -``` +```haskell prop3:: Gen Property prop3 = do (w,x,y,z) <- frequency [(9,genFromSpec spec1),(1,arbitrary)] @@ -160,7 +153,7 @@ probability of not being vacuously true. Now lets look closely at the specification, identifying the different parts which make it a statement in a *FOTL* -``` +```haskell spec4 :: Spec (Integer, Integer, Integer, Integer) spec4 = constrained $ \x -> match x $ \a b c d -> And [Assert $ a <=. b, Assert $ b <=. c, Assert $ c <=. d] @@ -174,7 +167,7 @@ spec4 = constrained $ \x -> Here are the complete definitions for `Term` and `Pred` -``` +```haskell data Term a where -- ^ An application of a function symbol `t` to a list of arguments App :: @@ -221,7 +214,7 @@ in the Constrained Generators System. Constructors of a type with kind `([Type] are candidates for function symbols. We make the constuctors real function symbols by making `Syntax`, `Semantics` and `Logic` instances for that type. -``` +```haskell -- | Syntactic operations are ones that have to do with the structure and appearence of the type. class Syntax (t :: [Type] -> Type -> Type) where inFix :: forall dom rng. t dom rng -> Bool @@ -248,7 +241,7 @@ class (Typeable t, Syntax t, Semantics t) => Logic (t :: [Type] -> Type -> Type) Here is an example of a type whose constructors are candidates for function symbols. Note that `IntegerSym` has kind `([Type] -> Type -> Type)` -``` +```haskell data IntegerSym (dom :: [Type]) rng where PlusW :: IntegerSym '[Integer, Integer] Integer MinusW :: IntegerSym '[Integer, Integer] Integer @@ -285,7 +278,7 @@ part of the context pointed to by the arrows (:<|) and (:|>), and this recurive applied to a new spec computed by 'propagate', where the variable `ctx` is replaced by HOLE. We end up on line **4** above, with three nested calls to `propagate`. Here is the defintion of `propagateSpec` -``` +```haskell propagateSpec :: forall v a. HasSpec v => Ctx v a -> Spec a -> Spec v propagateSpec context spec = case context of CtxHole -> spec @@ -308,7 +301,7 @@ programs to access the type stored in this `TypeRep`. The data type `List` implements heterogeneous lists. One can think of this as an inductive tuple. For example -``` +```haskell data List (f :: k -> Type) (as :: [k]) where Nil :: List f '[] (:>) :: f a -> List f as -> List f (a : as) @@ -326,7 +319,7 @@ The `TypeList ds` class constraint, says that `ds` has kind `[Type]` The methods of the `TypeList` class, along with the type family `FunTy`, are used to express the type of, and implement functions that manipulate `List`s -``` +```haskell type family FunTy ts res where FunTy '[] a = a FunTy (a : as) r = a -> FunTy as r @@ -334,7 +327,7 @@ type family FunTy ts res where Ie. `FunTy ds Bool` rewrites to `Integer -> Bool -> [Char] -> Bool` -``` +```haskell -- | Higher-order functions for working on `List`s class TypeList ts where uncurryList :: FunTy (MapList f ts) r -> List f ts -> r @@ -345,7 +338,7 @@ class TypeList ts where ``` Here are some examples that illustrate the methods of `TypeList` -``` +```haskell -- | Fold over a (List Term ts) with 'getTermsize' which consumes a Term component for each element of the list ex1:: Maybe Int ex1 = uncurryList getTermsize args1 @@ -356,7 +349,7 @@ ex1 = uncurryList getTermsize args1 getTermsize _ _ _ = Nothing ``` -``` +```haskell -- Fold over a list with two parts 'unLit' and 'getSize' ex2 :: Int ex2 = uncurryList_ unLit getsize args2 @@ -370,7 +363,7 @@ ex2 = uncurryList_ unLit getsize args2 Construct a function over `Terms` from a function over `(List Term '[a,b,c])` -``` +```haskell ex3 :: Term a -> Term b -> Term c -> String ex3 = curryList crush where crush :: (List Term '[a,b,c] -> String) @@ -380,7 +373,7 @@ ex3 = curryList crush Construct a function `FunTy '[a,b,c] r` from a function over `(List T '[a,b,c] -> r)` and a function from `(a -> T a)` -``` +```haskell ex4 ::Int -> Bool -> String -> Int ex4 = curryList_ one totalLength where totalLength :: List [] '[Int,Bool,String] -> Int @@ -403,7 +396,7 @@ The `HasSpec` class is at the heart of the system. It does two things 1. Identifies the operations necessary to generate random values for a type. 2. Provides the interface to QuickCheck (`genFromSpecT`) that supports writing impliication properties. -``` +```haskell class HasSpec a where -- | The `TypeSpec a` is the type-specific version of `Spec a` for type `a` type TypeSpec a @@ -443,22 +436,22 @@ types: [Bool](#HasSpecBool), [Integer](#HasSpecInteger), [Set a](#HasSpecSet), The type `Spec` is the datatype we use to describe properties about the variables in the `Spec`. It has 5 construtors. - ``` - data Spec a where - -- | There are no constraints at all. - TrueSpec :: Spec a +```haskell +data Spec a where + -- | There are no constraints at all. + TrueSpec :: Spec a - -- | The `Spec` is inconsistent - ErrorSpec :: NonEmpty String -> Spec a + -- | The `Spec` is inconsistent + ErrorSpec :: NonEmpty String -> Spec a --- | The Spec encodes a FOTL statement, with Predicates encoded in the type `Pred` - SuspendedSpec :: HasSpec a => Var a -> Pred -> Spec a + -- | The Spec encodes a FOTL statement, with Predicates encoded in the type `Pred` + SuspendedSpec :: HasSpec a => Var a -> Pred -> Spec a --- | The solution is exactly the elements in the Non empty list - MemberSpec :: NonEmpty a -> Spec a + -- | The solution is exactly the elements in the Non empty list + MemberSpec :: NonEmpty a -> Spec a --- | The solution is embedded in the type-specific `TypeSpec a` - TypeSpec :: HasSpec a => TypeSpec a -> [a] -> Spec a + -- | The solution is embedded in the type-specific `TypeSpec a` + TypeSpec :: HasSpec a => TypeSpec a -> [a] -> Spec a ``` @@ -466,7 +459,7 @@ It has 5 construtors. The `HasSpec Bool` instance is relatively simple, since the type `Bool` has only two elements. -``` +```haskell instance HasSpec Bool where type TypeSpec Bool = Set Bool @@ -508,7 +501,7 @@ instance HasSpec Bool where There is only one function symbol for `Bool` , the negation operation on `Bool`, `not`. -``` +```haskell data BoolSym (dom :: [Type]) rng where NotW :: BoolSym '[Bool] Bool @@ -527,7 +520,7 @@ instance Semantics BoolSym where The `Syntax` and `Semantics` instances are trivial, and should need no explanation. In order to talk about the `Logic` instance we must study the type of the `Logic` method `propagate`. The type of the method `propagate` is -``` +```haskell propagate :: (Logic t, AppRequires t as b, HasSpec a) => t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a ``` @@ -535,7 +528,7 @@ A `ListCtx` is a `Term` with a single `HOLE` and no variables (i.e. everything e For a unary function there is only one context `(Unary HOLE)` because a unary function has only one input, it can only have a `HOLE`, no literal constants are possible. -``` +```haskell instance Logic BoolSym where propagate _ _ TrueSpec = TrueSpec propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs @@ -563,7 +556,7 @@ which using the definition of `anySpec` is `(TypeSpec (Set.fromList [False,True] If the list has exactly 1 element, we apply the continuation to that element, and let the caller of `caseBoolSpec` decide what to do. -``` +```haskell caseBoolSpec :: (HasSpec Bool, HasSpec a) => Spec Bool -> (Bool -> Spec a) -> Spec a caseBoolSpec spec cont = case possibleValues spec of [] -> ErrorSpec (NE.fromList ["No possible values in caseBoolSpec"]) @@ -575,7 +568,7 @@ caseBoolSpec spec cont = case possibleValues spec of Finally, add the function symbol, with (`name NotW` == `"not_"`) as a function over terms -``` +```haskell not_ :: Term Bool -> Term Bool not_ x = App NotW (x :> Nil) ``` @@ -587,7 +580,7 @@ It has both a `Semigroup` and `Monoid` instance. A `Range` denotes a contiguous The Range `(Interval Nothing Nothing)` denotes the interval from negative infinity to positive infinity. A `Range` with a single `Nothing` denotes infinity on only one end. -``` +```haskell data Range = Interval (Maybe Integer) (Maybe Integer) deriving (Eq, Show) unionWithMaybe :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a @@ -620,7 +613,7 @@ the operation `<>` leads to an inconsistent Range where lower bound is greater t The `HasSpec` instance requires an instance for the type family `TypeSpec Integer` and five other methods. -``` +```haskell instance HasSpec Integer where type TypeSpec Integer = Range @@ -670,7 +663,7 @@ To make the `HasSpec Integer` instance usefull we must introduce function symbol `Syntax`, `Semantics` and `Logic` instances for those function symbols. Recall that a datatype whose constructors denote function symbols must have kind `([Type] -> Type -> Type)`. -``` +```haskell data IntegerSym (dom :: [Type]) rng where PlusW :: IntegerSym '[Integer, Integer] Integer MinusW :: IntegerSym '[Integer, Integer] Integer @@ -685,7 +678,7 @@ of the function symbol as `(FunTy dom rng)` which for `PlusW` would be `(+) :: I The function symbol `name` will be a Haskell function over terms. So for `PlusW` we would have `(+.) :: Term Integer -> Term Integer -> Term Integer` -``` +```haskell instance Syntax IntegerSym where name PlusW = "+." name MinusW = "-." @@ -708,7 +701,7 @@ The `Syntax` and `Sematics` are exactly what you would think. The `Logic` instan requires some explanation. First some helper functions for building `Spec Integer` without using any function symbols. They will be useful when we study the `Logic Integer` instance. -``` +```haskell negateRange :: Range -> Range negateRange (Interval ml mu) = Interval (negate <$> mu) (negate <$> ml) @@ -732,12 +725,10 @@ ltSpec n = typeSpec (Interval Nothing (Just (n - 1))) 2. If we have a range that includes [-1,0,1,2,3] `(Interval (Just (-1)) (Just 3))`, then the negation of that range would include [1,0,-1,-2,-3] `(Interval (Just (-3)) (Just 1))` We can compute that by negating and switching the bounds. - 3. The `(geqSpec 6)` means `x` such that `x >= 6`. We encode that as `(Interval (Just 6) Nothing)` 4. The Haskell functions `leqSpec`, `gtSpec`, and `ltSpec` use similar reasoning - -``` +```haskell instance Logic IntegerSym where propagate tag ctx spec = case (tag, ctx, spec) of (_, _, TrueSpec) -> TrueSpec @@ -772,7 +763,7 @@ instance Logic IntegerSym where ``` The type of the method `propagate` is -``` +```haskell propagate :: (Logic t, AppRequires t as b, HasSpec a) => t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a ``` @@ -834,7 +825,7 @@ It says `x conformsTo MemberSpec [11(8+3), 16(13+3)`. Which corresponds to the c Finally we define the lifted versions of the function symbols that work on `Term` -``` +```haskell (<=.) :: Term Integer -> Term Integer -> Term Bool (<=.) x y = App LessOrEqW (x :> y :> Nil) @@ -866,7 +857,7 @@ on constainer types is that they support the quantifier `forAll` which states th meets some constraint. In this minimal implementation, only the `Set` type supports `Container` but in the full system, with `HasSpec` instances for types such as `List` and `Map` , could also have `Container` instances. -``` +```haskell class Container t e | t -> e where fromForAllSpec :: (HasSpec t, HasSpec e) => Spec e -> Spec t forAllToList :: t -> [e] @@ -876,7 +867,7 @@ forAll :: (Container t a, HasSpec t, HasSpec a) => Term t -> (Term a -> Pred) -> Set supports the function symbols defined by the constructors of the `SetSym` datatype. -``` +```haskell data SetSym (dom :: [Type]) rng where MemberW :: (HasSpec a, Ord a) => SetSym [a, Set a] Bool SizeW :: (HasSpec a, Ord a) => SetSym '[Set a] Integer @@ -889,7 +880,7 @@ Set membership, set size, subset, and the quantification over its elements. We will use this type `SetSpec` as the `TypeSpec` for `Set` . Like many `TypeSpecs`, it has both `Semigroup` and `Monoid` instances -``` +```haskell data SetSpec a = SetSpec {setMust :: Set a, setAll :: Spec a, setCount :: Spec Integer} instance (Ord a, HasSpec a) => Semigroup (SetSpec a) where @@ -910,7 +901,7 @@ We will complete the `HasSpec (Set a)` instance description in a number of steps ### `Container` instance for `Set` -``` +```haskell instance Ord s => Container (Set s) s where fromForAllSpec e = typeSpec $ SetSpec mempty e TrueSpec forAllToList = Set.toList @@ -924,7 +915,7 @@ instance Ord s => Container (Set s) s where ### `Syntax` and `Semantics` instances for `SetSym` -``` +```haskell setSize :: Set a -> Integer setSize = toInteger . Set.size @@ -963,7 +954,7 @@ denote a Set with 1 element `a`, and `{}` denotes the empty set. ### Helper functions needed to define the `HasSpec (Set a)` instance -``` +```haskell setSize :: Set a -> Integer setSize = toInteger . Set.size @@ -1005,7 +996,7 @@ knownUpperBound (TypeSpec (Interval lo hi) cant) = upper lo hi ### `HasSpec` instance for Set -``` +```haskell instance (Container (Set a) a, Ord a, HasSpec a) => HasSpec (Set a) where type TypeSpec (Set a) = SetSpec a @@ -1115,7 +1106,7 @@ instance (Container (Set a) a, Ord a, HasSpec a) => HasSpec (Set a) where ### `Logic` instance of `SetSym` -``` +```haskell instance Logic SetSym where propagate tag ctx spec = case (tag, ctx, spec) of (_, _, TrueSpec) -> TrueSpec @@ -1161,7 +1152,7 @@ The function `genFromSpecT` generates a random value from a `Spec`. Of the 5 con involved, in that it consists of 1 or more `Pred`, and possibly multiple variables. Here is a simplified version of `genFromSpecT` to illustrate that point. -``` +```haskell genFromSpecT :: forall a m. (HasCallStack, HasSpec a, MonadGenError m) => Spec a -> GenT m a genFromSpecT (simplifySpec -> spec) = case spec of @@ -1183,7 +1174,7 @@ and the subset of `preds` that mention it. Then we solve each `SolverStep` in th Let's step throught the process on a the simple `SuspendedSpec` **spec3** given below. -``` +```haskell spec3 :: Spec (Integer, Integer, Integer) spec3 = constrained $ \ v4 -> match v4 $ \ v3 v1 v0 -> And [Assert $ v3 <=. v1, Assert $ v1 <=. v0] @@ -1298,7 +1289,7 @@ Since the `constrained` library function defining the original `spec3`, binds th the solution to the `Spec` can be found in the final environment bound by `v_4` which is `(-29,-2,19)`, the other variables are intermediate, and are used only to build the final solution. -``` +```haskell spec3 = constrained $ \ v_4 -> match v_4 $ \ v_3 v_1 v_0 -> And [Assert $ v_3 <=. v_1, Assert $ v_1 <=. v_0] ``` @@ -1313,7 +1304,7 @@ function `computeSpecSimplified` which runs in the `GE` monad which can collect if they occur. The function `localGESpec` catches `GenError`s and turns them into `ErrorSpec` , and re-raises `FatalSpec` if that occurs. -``` +```haskell -- | We want `genError` to turn into `ErrorSpec` and we want `FatalError` to turn into `FatalError` localGESpec ge = case ge of (GenError xs) -> Result $ ErrorSpec (catMessageList xs) @@ -1324,7 +1315,7 @@ localGESpec ge = case ge of Here is a partial definition for `computeSpecSimplified` that illustrates the important operation of handling multiple `Pred` embedded in the FOTL connective `And` -``` +```haskell computeSpecSimplified :: forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a) computeSpecSimplified x preds = localGESpec $ case simplifyPred preds of And ps -> do @@ -1354,7 +1345,7 @@ The complete definition follows. The other (non-And) rules fall into two cases. (which calls `propagateSpec`, which makes one or more calls to `propagate`), to compute the result. -``` +```haskell computeSpecSimplified :: forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a) computeSpecSimplified x pred3 = localGESpec $ case simplifyPred pred3 of @@ -1396,7 +1387,7 @@ This adds considerable complexity to the system, but the key ideas are fuly illu The `TypeSpec` for `(Either a b)` is the datatype `(SumSpec a b)` -``` +```haskell data SumSpec a b = SumSpec (Spec a) (Spec b) deriving (Show) @@ -1413,7 +1404,7 @@ The `HasSpec (Either a b)` instance is quite simple, essentially carrying around `Specs` in `SumSpec a b`. One for values `(Left a)` and a different one for values `(Right b)`. Note the special construtor `Case` of `Pred` specially designed for the type `Either`. -``` +```haskell instance (HasSpec a, HasSpec b) => HasSpec (Either a b) where type TypeSpec (Either a b) = SumSpec a b @@ -1438,7 +1429,7 @@ instance (HasSpec a, HasSpec b) => HasSpec (Either a b) where The function symbols on the Either type are embedded in the `EitherSym` datatype -``` +```haskell data EitherSym (dom :: [Type]) rng where LeftW :: EitherSym '[a] (Either a b) RightW :: EitherSym '[b] (Either a b) @@ -1490,7 +1481,7 @@ for datatypes where a single constructor has multiple components. We will look by nesting binary pairs. The `TypeSpec` for binary pairs is the type `PairSpec`. Which simply pairs two `Spec`. Since `Spec` has a `Monoid` instance, it is trival to make a `Monoid` instance for `PairSpec`. -``` +```haskell data PairSpec a b = Cartesian (Spec a) (Spec b) instance (HasSpec a, HasSpec b) => Show (PairSpec a b) where @@ -1500,14 +1491,13 @@ instance (HasSpec a, HasSpec b) => Semigroup (PairSpec a b) where (Cartesian x y) <> (Cartesian a b) = Cartesian (x <> a) (y <> b) instance (HasSpec a, HasSpec b) => Monoid (PairSpec a b) where mempty = Cartesian mempty mempty - ``` Grouping together two `Spec` is a common occurence. It happens in `SumSpec` (the `TypeSpec` for `Either`) above, and `PairSpec` (the `TypeSpec` for `(a,b)`) here. So combining two `Spec` where one of them may be an `ErrorSpec` deserves a few helper functions. In a sense `hasError` lifts the `HasSpec` method `guardTypeSpec` from type specific `TypeSpec` to the more general type `Spec`. -``` +```haskell -- | Return (Just errormessage) if the input contains an `ErrorSpec` hasError :: forall a. Spec a -> Maybe (NonEmpty String) hasError (ErrorSpec ss) = Just ss @@ -1537,7 +1527,7 @@ handleErrors spec1 spec2 f = case (hasError spec1, hasError spec2) of The `HasSpec (a,b)` instance for pairs is quite simple, relying on the `HasSpec` instances for `a` and `b`. -``` +```haskell instance (HasSpec a, HasSpec b) => HasSpec (a, b) where type TypeSpec (a, b) = PairSpec a b @@ -1559,7 +1549,7 @@ instance (HasSpec a, HasSpec b) => HasSpec (a, b) where The function symbols for pairs are encoded in the datatype `PairSym`. Its `Syntax` and `Semantics` instances are straightforward, except there are two `rewriteRules` which explain how `FstW` and `SndW` distribute over `PairW`. -``` +```haskell data PairSym (dom :: [Type]) rng where FstW :: PairSym '[(a, b)] a SndW :: PairSym '[(a, b)] b @@ -1570,7 +1560,7 @@ data PairSym (dom :: [Type]) rng where ### Syntax, Semantics, and Logic instances for PairSym -``` +```haskell deriving instance Eq (PairSym dom rng) instance Show (PairSym dom rng) where show = name @@ -1594,14 +1584,14 @@ The `Syntax` and `Semantics` instances are very simple, except for the `rewriteR how `FstW` and `SndW` project over a `PairW` application. The pattern matching over the over the application of the `PairW` application uses the Haskell Pattern synonym `Pair` -``` +```haskell -- | Create a Haskell Pattern where (Pair x y) matches (App PairW (x :> y :> Nil)) pattern Pair :: forall c. () => forall a b. (c ~ (a, b), HasSpec a, HasSpec b) => Term a -> Term b -> Term c pattern Pair x y <- App (getWitness -> Just PairW) (x :> y :> Nil) ``` -``` +```haskell instance Logic PairSym where propagateTypeSpec FstW (Unary HOLE) ts cant = typeSpec $ Cartesian (TypeSpec ts cant) TrueSpec propagateTypeSpec SndW (Unary HOLE) ts cant = typeSpec $ Cartesian TrueSpec (TypeSpec ts cant) @@ -1650,7 +1640,7 @@ sameSnd b ps = [a | (a, b') <- ps, b == b'] Finally we introduce the actual function symbols, that create `Term` -``` +```haskell fst_ :: (HasSpec a, HasSpec b) => Term (a, b) -> Term a fst_ x = App FstW (x :> Nil) @@ -1670,7 +1660,7 @@ adds one more component to instance that is one component smaller in size. Here an example of that process for ternary tuples. For the moment the most important part to study is the `TypeSpec` type familiy instance that makes clear the inductive step. -``` +```haskell instance (HasSpec a, HasSpec b, HasSpec c) => HasSpec (a, b, c) where type TypeSpec (a, b, c) = (Spec a, Spec (b, c)) -- Add one more component to binary tuples. @@ -1712,7 +1702,7 @@ The last interesting part is the function symbols `head3_` and `tail3_`, which w Just to emphasize the technique, we give the 4-tuple instance, to be sure to further demonstrate the inductive nature. Here adding an `a` part, to ternary tuple `(b,c,d)`. -``` +```haskell instance (HasSpec a, HasSpec b, HasSpec c, HasSpec d) => HasSpec (a, b, c, d) where type TypeSpec (a, b, c, d) = (Spec a, Spec (b, c, d)) @@ -1748,7 +1738,7 @@ instance (HasSpec a, HasSpec b, HasSpec c, HasSpec d) => HasSpec (a, b, c, d) wh Function symbols, to break Bigger tuples into sub-tuples -``` +```haskell data TupleSym (ds :: [Type]) r where Head3W :: All HasSpec '[a, b, c] => TupleSym '[(a, b, c)] a Tail3W :: All HasSpec '[a, b, c] => TupleSym '[(a, b, c)] (b, c) @@ -1776,7 +1766,7 @@ instance Semantics TupleSym where The `Logic` instance shows how to propagate `Spec` over the function symbols for 3-tuples `Head3W` and `Tail3W`, and 4-tuples `Head4W` and `Tail4W` -``` +```haskell instance Logic TupleSym where propagate _ _ TrueSpec = TrueSpec propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs @@ -1815,7 +1805,8 @@ of complexity to the system. 1. It needs to handle definitions using Derive-Generics 2. It needs to understand how to handle arbitrary Sum-of-Products 3. It needs to provide default method instances that use - [Default method signatures](https://downloads.haskell.org/ghc/9.0.1/docs/html/users_guide/exts/default_signatures.html) for every method of `HasSpec`. + [Default method signatures](https://downloads.haskell.org/ghc/9.0.1/docs/html/users_guide/exts/default_signatures.html) + for every method of `HasSpec`. The amount of extra code is very large, and actually hides the the important ideas behind the Design Principles we discuss in this document. So we have factored it out of the code for diff --git a/docs/Manual.md b/docs/Manual.md index 611ef02..ce3a236 100644 --- a/docs/Manual.md +++ b/docs/Manual.md @@ -2,125 +2,90 @@ The markdown source of this file can be obtained [here](https://github.com/input-output-hk/constrained-generators/blob/master/docs/Manual.md) - -All the examples in this file can be obtained -[here](https://github.com/input-output-hk/constrained-generators/blob/master/examples/Constrained/Examples/ManualExamples.hs) - - -**Table of Contents** - -- [Constrained Generators Manual](#constrained-generators-manual) - - [Constrained Generators is a First-Order Logic](#constrained-generators-is-a-first-order-logic) - - [Design Goals of the Library](#design-goals-of-the-library) - - [HasSpec instances](#hasspec-instances) - - [Building logic specifications using Haskell functions](#building-logic-specifications-using-haskell-functions) - - [Another example using conjunction and simple arithmetic](#another-example-using-conjunction-and-simple-arithmetic) - - [Function Symbols](#function-symbols) - - [Predefined HasSpec instances and their function symbols.](#predefined-hasspec-instances-and-their-function-symbols) - - [Function symbols for numeric types](#function-symbols-for-numeric-types) - - [` Function symbols for Bool`](#-function-symbols-for-bool) - - [Function symbols for List](#function-symbols-for-list) - - [Function symbols for Set](#function-symbols-for-set) - - [Function symbols for Map](#function-symbols-for-map) - - [Generating from and checking against specifications](#generating-from-and-checking-against-specifications) - - [How we solve the constraints](#how-we-solve-the-constraints) - - [How to pick the variable order](#how-to-pick-the-variable-order) - - [The total definition requirement ](#the-total-definition-requirement) - - [Using Match to introduce new variables for subcomponents](#using-match-to-introduce-new-variables-for-subcomponents) - - [Overloaded types in the library](#overloaded-types-in-the-library) -- [Library functions to build Term, Pred, Specification](#library-functions-to-build-term-pred-specification) - - [From Term to Pred](#from-term-to-pred) - - [For all elements in a container type (List, Set, Map)](#for-all-elements-in-a-container-type-list-set-map) - - [Reification](#reification) - - [Disjunction, choosing between multiple things with the same type](#disjunction-choosing-between-multiple-things-with-the-same-type) - - [Primed library functions which are compositions with match](#primed-library-functions-which-are-compositions-with-match) - - [Constructors and Selectors](#constructors-and-selectors) - - [Naming introduced lambda bound Term variables](#naming-introduced-lambda-bound-term-variables) - - [Existential quantifiers](#existential-quantifiers) - - [Conditionals](#conditionals) - - [Explanations](#explanations) - - [Operations to define and use Specifications](#operations-to-define-and-use-specifications) - - [Utility functions](#utility-functions) - - [Escape Hatch to QuickCheck Gen monad](#escape-hatch-to-quickcheck-gen-monad) -- [Strategy for constraining a large type with many nested sub-components.](#strategy-for-constraining-a-large-type-with-many-nested-sub-components) -- [Writing HasSpec instances by hand.](#writing-hasspec-instances-by-hand) - - [Strategy 1 using GHC.Generics](#strategy-1-using-ghcgenerics) - - [Strategy 2 writing your own SimpleRep instance](#strategy-2-writing-your-own-simplerep-instance) - - [Strategy 3 defining the SimpleRep instance in terms of another type with a SimpleRep instance](#strategy-3-defining-the-simplerep-instance-in-terms-of-another-type-with-a-simplerep-instance) - - [Strategy 4, bypassing SimpleRep, and write the HasSpec instance by Hand](#strategy-4-bypassing-simplerep-and-write-the-hasspec-instance-by-hand) -- [A look into the internals of the system.](#a-look-into-the-internals-of-the-system) - - +and all the examples in this file can be found +[here](https://github.com/input-output-hk/constrained-generators/blob/master/examples/Constrained/Examples/ManualExamples.hs). ## Constrained Generators is a First-Order Logic - A First-order typed logic (FOTL) has 4 components, where each component uses types to ensure well-formedness. 1. **Terms** consisting of - Variables: `x`, `y` . - Constants: `5`, `"abc"`, `True` . - - Applications: `elem_ "abc" xs`. Applications apply a function symbol (i.e. `elem_`) to a list of Terms, or support infix application (i.e. `abc ==. y`) + - Function symbols: `elem_`, `(==.)`, `(++.)` + - Applications: `elem_ "abc" xs`. 2. **Predicates** (Assert (x ==. 5)). Predicates are the assertions of boolean typed terms. 3. **Connectives** (And, Not, =>). Connectives make more complex Predicates out of simpler ones. 4. **Quantifiers** (Forall, Exists) -The **Constrained generators** system is almost a FOTL implemented as an embedded domain specific language in Haskell. -We say almost, because it doesn't really have a complete set of connectives. -It allows programmers to write Haskell programs with type `Specification T` that denote a set of random -values for the type `T`, that are subject to a set of constraints expressed as Predicates. This supports property -based testing where a completely random set of values may not be useful. - +The **Constrained generators** system is almost a FOTL implemented as an +embedded domain specific language in Haskell. We say almost, because it +doesn't really have a complete set of connectives. It allows programmers to +write Haskell programs with type `Specification T`, denoting a set of values of +type `T`, using declarative constraints. A `Specification T` in turn can be +used to both _check_ constraints: `check :: Specification T -> (T -> Bool)`, +and _generate values_: `gen :: Specification T -> Gen T`. This supports +property based testing where a completely random set of values may not be +useful without having to write explicit random generation logic. ## Design Goals of the Library The system was designed to have several important properties -1. A Specification determines a `QuickCheck` generator for generating random values subject to constraints. -2. A Specification determines a check that a particular value meets all the specifications constraints. -3. If a Specification is over constrained, the system tries to explain where the conflict occurs. -4. The system is extensible so specifications can be extended to any type. -5. The system is modular so it can be broken into independant modules. - -The first part is implemented by the function `genFromSpec` - -``` +1. A Specification determines a `QuickCheck` generator for generating random + values subject to constraints. +2. A Specification determines a check that a particular value meets all the + specifications constraints. +3. The system is compositional so specifications can be re-used +4. If a Specification is over-constrained, the system tries to explain where + the conflict occurs. +5. The system is extensible so that it can accomodate new types and functions. + +Point (1) is implemented by the following function +```haskell genFromSpec :: HasSpec a => Specification a -> QuickCheck.Gen a ``` - -The second is implemented by the function `conformsToSpec` - -``` +and (2) by this function: +```haskell conformsToSpec :: HasSpec a => a -> Specification a -> Bool ``` - -The third is embodied by the error messages when solving a constraint fails - - -The **Constrained Generators** system is implemented as an embeded domain specific language in Haskell. -The Terms, Predicates, Connectives, and Quantifiers of the first order logic are embedded into three -Haskell datatypes (`Specification t`, `Term t`, and `Pred`). There is a rich (extendable) library -of Haskell functions that can be used to define and construct values of these types. The library is -implemented in a such a way, that the four parts of the logic are defined in ways that are similar -to Haskell expressions with type Bool. - -Let us look at a simple example, and study how this is done. Below is a Haskell declaration that defines a -specification of a pair of Int (`p`) , subject to the constraint that the first component (`x`) -is less than or equal to the second component (`y`) plus 2 - -``` +(3) is captured succinctly by: +```haskell +instance Monoid (Specification t) -- This is far from the whole story... +``` +while (4) is embodied primarily in the error messages given when `genFromSpec` +fails. Point (5) meanwhile requires a bit of explanation and will in no small part +be the subject of this document. + +The **Constrained Generators** system is implemented as an embeded domain +specific language in Haskell. The Terms, Predicates, Connectives, and +Quantifiers of the first order logic are embedded into three Haskell datatypes +(`Specification t`, `Term t`, and `Pred`). There is a rich (extendable) library +of Haskell functions that can be used to define and construct values of these +types. The library is implemented in a such a way, that the four parts of the +logic are defined in ways that are similar (but different in important ways we +will cover below) to Haskell expressions of type Bool. + +Let us look at a simple example and study how this is done. Below is a Haskell +declaration that defines a specification of a pair of Int (`p`) , subject to +the constraint that the first component (`x`) is less than or equal to the +second component (`y`) plus 2 + +```haskell leqPair :: Specification (Int, Int) leqPair = constrained $ \ p -> match p $ \ x y -> assert (x <=. (y + lit 2)) ``` -The library uses Haskell lambda expressions to introduce variables in the Term language of the system, -and Haskell functions to build Terms and Predicates. The Haskell function `lit` takes Haskell values -and turns them into constants in the Term language. We give monomorphic types to the Haskell functions used in the -above definitions. We discuss more general types in a [later section](#overloaded). +The library uses Haskell lambda expressions to introduce variables in the Term +language of the system, and Haskell functions to build `Term`s and +`Predicate`s. The Haskell function `lit` takes Haskell values and turns them +into constants in the Term language. We'll give partially monomorphized types +to the Haskell functions used in the above definitions. We discuss more general +types in a [later section](#overloaded). -``` +```haskell constrained :: HasSpec a => (Term a -> Pred) -> Specification a match :: (HasSpec a, HasSpec b) => Term (a,b) -> (Term a -> Term b -> Pred) -> Pred @@ -132,13 +97,15 @@ assert :: Term Bool -> Pred (<=.) :: OrdLike a => Term a -> Term a -> Term Bool ``` -The Haskell Constraint `HasSpec a` states that the type `a` has been admitted to the system as one of the types -that can be subject to constraints. The system comes with a large set of `HasSpec` instances, including ones for: +The Haskell Constraint `HasSpec a` states that the type `a` has been admitted +to the system as one of the types that can be subject to constraints. The +system comes with a large set of `HasSpec` instances for types in `base` and +`containers`, including ones for: 1. Bool 2. Tuples 3. Sums -4. Numeric types (Int, Integer, Natural, Int8, Int16, Int32, Int64, Word8, Word16, Word32, Word64) +4. Numeric types (Int, Integer, Natural, Int/Word{8,16,32,64}) 5. Lists 6. Maps 7. Sets @@ -149,21 +116,26 @@ that can be subject to constraints. The system comes with a large set of `HasSpe ## HasSpec instances -`HasSpec` instances can always be added to admit more types. Any type with a `GHC.Generics(Generic)` instance can be -given a default instance by using its Sum-of-Products generic definition. In the Cardano Ledger System -over 200 types in the Ledger code base have been given `HasSpec` instances, either by using the `GHC.Generics` path, or by writing the instances by hand. +`HasSpec` instances can always be added to admit more types. Any type with a +`Generic` instance can be given a default instance by using its generic +definition - provided that the types it uses have `HasSpec` instances. In the +Cardano Ledger System over 200 types in the Ledger code base have been given +`HasSpec` instances, either by using the `GHC.Generics` path, or by writing the +instances by hand (more on this later). ## Building logic specifications using Haskell functions -Note that `constrained` and `match` take functions, which abstract over terms, and return `Specification` and `Pred`. -Using the library functions, variables in the Term language are always introduced using Haskell lambda abstractions. And the library -functions combine these into Terms, Preds, and Specifications. +Note that `constrained` and `match` take functions, which abstract over terms, +and return `Specification` and `Pred`. Using the library functions, variables +in the Term language are always introduced using Haskell lambda abstractions. +And the library functions combine these into Terms, Preds, and Specifications. ## Another example using conjunction and simple arithmetic -Suppose we want to put more than one simple condition on the pair of Ints. We would do that using the connective `And` that converts a `[Pred]` into a `Pred` +Suppose we want to put more than one simple condition on the pair of Ints. We +would do that using the connective `And` that converts a `[Pred]` into a `Pred` -``` +```haskell sumPair :: Specification (Int, Int) sumPair = constrained $ \p -> match p $ \x y -> @@ -174,45 +146,43 @@ sumPair = constrained $ \p -> ] ``` -This example also re-illustrates that `(Term Int)` has a (partial) Num instance, and that we can constrain -multiple (different) variables using simple `Num` methods (`(+)`, `(-)`, and `negate`). Note also -the operator: `(==.) :: (Eq n, HasSpec n) => Term n -> Term n -> Term Bool` +This example also re-illustrates that `(Term Int)` has a (partial) Num +instance, and that we can constrain multiple (different) variables using simple +`Num` methods (`(+)`, `(-)`, `(*)`, and `negate`). Note also the operator: +`(==.) :: (Eq n, HasSpec n) => Term n -> Term n -> Term Bool` ## Function Symbols -Note that `(<=.)` , and `(==.)` are two of the function symbols in the first order logic. They obey a -useful naming convention. Infix function symbols corresponding to Haskell infix operators have -corresponding infix operators, lifting Haskell infix functions with type `(a -> b -> c)`, to library infix -functions which have analogous types `(Term a -> Term b -> Term c)` -and are named using the convention that we add the dot `(.)` to the end of the Haskell operator. +Note that `(<=.)` and `(==.)` are two of the function symbols in the first +order logic. They obey a useful naming convention. Infix operators +corresponding to Haskell infix operators named using the convention that we add +the dot `(.)` to the end of the Haskell operator. -A similar naming convention holds for function symbols which are not infix, except instead of adding a -dot to the end of the Haskell name, we add an underscore (`_`) to the end of the Haskell functions's -name. Some examples follow. +A similar naming convention holds for normal prefix function symbols, +except instead of adding a dot to the end of the Haskell name, we add an +underscore (`_`) to the end of the Haskell functions's name. Some examples +follow. -``` -(fst :: (a,b) -> a)` **to** -(fst_ :: (HasSpec a,HasSpec b) => Term (a,b) -> Term a) -``` -``` -(snd :: (a,b) -> b) **to** -(snd_ :: (HasSpec a,HasSpec b) => Term (a,b) -> Term b) -``` +```haskell +fst_ :: (HasSpec a,HasSpec b) => Term (a,b) -> Term a +-- Corresponds to +fst :: (a,b) -> a -``` -(not :: Bool -> Bool) **to** -(not_ :: Term Bool -> Term Bool) -``` +snd_ :: (HasSpec a,HasSpec b) => Term (a,b) -> Term b +-- Corresponds to +snd :: (a,b) -> b -``` -(member :: a -> Set a -> Bool) **to** -(member_ :: HasSpec a => Term a -> Term (Set a) -> Term Bool) +member_ :: HasSpec a => Term a -> Term (Set a) -> Term Bool +-- Corresponds to +member :: a -> Set a -> Bool +-- etc ``` -While the underscored function symbols, may appear to be just to an Applicative lifting over `Term`, that is not the case. -An Applicative lifting would allow the base function to be applied under the `Term` type, but The underscored function symbols -also know how to reason logically about the function. - +While the underscored function symbols may appear to be just to an Applicative +lifting over `Term`, that is not the case. An Applicative lifting would allow +the base function to be applied under the `Term` type, but the underscored +function symbols also know how to reason logically about the function and are +not easily lifted from simple haskell functions. ## Predefined HasSpec instances and their function symbols. @@ -221,9 +191,9 @@ A type with a `HasSpec` instance might have a number of Function Symbols that op There are a number of types that have predefined `HasSpec` instances. As a reference, we list them here along with the types of their function symbols. -### Function symbols for numeric types +### Numeric Types -`(Int, Integer, Natural, Int8, Int16, Int32, Int64, Word8, Word16, Word32, Word64)` +`(Int, Integer, Natural, Int/Word{8, 16, 32, 64})` The function symbols of numeric types are: @@ -234,24 +204,23 @@ The function symbols of numeric types are: 5. `(==.) :: (Eq a, HasSpec a) => Term a -> Term a -> Term Bool` 6. A partial Num instance for (Term n) where n is a Numeric type. Operators `(+)`, `(-)`, `(*)` -### Function symbols for Bool +### Booleans The function symbols of `Bool` are: 1. `(||.) :: Term Bool -> Term Bool -> Term Bool` infix `or` 2. `not_ :: Term Bool -> Term Bool` -### Function symbols for List +### Lists -`HasSpec a => HasSpec [a]` +We have the instance `HasSpec a => HasSpec [a]`. The function symbols of `[a]` are: - 1. `foldMap_ :: (Sized [a], Foldy b, HasSpec a) => (Term a -> Term b) -> Term [a] -> Term b` 2. `singletonList_ :: (Sized [a], HasSpec a) => Term a -> Term [a]` 3. `append_ :: (Sized [a], HasSpec a) => Term [a] -> Term [a] -> Term [a]` -### Function symbols for Set +### Sets `HasSpec a => HasSpec (Set a)` @@ -264,7 +233,7 @@ The function symbols of `(Set a)` are: 5. `disjoint_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term Bool` 6. `fromList_ :: (Ord a, HasSpec a) => Term [a] -> Term (Set a)` -### Function symbols for Map +### Maps `(HasSpec k, HasSpec v) => HasSpec (Map k v)` @@ -281,10 +250,9 @@ Once we have written a `Specification` what can we do with it? Specifications ha 1. We can interpret it as a generator of values the meet all the constraints inside the specification. 2. We can interpret it as a function that checks if a given value meets all the constraints inside the specification. - The first interpretation of the specification is the function `genFromSpec` -``` +```haskell --| Generate a value from the spec in the QuickCheck monad 'Gen' genFromSpec:: (HasCallStack, HasSpec a) => Specification a -> QuickCheck.Gen a ``` @@ -296,11 +264,11 @@ Consider a system of 4 variables _w,x,y,z_ where we want to test the QuickCheck `(w < x && x < y && y < z) ==> property (w < z)` We might write a QuickCheck property like this -``` -prop1 :: Gen Property +```haskell +prop1 :: Property prop1 = do - (w,x,y,z) <- arbitrary :: Gen (Int,Int,Int,Int) - pure $ (w < x && x < y && y < z) ==> property (w < z) + forAll arbitrary $ \(w,x,y,z) :: (Int,Int,Int,Int) -> + (w < x && x < y && y < z) ==> property (w < z) ``` The problem with this is that the probability that the condition `(w < x && x < y && y < z)` is True, for random @@ -315,107 +283,96 @@ ghci> quickCheck prop1 A vacuous pass, becomes a QuickCheck `discard`, so we cannot find 100 successful passes. We can do a better job by constraining the condition using `genFromSpec` -``` +```haskell spec1 :: Specification (Int,Int,Int,Int) spec1 = constrained' $ \ w x y z -> [w <. x, x <. y, y <. z] -prop2:: Gen Property -prop2 = do - (w,x,y,z) <- genFromSpec spec1 - pure $ (w < x && x < y && y < z) ==> property (w < z) +prop2:: Property +prop2 = + forAll (genFromSpec spec1) $ \(w,x,y,z) + (w < x && x < y && y < z) ==> property (w < z) ``` -Now the test passes. +Now the test passes! ``` ghci> quickCheck prop2 +++ OK, passed 100 tests. ``` -Now this isn't a very good test either, since the precedent is alway true. A better solution would be to -generate a mix, where the precedent is True most of the time, but sometimes False. Like this. - -``` -prop3:: Gen Property -prop3 = do - (w,x,y,z) <- frequency [(9,genFromSpec spec1),(1,arbitrary)] - pure $ (w < x && x < y && y < z) ==> property (w < z) -``` - -Observe the result: +The second interpretation of the specification is as a constraint checker, implemented as the function. +```haskell +conformsToSpec :: HasSpec a => a -> Specification a -> Bool ``` -ghci> quickCheck prop3 -+++ OK, passed 100 tests; 7 discarded. -``` - -The `7 discarded` arises because in most random samples of `w`, `x`, `y`, and `z`, the ordering constraint will -not be true, so a discard will occur. Because the ratio of constrained to random is 9 to 1, so the number -of failures is small enough that we don't `give up`. The role of the `arbitrary` is to guard against the possibility -that the constrained spec might be over constrained, and in that case will be values that will never be chosen in a random test. -Which means we will not be choosing a good sample of the test space, so some bugs might escape detection. -By adjusting the test so that any `arbitrary` samples, that are not ordered, pass the test, we identify -a piuntin the sample space that the code does not handle correctly. In a later section we discuss how to use -QuickChrck `classify` and `cover` write better tests. -The purpose of constrained generators is to make it possible to write conditional 'implication' properties -that have a high probability of not being vacuously true, and to combine this with other random -techniques to make better samples of the test-space. +Using this we can write a (admittedly silly) test that showcases this explicitly: +```haskell +spec1 :: Specification (Int,Int,Int,Int) +spec1 = constrained' $ \ w x y z -> [w <. x, x <. y, y <. z] -The second interpretation of the specification is as a constraint checker, implemented as the function. - -``` -conformsToSpec :: HasSpec a => a -> Specification a -> Bool +prop2' :: Property +prop2' = + forAll (genFromSpec spec1) $ \(w,x,y,z) + (w,x,y,z) `conformsToSpec` spec1 ==> property (w < z) ``` +Which similarly will always succeed and should never be discarded. + ## How we solve the constraints +Before we continue delving into how we use the library and the finer points +surrounding generics and overloading it's worth-while to take a detour into how +we solve constraints. Understanding and internalising this will be helpful when +writing anything but the simplest generators. + The strategy for generating things from `Pred`s is relatively straightforward and relies on one key fact: any constraint that has only one free variable `x` and where `x` occurs only once can be turned into a `Specification` for `x`. -We say that such constraints _define_ `x` and given a set of constraints `ps` -and a variable `x` we can split `ps` into the constraints that define `x` and -any constraints that don't. We can then generate a value from `x` by computing -a spec for each defining constraint in `ps` and using the `Semigroup` structure -of `Specification`s to combine them and give them to `genFromSpecT`. Once we obtain a -value for `x` we can substitute this value in all other constraints and pick -another variable to solve. +We say that such constraints _define_ `x` (alt. are _defining_ for `x`) and +given a set of constraints `ps` and a variable `x` we can split `ps` into the +constraints that define `x` and any constraints that don't. We can then +generate a value from `x` by computing a spec for each _defining constraint_ in +`ps` and using the `Semigroup` structure of `Specification`s to combine them +and give them to `genFromSpecT`. Once we obtain a value for `x` we can +substitute this value in all other constraints and pick another variable to +solve. For example, given the following constraints on integers `x` and `y` ``` - x <. 10 - 3 <=. x - y <. x +x <. 10 +3 <=. x +y <. x ``` we see that `x <. 10` and `3 <=. x.` are defining constraints for `x` and there -are no defining constraints for `y`. We compute a `Specification` for `x` for each +are no defining constraints for `y` (yet!). We compute a `Specification` for `x` for each constraint, in this case `x <. 10` turns into something like `(-∞,10)` and `3 <=. x` turns into `[3, ∞)`. We combine the specs to form `[3, 10)` from which we can generate a value, e.g. 4 (chosen by fair dice roll). We then substitute `[x := 4]` in the remaining constraints and obtain `y <. 4`, giving us a defining -constraint for `y`. +constraint for `y`. We then repeat the process for `y`, giving us a specification +like `(-∞,4)` for `y`, from which we can generate a value. ### How to pick the variable order At this point it should be relatively clear that the order we pick for the variables matters a great deal. If we choose to generate `y` before `x` in our example we will have no defining constraints for `y` and so we pick a value for -it freely. But that renders `x` unsolvable if `y > 9` - which will result in +it freely. But that renders `x` unsolvable if `y >= 9` - which will result in the generator failing to generate a value (one could consider backtracking, but -that is very computationally expensive so _relying_ on it would probably not be -wise). +that is very computationally expensive so _relying_ on it would not be wise). Computing a good choice of variable order that leaves the least room for error -is obviously undecidable and difficult and we choose instead an explicit -syntax-directed variable order. Specifically, variable dependency in terms is -_left-to-right_, meaning that the variables in `x + y <. z` will be solved in -the order `z -> y -> x`. On top of that there is a constraint `dependsOn y x` -that allows you to overwrite the order of two variables. Consequently, the -following constraints will be solved in the order `z -> x -> y`: +is difficult and we choose instead an explicit syntax-directed variable order. +Specifically, variable dependency in terms is _left-to-right_, meaning that the +variables in `x + y <. z` will be solved in the order `z -> y -> x`. On top of +that there is a constraint `dependsOn y x` that allows you to overwrite the +order of two variables. Consequently, the following constraints will be solved +in the order `z -> x -> y`: ``` x + y <. z @@ -466,7 +423,7 @@ The principal problem above is that information that is present in the constraints is lost, which would force us to rely on a `suchThat` approach to generation - which will become very slow as constraint systems grow. -### Using Match to introduce new variables for subcomponents +### Using `match` to introduce new variables for subcomponents A solution to the total definition requirement is to *introduce more variables*. We can rewrite the problematic `fst p <. snd p` example below as: @@ -492,8 +449,8 @@ constraints - these need to be bound somewhere - and (2) the order of `fst_ p = x` is important, `p` depends on `x`, and not the other way around. -To do both of these things at the same time we use the `match` construct -to the language: +To do both of these things at the same time we use the `match` construct to the +language: ``` match :: Term (a,b) -> (Term a -> Term b -> Pred) -> Pred @@ -518,9 +475,8 @@ match p $ \ x y -> x <. y In previous sections we provided some types for several of the library functions: `constrained`, `match`, - -``` -constrained:: HasSpec a => (Term a -> Pred) -> Specification a +```haskell +constrained :: HasSpec a => (Term a -> Pred) -> Specification a match :: (HasSpec a, HasSpec b) => Term (a,b) -> (Term a -> Term b -> Pred) -> Pred @@ -529,14 +485,14 @@ match :: (HasSpec a, HasSpec b) => It turns out, that these functions would be much more useful with more general types. This also applies to some other library functions (`reify`, `caseOn`, etc.) we have not yet introduced. The general type of `constrained` is: -``` -constrained:: (IsPred p, HasSpec a) => (Term a -> p) -> Specification a +```haskell +constrained :: (IsPred p, HasSpec a) => (Term a -> p) -> Specification a ``` This general type allows the function passed to `constrained` to be any function, that given a Term, returns any type that acts like a `Pred`. The class IsPred is defined as follows, and has 4 instances. -``` +```haskell class Show p => IsPred p where toPred :: p -> Pred @@ -548,14 +504,14 @@ instance IsPred Pred Thus the following would be type-correct calls to constrained. -``` +```haskell ex1 :: Specification Int ex1 = constrained $ \ x -> True -- Any Haskell Boolean value ex2 :: Specification Int ex2 = constrained $ \ x -> x ==. lit 3 --- Any Haskell term, with type (Term Bool) +-- Any Haskell term, with type Term Bool ex3 :: Specification Int ex3 = constrained $ \ x -> [ x <=. lit 2, x >=. lit 5 ] @@ -566,24 +522,30 @@ ex4 = constrained $ \ x -> assert $ x == lit 9 -- Anything with type Pred ``` -The type of `match` is also overloaded. It supports writing specifications over type with sub-components, allowing -each sub-component to be individually constrained. +The type of `match` is similarly overloaded. It supports writing specifications +over type with sub-components, allowing each sub-component to be individually +constrained. The `match` library function is used to introduce new `Term` variables for the sub-components of another type. If `t` has type `T`, and `T` has 3 sub-components, then the `match` function would take a Haskell lambda expression with three parameters. `(match t $ \ x y z -> ...)`. Its overloaded type is: -``` -match - :: (HasSpec a, IsProductType a, IsPred p) => - Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred +``` haskell +match :: ( HasSpec a + , IsProductType a + , IsPred p + ) => Term a + -> FunTy (MapList Term (ProductAsList a)) p + -> Pred ``` -The meaning of this is a bit hard to parse: `IsProductType a`. It means the type `a` is isomorphic to a product type. -I.e. isomorphic to `(t1,t2, ..., tn)` So all tuples would work. So would any type whose constructor had -one or more arguments, So would any type whose HasSpec instance was derived via the GHC.Generics instance. -So in summary, if the type `a` has **n** distinct parts, then the constraint (`IsProductType a`) is met, -and the interpretation of the `FunTy` is a function with **n** parameters. +The meaning of this is a bit hard to parse: `IsProductType a`. It means the +type `a` is isomorphic to a product type. I.e. isomorphic to `(t1,t2, ..., tn)` +So all tuples would work. So would any type with a single constructor of +one or more arguments whose HasSimpleRep instance was derived via the +GHC.Generics instance. So in summary, if the type `a` has **n** distinct +parts, then the constraint (`IsProductType a`) is met, and the interpretation +of the `FunTy` is a function with **n** parameters. ``` type FunTy (MapList Term (ProductAsList a)) p = t1 -> t2 -> ... -> tn -> p @@ -596,7 +558,7 @@ type FunTy (MapList Term (ProductAsList a)) p = t1 -> t2 -> ... -> tn -> p `assert` lifts a `(Term Bool)` to a `Pred`. by using the `IsPred` class, we can often get around using it, but it becomes necessary when we want to use the `And` operator, and the operands of `And` are a mix of `Pred`, `(Term Bool), and other operations. Here is a very simple use. Further examples illustrate its use in more challenging contexts. -``` +```haskell ex5 :: Specification [Int] ex5 = constrained $ \ xs -> assert $ elem_ 7 xs ``` @@ -609,7 +571,7 @@ Note that `elem_` is the function symbol corresponding to `Data.List.elem`. The library function `forAll` is used to impose a constraint on every element of a container type. There are three `Forallable` instances in the Base system. -``` +```haskell class Forallable t e | t -> e where instance Ord k => Forallable (Map k v) (k, v) instance Ord a => Forallable (Set a) a @@ -618,7 +580,7 @@ instance Forallable [a] a Here is an example of its use. -``` +```haskell ex6 :: Specification [Int] ex6 = constrained $ \ xs -> forAll xs $ \ x -> [ x <=. 10, x >. 1] @@ -664,7 +626,7 @@ The first use: `(reifies b a f)`, says a term `b` can be obtained from a term ` Here is an example of its use. Internally, it works by forcing the solution of `a` before solving for `b`, applying the `f` to the solution for `a`, and then constructing a `(Term b)` obtained from this value. -``` +```haskell ex7 :: Specification (Int,[Int]) ex7 = constrained $ \ pair -> match pair $ \ n xs -> @@ -688,7 +650,7 @@ True The second operation `reify` can be defined using `reifies` by placing an existential constraint on the range of the function. Here is an example of the use of `reify` -``` +```haskell ex8 :: Specification ([Int],[Int]) ex8 = constrained $ \ pair -> match pair $ \ xs1 xs2 -> @@ -718,7 +680,7 @@ True The third operation `assertReified` can be used to place a boolean constraint on the existential. Here is an example of its use. -``` +```haskell ex9 :: Specification Int ex9 = constrained $ \x -> [ assert $ x <=. 10 @@ -751,7 +713,7 @@ Sometimes we want to choose between several different specifications for the sam Let's look at the first. Multiple constuctors from the same type. This uses the `caseOn` library functions and its two helper functions `branch` (where each constructor is choosen equally) and `branchW` (where we can give weights, to determine the frequency each constructor is choosen). The type of `caseOn` -``` +```haskell caseOn :: Term a -> FunTy @@ -766,7 +728,7 @@ unweighted using `(branch ...)`, where the `...` is a function with *m* paramete subcomponents of that constructor). First we introduce a sum of products type `Three` and use the GHC.Generics instance to derive the HasSpec instance. -``` +```haskell data Three = One Int | Two Bool | Three Int deriving (Ord, Eq, Show, Generic) instance HasSimpleRep Three instance HasSpec Three @@ -774,7 +736,7 @@ instance HasSpec Three Here is an example using the mechanism with no weights (`branch`), where every branch is equilikely. -``` +```haskell ex10 :: Specification Three ex10 = constrained $ \ three -> caseOn three @@ -788,7 +750,7 @@ expects the branches to be in the same order the constructors are introduced in Here is another example using the weighted mechanism (`branchW`). -``` +```haskell ex11 :: Specification Three ex11 = constrained $ \ three -> caseOn three @@ -805,13 +767,13 @@ The second way to specify disjunctions is to choose `chooseSpec`, where the two type, but are distinguished logically by the two input specifications. The type of `chooseSpec` is as follows, where the `Int` determines the frequency of each choice. -``` -chooseSpec:: HasSpec a => (Int, Specification a) -> (Int, Specification a) -> Specification a +```haskell +chooseSpec :: HasSpec a => (Int, Specification a) -> (Int, Specification a) -> Specification a ``` Here is an example. -``` +```haskell ex12 :: Specification (Int,[Int]) ex12 = chooseSpec (5, constrained $ \ pair -> @@ -852,7 +814,7 @@ defined interms of the un-primed function and `match`, and the second defined nt The primed version of `forAll` is `forAll'` -``` +```haskell ex13a :: Specification [(Int,Int)] ex13a = constrained $ \ xs -> forAll xs $ \ x -> match x $ \ a b -> a ==. negate b @@ -864,7 +826,7 @@ ex13b = constrained $ \ xs -> The primed version of `constrained` is `constrained'` -``` +```haskell ex14a :: Specification (Int,Int,Int) ex14a = constrained $ \ triple -> match triple $ \ a b c -> [ b ==. a + lit 1, c ==. b + lit 1] @@ -876,7 +838,7 @@ ex14b = constrained' $ \ a b c -> [ b ==. a + lit 1, c ==. b + lit 1] The primed version of `reify` is `reify'` -``` +```haskell ex15a :: Specification (Int,Int,Int) ex15a = constrained $ \ triple -> match triple $ \ x1 x2 x3 -> @@ -899,7 +861,7 @@ In Haskell we can define data types with multiple constructors, and constructors The library functions `onCon`, `sel`, and `isJust`, allow us to constrain such types in a way less verbose than using the `caseOn` library function. Consider the following -``` +```haskell ex16 :: Specification Three ex16 = constrained $ \ three -> caseOn three @@ -916,7 +878,7 @@ This requires that the GHC language directive`{-# LANGUAGE DataKinds #-}` be in Then apply it to a Term with the type returned by that constructor, followed by a Haskell function with one parameter for each subcomponent of that constructor, that returns a Pred. Here is `ex16` redone using three `onCon` predicates. -``` +```haskell ex17:: Specification Three ex17 = constrained $ \ three -> [ onCon @"One" three (\ x -> x==. lit 1) @@ -929,21 +891,21 @@ The real power of `onCon` is when you only want to constrain one (or a subset) o and the other constructors remain unconstrained. Here we only constrain the constructor `Three` and the constructors `One` and `Two` remain unconstrained. -``` +```haskell ex18:: Specification Three ex18 = constrained $ \ three -> onCon @"Three" three ( \ x -> x==. lit 3) ``` Here is another example where we only constrain the constructor `Just` of the maybe type. -``` +```haskell ex19 :: Specification (Maybe Bool) ex19 = constrained $ \ mb -> onCon @"Just" mb (\ x -> x==. lit False) ``` Haskell allows the definition of data types with named selectors. Here is an example. -``` +```haskell data Dimensions where Dimensions :: { length :: Int @@ -956,7 +918,7 @@ instance HasSpec Dimensions This introduces Haskell functions with types -``` +```haskell length :: Dimensions -> Int width :: Dimensions -> Int depth :: Dimensions -> Int @@ -967,14 +929,14 @@ instances, the we can use the `sel` library function to create lifted versions o the Haskell selector functions like this. Nothe that the lifted `width` uses the trailing under score convention: `width_` because it manipulates `Term`s not values. -``` +```haskell width_ :: Term Dimensions -> Term Int width_ d = sel @1 d ``` This requires the `DataKinds` directive, and importing `GHC.Generics` and `GHC.TypeLits` to work. -``` +```haskell {-# LANGUAGE DataKinds #-} import GHC.Generics import GHC.TypeLits @@ -984,7 +946,7 @@ When we type-apply the library function `sel` to a type-level `Natural` number l selects the `ith` selector function. The selectors are numbered from `0` to `n-1` . Selection can always be expressed using `match` like this: -``` +```haskell ex20a :: Specification Dimensions ex20a = constrained $ \ d -> match d $ \ l w d -> [ l >. lit 10, w ==. lit 5, d <. lit 20] @@ -992,7 +954,7 @@ ex20a = constrained $ \ d -> which can be reexpressed using `sel` as this. -``` +```haskell ex20b :: Specification Dimensions ex20b = constrained $ \ d -> [sel @0 d >. lit 10 @@ -1003,14 +965,14 @@ ex20b = constrained $ \ d -> When we wish to constrain just a subset of the subcomponents, selectors make it possible to write more concise `Specification`s. -``` +```haskell ex21 :: Specification Dimensions ex21 = constrained $ \ d -> width_ d ==. lit 1 ``` ## Naming introduced lambda bound Term variables -1. [var|name|] +1. `[var|name|]` When we use a library function that introduces new Term variable using a Haskell lambda expression, the system gives the Haskell variable a unique Term level name such as `v0` or `v1` or `v2` etc. When the specification is @@ -1019,7 +981,7 @@ Term level names that were assigned to the Haskell variables. This means the err understand. For example consider the over constrained specification. It is over constrained because `left` cannot be simultaneously equal to `right` and `right + lit 1` -``` +```haskell ex22a :: Specification (Int,Int) ex22a = constrained $ \ pair -> match pair $ \ left right -> @@ -1042,14 +1004,14 @@ Note the error message is in terms of the internal Term name `v1`. Which is not To make error messages clearer we can name Haskell lambda bound variables using `[var|left|]` instead of just `left`. In order to do this we must have the following directives in our file. -``` +```haskell {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ViewPatterns #-} ``` Here is the same example using this naming schema. -``` +```haskell ex22b :: Specification (Int,Int) ex22b = constrained $ \ [var|pair|] -> match pair $ \ [var|left|] [var|right|] -> [ left ==. right, left ==. right + lit 1] @@ -1069,36 +1031,32 @@ Original spec ErrorSpec ## Existential quantifiers -1. `exists` -2. `unsafeExists` - - -Sometimes we want to constrain a variable, in terms of another internal or hidden variable. -A classic example is constraining a number to be odd. A number `x` is odd, if there exists -another internal number `y`, such that, `x` is equal to `y + y + 1` - +1. `exists` +2. `unsafeExists` -Here is an example. +Sometimes we want to constrain a variable, in terms of another internal or +hidden variable. A classic example is constraining a number to be odd. A +number `x` is odd, if there exists a number `y` such that `x == y + y + 1`: -``` +```haskell ex22 :: Specification Int ex22 = constrained $ \ [var|oddx|] -> unsafeExists (\ [var|y|] -> [Assert $ oddx ==. y + y + 1]) ``` -Why do we call the library function `unsafeExists`? It is unsafe because the library function -`conformsToSpec` will fail to return `True` when called on a generated result. Why? -Because the system does not know how to find the internal, hidden variable. To solve this -the safe function `exists` takes two Haskell lambda expressions. The first is a function -that tells how to compute the hidden variable from the values returned by solving the constraints. -The second is the normal use of a Haskell lambda expression to introduce a Term variable -naming the hidden variable. Here is an example. +Why do we call the library function `unsafeExists`? It is unsafe because the +library function `conformsToSpec` will fail to return `True` when called on a +generated result. Why? Because the system does not know how to find the +hidden variable `y`. To solve this the safe function `exists` takes two +Haskell lambda expressions. The first is a function that tells how to compute +the hidden variable from the values returned by solving the constraints. The +second is the normal use of a Haskell lambda expression to introduce a Term +variable naming the hidden variable: -``` +```haskell ex23 :: Specification Int -ex23 = ExplainSpec ["odd via (y+y+1)"] $ - constrained $ \ [var|oddx|] -> +ex23 = constrained $ \ [var|oddx|] -> exists -- first lambda, how to compute the hidden value for 'y' (\eval -> pure (div (eval oddx - 1) 2)) @@ -1107,19 +1065,21 @@ ex23 = ExplainSpec ["odd via (y+y+1)"] $ (\ [var|y|] -> [Assert $ oddx ==. y + y + 1]) ``` -One might ask what is the role of the parameter `eval` in the first lambda expression passed to `exists`. -Recall that we are trying assist the function `conformsToSpec` in determining if a completely known value -conforms to the specification. In this context, every Term variable is known. But in the specification we -only have variables with type `(Term a)`, what we need are variables with type `a`. The `eval` functional parameter -has type +One might ask what is the role of the parameter `eval` in the first lambda +expression passed to `exists`. Recall that we are trying assist the function +`conformsToSpec` in determining if a _completely known_ value conforms to the +specification. In this context, every Term variable bound before this point is +known. But in the specification we only have variables with type `(Term a)`, +what we need are variables with type `a`. The `eval` functional parameter has +type: ``` eval :: Term a -> a ``` -This, lets us access those values. In the example the Term variable `(oddx :: Term Int)` is in scope, so +This lets us access those values. In the example the Term variable `(oddx :: Term Int)` is in scope, so `(eval oddx :: Int)`, and since this is only used when calling `conformsToSpec`, we actually have the -value of the `oddx` for `eval` to return. Finally `(div (eval oddx - 1) 2))` tells us how to compute +value of the `oddx` for `eval` to return. Finally `div (eval oddx - 1) 2` tells us how to compute the value of the hidden variable. @@ -1131,7 +1091,7 @@ If one has a term `x` with type `(Term Bool)` one could use the value of this te define a Specification conditional on this term by using the `(caseOn x ...)` library function. There are two more concise library function one can use instead. -``` +```haskell whenTrue :: IsPred p => Term Bool -> p -> Pred ifElse :: (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred ``` @@ -1139,7 +1099,7 @@ ifElse :: (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred For example consider the data type `Rectangle` where the selector `square` indicates that the rectangle has equal length width and length. -``` +```haskell data Rectangle = Rectangle { wid :: Int, len :: Int, square :: Bool} deriving (Show, Eq,Generic) instance HasSimpleRep Rectangle @@ -1148,7 +1108,7 @@ instance HasSpec Rectangle We can enforce this in a specification as follows. -``` +```haskell ex26 :: Specification Rectangle ex26 = constrained' $ \ wid len square -> [ assert $ wid >=. lit 0 @@ -1161,7 +1121,7 @@ Note that there are no constraints relating `wid` and `len` if the selector `squ The library function `ifElse` allows two separate sets of constraints, one when the `square` is `True` and a completely separate set when `square` is `False` -``` +```haskell ex27 :: Specification Rectangle ex27 = constrained' $ \ wid len square -> ifElse square @@ -1178,7 +1138,7 @@ ex27 = constrained' $ \ wid len square -> Explanations allow the writer of a specification to add textual message, that can be used if solving a specification fails. These library functions have type -``` +```haskell explanation :: NonEmpty String -> Pred -> Pred assertExplain :: IsPred p => NonEmpty String -> p -> Pred ExplainSpec :: [String] -> Specification a -> Specification a @@ -1186,7 +1146,7 @@ ExplainSpec :: [String] -> Specification a -> Specification a Here is a specification with no explanations -``` +```haskell ex28a :: Specification (Set Int) ex28a = constrained $ \ s -> [ assert $ member_ (lit 5) s @@ -1205,7 +1165,7 @@ While combining 2 SetSpecs By adding an `ExplainSpec` like this -``` +```haskell ex28b :: Specification (Set Int) ex28b = ExplainSpec ["5 must be in the set"] $ constrained $ \ s -> @@ -1226,7 +1186,7 @@ While combining 2 SetSpecs (SetSpec must=[ 5 ] elem=TrueSpec @(Int) size=TrueSpec @(Integer)) ``` -``` +```haskell ex28c :: Specification (Set Int) ex28c = constrained $ \ s -> explanation (pure "5 must be in the set") @@ -1253,7 +1213,7 @@ There are a number of library functions that create specifications directly and do not use the `constrained` library function. These are particulary useful in conjunction with the library function `satisfies` which converts a `Specification` into a `Pred` -``` +```haskell satisfies :: HasSpec a => Term a -> Specification a -> Pred equalSpec :: a -> Specification a notEqualSpec :: HasSpec a => a -> Specification a @@ -1267,7 +1227,7 @@ cardinality :: (Number Integer, HasSpec a) => Specification a -> Specification I Here is an example of the use of `satisfies` in conjunction with `notMemberSpec` -``` +```haskell ex29 :: Specification Int ex29 = constrained $ \ x -> [ assert $ x >=. lit 0 @@ -1288,7 +1248,7 @@ In essence this spec says `x` is either `0`, `1`, `4`, or `5`, where These functions are generally useful when writing and debugging specifications. -``` +```haskell -- | Simplify a Term simplifyTerm :: Term a -> Term a @@ -1320,7 +1280,7 @@ debugSpec :: HasSpec a => Specification a -> IO () The function `forAllSpec` allows one to turn a `Specification` into a QuickCheck `Property` -``` +```haskell forAllSpec :: (HasSpec a, QuickCheck.Testable p) => Specification a -> (a -> p) -> QuickCheck.Property @@ -1329,7 +1289,7 @@ forAllSpec :: The librrary function `monitor` allows specification writers to access some of the QuickCheck property modifiers, like `classify`, `label`, and `cover`, by turning them into a `Pred` using `monitor` -``` +```haskell monitor :: ((forall a. Term a -> a) -> QuickCheck.Property -> QuickCheck.Property) -> Pred @@ -1338,7 +1298,7 @@ monitor The monitor `Pred` has no effect, unless the `Specification` that embeds the `monitor` call, is lifted to a `Property` using `forAllSpec. Here is a example. -``` +```haskell ex30 :: Specification (Int, Int) ex30 = constrained $ \ [var|p|] -> match p $ \ [var|x|] [var|y|] -> @@ -1372,7 +1332,7 @@ True The second example uses `forAllSpec` to create a `Property`, that passes as long as the generator does not fail. -``` +```haskell prop31 :: QuickCheck.Property prop31 = forAllSpec ex30 $ \_ -> True ``` @@ -1396,7 +1356,7 @@ We modify it by adding a `monitor` predicate. The purpose of this example is two 1. Illustrate the use of `monitor` 2. Demonstrate that the weighted `caseOn` changes the frequency at which the branches are choosen. -``` +```haskell ex11m :: Specification Three ex11m = constrained $ \ three -> [ caseOn three @@ -1448,7 +1408,7 @@ to build a skeleton `Specification` that does nothing more than just bring into (possibly nested) subcomponent. We build a deeply nested example by building on top of the types from previous examples `Three` and `Rectangle`. We introduce a new deeply nested type `Nested` -``` +```haskell data Nested = Nested Three Rectangle [Int] deriving (Show,Eq,Generic) instance HasSimpleRep Nested @@ -1464,7 +1424,7 @@ this stage is to just introduce a variable for each subcomponent. So we use `Tr no constraints on each of these subcomponents. We use named variables, and use a comment to label each `branch` with the name of the construtor. -``` +```haskell skeleton :: Specification Nested skeleton = constrained $ \ [var|nest|] -> match nest $ \ [var|three|] [var|rect|] [var|line|] -> @@ -1477,10 +1437,11 @@ skeleton = constrained $ \ [var|nest|] -> ] ``` -Once we have the `skeleton` compiling, we can replace each `TruePred` with some constraints. -In this stage, we worry just about the constraints, and which `Pred` to use, and not about how we bring -a variable into scope for each subcomponent. Experience show that we have way fewer compiler -errors, using this one step at a time strategy. +Once we have the `skeleton` compiling, we can replace each `TruePred` with some +constraints. In this stage, we worry just about the constraints, and which +`Pred` to use, and not about how we bring a variable into scope for each +subcomponent. Experience show that we have way fewer compiler errors, using +this one step at a time strategy. # Writing HasSpec instances by hand. @@ -1527,7 +1488,7 @@ so do not forget to put the deriving clause `deriving (Generic,Eq,Show)` in the This strategy depends on the provided `(SimpleRep T)` associated type family instance, being an actual Sum-of-Products type. This requires quite a bit of knowledge about the internals of the system. Let's look closely at the `SimpleRep` class -``` +```haskell class Typeable (SimpleRep a) => HasSimpleRep a where type SimpleRep :: * -> * type family SimpleRep a @@ -1537,15 +1498,14 @@ class Typeable (SimpleRep a) => HasSimpleRep a where What kind of type lends itself to this strategy? 1. A type that has internal structure that enforces some internal invariants. -2. A type that has a -builder- function, that takes simple input, and constructs the internal struture. -3. A type that has an -accessor- function, that takes the internal structure, and returns the simple input. -4. A type where the -simple input- has a Sum-of-Products representation. +2. A type that has a _builder_ function, that takes simple input, and constructs the internal struture. +3. A type that has an _accessor_ function, that takes the internal structure, and returns the simple input. +4. A type where the _simple input_ has a Sum-of-Products representation. -Often the -builder- function is implemented as a Haskell Pattern. Here is an example that come from the Cardano Ledger. +Often the _builder_ function is implemented as a Haskell Pattern. Here is an example that come from the Cardano Ledger. A lot of complicated stuff is not fully describe here, but the example gives an overview of how it works. - -``` +```haskell -- NOTE: this is a representation of the `ShelleyTxOut` type. You can't -- simply use the generics to derive the `SimpleRep` for `ShelleyTxOut` -- because the type is memoized (i.e. it stores a hidden copy of the actual bytes that @@ -1568,14 +1528,14 @@ instance (Era era, Val (Value era)) => HasSimpleRep (ShelleyTxOut era) where instance (EraTxOut era, HasSpec (Value era)) => HasSpec (ShelleyTxOut era) ``` -TODO add more explanation about the types. Much of the example of depends on properties of TxOut -that is not explained. + ## Strategy 3 defining the SimpleRep instance in terms of another type with a SimpleRep instance The type `Coin` is a defined as -``` +```haskell newtype Coin = Coin {unCoin :: Integer} ``` The operations on Coin ensure the invariant that one cannot build a `Coin` with a negative value. @@ -1583,7 +1543,7 @@ We can enforce these invariants in a `SimpleRep` instance by making the `SimpleR `Natural` is one of the numeric types, and has its own `SimpleRep` instance, so it is a good choice. Here is the `SimpleRep` instance, and the `HasSpec` instance defined using that representation. -``` +```haskell instance HasSimpleRep Coin where type SimpleRep Coin = Natural toSimpleRep (Coin i) = case integerToNatural i of @@ -1605,7 +1565,7 @@ naturalToCoin = Coin . fromIntegral To write a `Specification` for `Coin` we simply `match` against it, and then use the operations on the underlying type `Word64` to constraint it. -``` +```haskell ex34 :: Specification Coin ex34 = constrained $ \coin -> match coin $ \ nat -> [nat >=. lit 100, nat <=. lit 200] @@ -1627,7 +1587,7 @@ Coin {unCoin = 119} The `HasSpec` class has an associated type family and many methods. Here is a summary of some of it. -``` +```haskell class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec a)) => HasSpec a where -- | The `TypeSpec a` is the type-specific `Specification a`. type TypeSpec a