Tao

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

Asserts that the expected type is equal to the actual type.

Roughly an alias for AssertEq, but as an operator.

Equations

'(m, e) @=? a = AssertEq m e a

type family (actual :: k) @?= (expected :: (Symbol, k)) :: () where ... infix 1

Asserts that the actual type is equal to the expected type.

Roughly an alias for AssertEq, but as an operator.

Equations

a @?= '(m, e) = AssertEq m e a

type family (msg :: Symbol) @<> (expected :: k) :: (Symbol, k) where ... infix 2

Pairs an assertion message with an expected type.

Equations

m @<> e = '(m, e)

type family (expected :: k) <>@ (msg :: Symbol) :: (Symbol, k) where ... infix 2

Pairs an assertion message with an expected type. Flipped version of @<>.

Equations

e <>@ m = '(m, e)

type family (msg :: Symbol) @<>? (result :: Bool) :: () where ... infix 2

Operator version of AssertBool.

Equations

m @<>? r = AssertBool m r

type family (result :: Bool) ?<>@ (msg :: Symbol) :: () where ... infix 2

Flipped, operator version of AssertBool.

Equations

r ?<>@ m = AssertBool m r

Assertions as type functions

type family AssertBool (msg :: Symbol) (condition :: Bool) :: () where ...

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.

Equations

AssertBool m True = ()

AssertBool m False = TypeError (Text m :<>: Text ": condition was false")

type family AssertEq (msg :: Symbol) (expected :: k) (actual :: k) :: () where ...

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.

Equations

AssertEq m e a = AssertEq' m e a (e == a)

type family AssertEq' (msg :: Symbol) (expected :: k) (actual :: k) (result :: Bool) :: () where ...

Helper for the implementation of AssertEq. Users should never need to use this directly.

Equations

AssertEq' m _ _ True = ()

AssertEq' m e a False = TypeError (((((Text m :<>: Text ": expected (") :<>: ShowType e) :<>: Text "), actual (") :<>: ShowType a) :<>: Text ")")

Folding lists of assertions

type family AssertAll (xs :: [()]) :: () where ...

Helper function to fold a bunch of type-level units down to a single unit. This is convenient for squashing down a type-level list of assert results.

Equations

AssertAll '[] = ()

AssertAll (() ': xs) = AssertAll xs