Last time, I was looking into establishing equality on various conditions on `Wai.Request`, but established that this wasn’t what I was looking for. We did, however, establish how to perform casts and use polymorphic lists in a fashion that’s quite OO. Now I’m planning to drive right off road and try a bit of type-level reasoning.

Let’s start by simplifying the problem we had last time. Let’s stoop worrying about complex record types and just deal with primitive types. We’ll restrict our attention to equality and comparison conditions on those types. Let’s start by setting up some machinery.

``data Equality = Eql | NEql deriving (Show, Ord, Eq, Typeable)``
``````equalityAsFunc :: (Eq a) => Equality -> a -> a -> Bool
equalityAsFunc Eql = (==) equalityAsFunc NEql = (/=)``````
``data Comparison = LTh | LThE | GThE | GTh deriving (Show, Eq, Ord, Typeable)``
``````comparisonAsFunc :: (Ord a) => Comparison -> a -> a -> Bool
comparisonAsFunc LTh = (<)
comparisonAsFunc LThE = (<=)
comparisonAsFunc GTh = (>)
comparisonAsFunc GThE = (>=)``````
``````class Invertable a where
invert :: a -> a``````
``````instance Invertable Comparison where
invert LTh = GThE
invert GTh = LThE
invert GThE = LTh
invert LThE = GTh``````
``````instance Invertable Equality where
invert Eql = NEql
invert NEql = Eql``````
``````-- I could make all functors of a invertable invertable, but I'm not sure that would actually be a good idea.
instance (Invertable a) => Invertable (Maybe a) where
invert = fmap invert``````
``````-- Util
infixl 3 <|!> (<|!>) :: Maybe a -> a -> a
(<|!>) = flip fromMaybe``````

Now, we’re going to have a Condition typeclass, and at the very least we’re going to have instances for “always true/false”, “test for equality/inequality” and “compare against value”. And here’s the important bit: we’re going to want to analyze the relationship between them, even if they’re not the same type.

``data ConditionRelationship = Same | Compatible | Incompatible | AImpliesB | BImpliesA deriving (Show, Ord, Eq, Typeable)``
``````instance Invertable ConditionRelationship where
invert AImpliesB = ImpliesA
invert BImpliesA = AImpliesB
invert x = x``````

Young Rankenstein

Now, how would we achieve this in an OO world? Well, we’d implement something like this:

``````class Condition0 c where
analyze = (Condition0 d) => c -> d -> Maybe ConditionRelatioship``````

Where we’d return `Nothing` if `c` didn’t know how to analyze its relationship with `d`. Using the `cast` mechanism we’ve already seen, you can definitely implement this. And indeed, I did. (I tried an approach involving a more symmetric approach and some type magic, but ultimately couldn’t get it to fly.)

Let’s revise the definition a little so that we can actually it to test values. But we’re going to have to introduce a second type, `v`, the value under test.

