Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
- type family (expected :: (Symbol, k)) @=? (actual :: k) :: () where ...
- type family (actual :: k) @?= (expected :: (Symbol, k)) :: () where ...
- type family (msg :: Symbol) @<> (expected :: k) :: (Symbol, k) where ...
- type family (expected :: k) <>@ (msg :: Symbol) :: (Symbol, k) where ...
- type family (msg :: Symbol) @<>? (result :: Bool) :: () where ...
- type family (result :: Bool) ?<>@ (msg :: Symbol) :: () where ...
- type family AssertBool (msg :: Symbol) (condition :: Bool) :: () where ...
- type family AssertEq (msg :: Symbol) (expected :: k) (actual :: k) :: () where ...
- type family AssertEq' (msg :: Symbol) (expected :: k) (actual :: k) (result :: Bool) :: () where ...
- type family AssertAll (xs :: [()]) :: () where ...
Introduction
tao
provides type-level assertion operators/functions and only depends on
base
. The operators are influenced by the HUnit
unit testing library. Using this library should feel somewhat similar to unit testing,
but at the type-level!
The Getting Started section walks through general usage.
Getting Started
We will start with a minimal example. We want to confirm that the promoted
True
type is equal to the promoted True
type.
unitTest :: Proxy '() unitTest = Proxy :: Proxy (AssertEq "True is True" 'True 'True)
This function's type is a proxy containing promoted unit. In the body of
the function, we have annotated the Proxy
value we are constructing using
AssertEq
, and AssertEq
produces the promoted unit type. This is where
we are specifying our test. We give AssertEq
three things:
- a
Symbol
that is used as a message on assertion failure - an expected type
- the actual type
If the expected type and actual type are equal, the test passes and our code compiles! What if the types are not equal?
unitTest :: Proxy '() unitTest = Proxy :: Proxy (AssertEq "True is True" 'True 'False)
Then the compiler will tell us something is very wrong:
* True is True: expected ('True), actual ('False) * In the expression: Proxy :: Proxy (AssertEq "True is True" 'True 'False) In an equation for ‘unitTest’: unitTest = Proxy :: Proxy (AssertEq "True is True" 'True 'False)
Testing that true is true is not super useful. We could do something instead like:
unitTest :: Proxy '() unitTest = Proxy :: Proxy (AssertEq "3 = 1 + 2" 3 (1 + 2))
In the above we have specified that 3
is equal to 1 + 2
using type-level
natural numbers.
What if we want to have more than one test? We could make multiple proxies:
testAddingNats :: Proxy '() testAddingNats = Proxy :: Proxy (AssertEq "3 = 1 + 2" 3 (1 + 2)) upFromHowManyChambers :: Proxy '() upFromHowManyChambers = Proxy :: Proxy (AssertEq "36 = 6 * 6" 36 (6 * 6))
This works, but it is fairly heavy-handed. It would be nice to instead just stuff all of our assertions in a type-level list. A first attempt might look like this:
unitTests :: Proxy '[ '(), '() ] unitTests = Proxy :: Proxy '[ AssertEq "3 = 1 + 2" 3 (1 + 2) , AssertEq "36 = 6 * 6" 36 (6 * 6) ]
This is an improvement, but now we have to add a promoted unit to the
type-level list in unitTest
's type signature every time we add an assertion.
A helper called AssertAll
is provided for this case:
unitTests :: Proxy '() unitTests = Proxy :: Proxy (AssertAll '[ AssertEq "3 = 1 + 2" 3 (1 + 2) , AssertEq "36 = 6 * 6" 36 (6 * 6) ])
AssertAll
will squash down all the result units from assertions into a single
unit. This way, we can keep on adding assertions and never have to fuss with
unitTest
's type signature along the way.
So far, we have used AssertEq
in all of the above examples. tao
provides
HUnit
-like operators too:
unitTests :: Proxy '() unitTests = Proxy :: Proxy (AssertAll '[ "3 = 1 + 2" @<> 3 @=? 1 + 2 , "36 = 6 * 6" @<> 36 @=? 6 * 6 ])
In the above, we used @=?
as a rough alias for AssertEq
. We attached an
assertion message using @<>
. Using the operators can be nice when we want to
cut down on parentheses.
If we prefer to put our expected types and assertion messages to the right, we could write this equivalently as:
unitTests :: Proxy '() unitTests = Proxy :: Proxy (AssertAll '[ 1 + 2 @?= 3 <>@ "3 = 1 + 2" , 6 * 6 @?= 36 <>@ "36 = 6 * 6" ])
Woo - now we know how to use tao
! As a next step, we can take a look at
the tao-example repo to
see tao
being used to test a few slightly more complicated type-level
computations.
Assertions as type operators
type family (expected :: (Symbol, k)) @=? (actual :: k) :: () where ... infix 1 Source #
Asserts that the expected type is equal to the actual type.
Roughly an alias for AssertEq
, but as an operator.
type family (actual :: k) @?= (expected :: (Symbol, k)) :: () where ... infix 1 Source #
Asserts that the actual type is equal to the expected type.
Roughly an alias for AssertEq
, but as an operator.
type family (msg :: Symbol) @<> (expected :: k) :: (Symbol, k) where ... infix 2 Source #
Pairs an assertion message with an expected type.
m @<> e = '(m, e) |
type family (expected :: k) <>@ (msg :: Symbol) :: (Symbol, k) where ... infix 2 Source #
Pairs an assertion message with an expected type. Flipped version of
@<>
.
e <>@ m = '(m, e) |
type family (msg :: Symbol) @<>? (result :: Bool) :: () where ... infix 2 Source #
Operator version of AssertBool
.
m @<>? r = AssertBool m r |
type family (result :: Bool) ?<>@ (msg :: Symbol) :: () where ... infix 2 Source #
Flipped, operator version of AssertBool
.
r ?<>@ m = AssertBool m r |
Assertions as type functions
type family AssertBool (msg :: Symbol) (condition :: Bool) :: () where ... Source #
Asserts that the type-level condition is true. Returns unit when the
condition is true and produces a type error otherwise. The input Symbol
is a message that is displayed as part of the type error.
AssertBool m True = () | |
AssertBool m False = TypeError (Text m :<>: Text ": condition was false") |
type family AssertEq (msg :: Symbol) (expected :: k) (actual :: k) :: () where ... Source #
Asserts that the expected type is equal to the actual type. Returns unit
when the types are equal and produces a type error otherwise. The input
Symbol
is a message that is displayed as part of the type error.
type family AssertEq' (msg :: Symbol) (expected :: k) (actual :: k) (result :: Bool) :: () where ... Source #
Helper for the implementation of AssertEq
. Users should never need
to use this directly.