Very experimental! An introductory talk is available here from BOB 2016 (slides)
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE OverloadedStrings #-}
import GHC.TypeLits
import Data.Proxy
import Data.Monoid
import qualified Data.Text as Text
import Verdict
Sometimes you want to provide extra guarantees about a type that are best expressed in terms of a smart constructor with an opaque type:
newtype NonEmptyList' a = NonEmptyList' { getList :: [a] }
makeNonEmptyList :: [a] -> Maybe (NonEmptyList' a)
makeNonEmptyList x | null x = Nothing
| otherwise = Just (NonEmptyList' x)
Where the NonEmptyList' constructor is not exported.
This works, but it has quite a few downsides. You can no longer derive things
like Read and FromJSON without losing the invariants you set up. If you
have a NonEmptyList' that is also of maximum length 100, you need to either
have a newtype to again wrap your NonEmptyList', or a newtype that expresses
both those constraints. Either way, all the functions you wrote for
NonEmptyList', and which ideally would work with NonEmptyMax100List, won't
do so (without some newtype unwrapping or coercing).
Instead, with verdict you can do this:
type NonEmptyList a = Validated (Not (Length 0)) [a]
The smart constructor comes for free as validate. Specialized for clarity:
mkNonEmpty :: [a] -> Either ErrorTree (NonEmptyList a)
mkNonEmpty = validate
The Read instance also comes for free, and checks for validity:
testRead :: NonEmptyList Int
testRead = read "[]"
testRead will throw a descriptive error message.
Writing functions that express their precise assumptions can then be done with
Implies:
safeHead :: (c `Implies` (Not (Length 0))) => Validated c [a] -> a
safeHead = head . getVal
Now, if we have another type:
type ReasonableList a = Validated (MinLength 1 :&& MaxLength 100) [a]
Our function safeHead will typecheck when given either a ReasonableList or
a NonEmptyList (or anything else with constraints that imply the length is
not zero).
The library provides some terms that can be used in the little constraint DSL.
Additionally, you may want to create your own. Doing so is as easy as declaring
an empty datatype, and a HaskVerdict instance for it. Let us for example
define a predicate InCircle cx cy r, which is true of a Point if the point
is inside a circle of radius r centered on coordinates (cx, cy):
data InCircle centerX centerY radius
data Point = Point { x :: Integer, y :: Integer } deriving (Eq, Show)
instance (KnownNat cx, KnownNat cy, KnownNat r)
=> HaskVerdict (InCircle cx cy r) Point where
haskVerdict _
= check (\p -> (x p - centerX) ^ 2 + (y p - centerY) ^ 2 < radius ^ 2) err
where centerX = natVal (Proxy :: Proxy cx)
centerY = natVal (Proxy :: Proxy cy)
radius = natVal (Proxy :: Proxy r)
err = "Point not inside circle: " <> (Text.pack $ show ((centerX, centerY), radius))
Additionally, you may also want to declare type instances for Implies' which
describe what things imply or are implied by your new constraint.
type instance Implies' (InCircle cx cy r) (InCircle cx cy r') = r <= r'
Sometimes you may not want to or are not able to change the types of records. You can still validate them:
mkUpperRightQuad :: ApplicativeError ErrorTree m
=> Integer -> Integer -> m Point
mkUpperRightQuad x' y' = Point <$> x' `checkWith` (Proxy :: Proxy (Minimum 0))
<*> y' `checkWith` (Proxy :: Proxy (Minimum 0))
If we instantiate ApplicativeError to a short-circuiting applicative (like
Either), only the first result will be returned. If we use something like
Failure, all of them will:
main :: IO ()
main = do
print (mkUpperRightQuad 5 3 :: Either ErrorTree Point)
print (mkUpperRightQuad (-2) 1 :: Either ErrorTree Point)
print (mkUpperRightQuad (-2) (- 1) :: Either ErrorTree Point)
print (mkUpperRightQuad (-2) (- 1) :: Failure ErrorTree Point)
print (mkUpperRightQuad 0 (- 1) :: Either ErrorTree Point)
print testRead
The results:
Right (Point {x = 5, y = 3})
Left (Leaf "Should be more than 0")
Left (Leaf "Should be more than 0")
Failure (And (Leaf "Should be more than 0") (Leaf "Should be more than 0"))
Left (Leaf "Should be more than 0")
tutorial: Leaf "this still needs to be figured out"