``````{-# LANGUAGE RankNTypes #-}
class Condition1 v a where
analyzeSame :: a -> a -> ConditionRelationship
analyzeDifferent :: (Condition1 v b) => a -> b -> Maybe ConditionRelationship
test :: a -> v -> Bool``````
``````analyze :: (Condition1 v a, Condition1 v b) => a -> b -> ConditionRelationship
analyze x y = a <|> b <|> c <|!> Compatible
-- If we have no idea, say it's compatible
where a = analyzeSame x <\$> (cast y)
b = analyzeDifferent x y
c = invert \$ analyzeDifferent y x``````

Now, there’s actually a serious problem with this code: it doesn’t even compile! The problem is with the `v`s in `analyze`. It can’t determine that they’re the same. This I actually find weird, given that I’ve specified that `a` and `b` share a `v`, but it’s solvable.

First, I want to talk a bit about what the rank 2 typeclass actually is. It specifies a set of functions that can be called with an `a` and a `v`, but doesn’t restrict the `a` or the `v` in any way. So, all it’s really giving you is a relationship between the two types. And `analyze` never uses `v`, so it can’t deduce anything about it.

Now, there’s an extension called `FunctionalDependencies` and another called `TypeFamilies` that’d resolve this, but actually all we need to do is take the `test` method back out.

``````class (Eq a, Show a, Typeable a, Invertable a) => Condition2 a where
analyzeSame2 :: a -> a -> ConditionRelationship
analyzeDifferent2 :: (Condition2 b) => a -> b -> Maybe ConditionRelationship``````
``````class (Condition2 a) => Condition3 v a where
test :: a -> v -> Bool``````
``````analyze2 :: (Condition2 a, Condition2 b) => a -> b -> ConditionRelationship
analyze2 x y = a <|> b <|> c <|!> Compatible -- We have no idea, say it's compatible
where a = analyzeSame2 x <\$> (cast y)
b = analyzeDifferent2 x y
c = invert \$ analyzeDifferent2 y x``````

That works, doesn’t use any more extensions, (although Lord knows I’ve been playing extension pokemon recently) and also leaves us with the possibility of using different `v`s with the same `a`, even if in this particular case I can’t see why we’d wish to. For that matter, we could remove the interdependency between the two.

``````class Condition4 v a where
test :: a -> v -> Bool``````

I found it really interesting the process I went through here: we actually ended up with a better design and separated our concerns as a consequence of the type system complaining about the functions we actually implemented.

Into The Lens

Let’s rename our concepts:

``````class (Eq a, Show a, Typeable a, Invertable a) => Analyzable a where
analyzeSame :: a -> a -> ConditionRelationship
analyzeDifferent :: (Analyzable b) => a -> b -> Maybe ConditionRelationship``````
``````class Testable v a where
test :: a -> v -> Bool``````

First some definitions:

``````data Value c v = Value {
_value :: v,
_condition :: c
} deriving (Typeable, Eq, Show)``````
``makeLenses ''Value``
``````instance (Invertable c) => Invertable (Value c v) where
invert = over condition invert``````

I’m using the `lens` package here, although to be honest I’m really only using it to start learning it. The actual practical benefits of it in the code I’ve written are very small, but I’m hoping to slowly pick up more aspects. In fact, of the code I’ve written so far this is the only bit that actually shows an improvement.

Breaking it down, we’re saying that if a `condition` is invertable, a `Value` using that `condition` is invertable by inverting the `condition`. Even though this is pretty elegant, but it’s going to take me a fair while to get my head around lens in general (There’s been loose talk of a lens NICTA-style course, that would be awesome.).

Scopes Monkey

So, we can declare an equality value to be a condition:

``instance (Typeable a, Show a, Eq a) => Condition a (Value Equality a) where``

I’m deliberately skipping the instance code because it’s pretty boring and predictable. The interesting case is when we’re implementing comparison:

``analyzeEqualOther :: (Invertable b, Testable v b) => b -> Equal v -> ConditionRelationship``

(I’ll skip the implementation.) Now for an instance:

``````instance (Typeable a, Show a, Ord a) => Analyzable (Value Comparison a) where
analyzeSame = analyzeCompSame -- elided
analyzeDifferent x y = analyzeEqualOther x <\$> y2
where y2 = cast y``````

Makes sense. Doesn’t compile. The reason’s a bit weird: it can’t figure out exactly what to cast `y` to. So let’s try this:

``    where y2 = (cast y :: Maybe (Value Equality a))``

Still doesn’t work. Here, the error message isn’t particularly helpful (unlike quite a few that just point you directly to the extension that you might need). The problem is actually that the `a` in the `y2` expression isn’t the same as the `a` in the instance declaration. I don’t really understand why that decision was made (the explanation probably features the word “parametricity”), but you can reverse it by adding in another extension:

``{-# LANGUAGE ScopedTypeVariables #-}``

QuickCheck Yourself

There’s a plethora of things we could test, but let’s start with this one: What actually is the relationship between the `Analyzeable` version of condition and the `Testable` version of condition? Well, the answer is approximately that given two types that are both, we should be able to pick a set of `v`s such that we can deduce the behaviour of one from the other.

It would be lovely if we could achieve this through the type system, but I think that would be a serious reach, and even if it was possible it’s doubtful it would be readable. So instead let’s try using QuickCheck, the original property testing tool.

Aside: conversely, there should be no value of `v` where the behaviour of the two contradict one another. However, this latter condition is kind of hard to demonstrate using any example-based system. For that, you really do want Idris.

We need to set up some infrastructure to make cabal run tests.

``````Test-suite test
Type:              exitcode-stdio-1.0
Hs-source-dirs:    test
Main-is:           Main.hs
Build-depends:     base >=4.7 && <4.8,
tasty,
tasty-quickcheck,
derive,
QuickCheck,
myprojectname``````

This introduces a new target called `test`. I’ve not used quickcheck before so this is quite interesting. `tasty` appears to be the standard test running infrastructure. Note that since the test code is actually a separate executable, you need to put your own code as a dependency.

Stuck In The Middle With You

So, let’s pick five distinct values, `a`, `b`, `c`, `d` and `e`. We’ll put conditions at `b` and `d` and then test all five values in pairs. We can then read out from the set of pairs what the correct relationships between the two conditions is.

``````import Test.QuickCheck

data TestValues x = TestValues {
a :: x,
b :: x,
c :: x,
d :: x,
e :: x
} deriving (Show, Eq, Ord)

instance (Arbitrary a, Ord a, Num a) => Arbitrary (TestValues a) where
arbitrary = do
a <- getPositive <\$> arbitrary
b <- (a +) <\$> getPositive <\$> arbitrary
c <- (b +) <\$> getPositive <\$> arbitrary
d <- (c +) <\$> getPositive <\$> arbitrary
e <- (d +) <\$> getPositive <\$> arbitrary
return (TestValues a b c d e)``````

This is all rather fun: `arbitrary` returns a value in the `Gen` monad. `getPositive` unwraps a `Positive` and return type polymorphism kicks in.

Normally, though, how to create an `Arbitrary` instance is obvious given its components, setting them up is going to get boring real fast, which is where the `derive` package kicks in

``````{-# LANGUAGE TemplateHaskell #-}
import Data.DeriveTH

derive makeArbitrary ''Equality
derive makeArbitrary ''Comparison
derive makeArbitrary ''Value``````

This now enables us to write the code we wanted:

``````propDeduce :: (Analyzable (Value c1 v), R.Testable v (Value c1 v), Analyzable (Value c2 v), R.Testable v (Value c2 v))
=> c1 -> c2 -> TestValues v -> Bool
propDeduce c1 c2 testValues = expected == drawConclusion x y testValues where
x = Value c1 (b testValues)
y = Value c2 (d testValues)
expected = analyze x y

drawResults :: (R.Testable v (Value c1 v), R.Testable v (Value c2 v))
=> (Value c1 v) -> (Value c2 v) -> TestValues v -> [(Bool,Bool)]
drawResults x y testValues = result where
result = f <\$> ([a, b, c, d, e] <*> (pure testValues))
f v = (test x v, test y v)

drawConclusion :: (R.Testable v (Value c1 v), R.Testable v (Value c2 v))
=> (Value c1 v) -> (Value c2 v) -> TestValues v -> ConditionRelationship
drawConclusion x y testValues = ac (length conclusions) conclusions where
conclusions = nub \$ drawResults x y testValues
ac 4 _ = Compatible
ac 3 _ = ac3 missingConclusion
ac _ x | null \$ x \ [(True,True),(False,False)] = Same
ac _ _ = Incompatible
missingConclusion = head \$ [(True, True),(True, False),(False, True),(False,False)] \ conclusions
ac3 (False, True) = BImpliesA
ac3 (True, False) = AImpliesB
ac3 (True, True) = Incompatible
ac3 _ = Compatible``````

You can now write quickcheck properties like

``````prop_deduceCompEq :: Comparison -> Equality -> TestValues Int -> Bool
prop_deduceCompEq = propDeduce``````

(There may be a better way of instantiating propDeduce with different types, but this definitely works.)

In practice, what now happens is you spend a large amount of time actually fixing your code and your tests. What you’re seeing above is the output of that process. I learned a few things in the process.

• Although QuickCheck is good at telling you there’s a problem, it’s got no facilities at all for telling you why.
• Having relatively complex types makes it quite hard to reproduce a test in the repl. Conceivably the tooling for this could be improved.
• You need to split your code up into chunks that are testable in the repl. This is a lesson Clojure taught me as well, but having access to an excellent debugger in other languages keeps unteaching it.

This is getting really long: I’ve skipped over the entire tasty `code` and the entire implementation.

Review

So the `Condition` design looks more appropriate to the aim of actually allowing us to optimize our tests, and Haskell’s led us to a typeclass design better than the original item. There are, however, certain problems. For instance, the design I’ve outlined here is incapable of spotting that “> 2” is the same as “>= 3” in the `Integer` domain. Pretty much the only good solution to this is to require stronger conditions than just `Eq` and `Ord` for condition values, which allow you to perform these analyses. I’m not very inclined to do that, but this problem doesn’t ruin my intended use. However, it highlights again just how challenging it is to write something truly polymorphic and correct.

It’s pretty easy to see how you can extend this into projections as well. However, in practice it gets pretty tricky, because you need to do an order 2 cast. Thankfully, I got a good answer on StackOverflow of exactly how to achieve that. Separating out the concept of the condition from the projection also seems like a strong idea. Ultimately, though, I don’t really like the way this is going. Casts work, and `Maybe` makes them safe, but the design feels like I’m circumventing the type system rather than using it.