> IMO, a unit that does not pass a spec/test should cause a compile time error.
We can achieve this in dependently-typed languages like Idris. First we define a datatype 'Equal x y', which will represent the proposition that expression 'x' is equal to expression 'y':
data Equal x y where
Refl : (x : _) -> Equal x x
There are two things to note:
- There is only one way to construct a value of type `Equal x y`, which is to use the constructor we've called `Refl`.
- `Refl` only takes one argument, `x` (of arbitrary type `_`), and it only constructs values of type `Equal x x`. This is called "reflexivity", thus the name `Refl`.
Hence if we use the type `Expr x y` anywhere in our program, there is only one possible value we can provide that might typecheck (`Refl x`), and that will only typecheck if `Expr x x` unifies with `Expr x y`, which will only happen if `x` and `y` are the same thing; i.e. if they are equal. Thus the name `Equal`.
This `Equal` type comes in the standard library of all dependently typed languages, and is widely used. To use it for testing we just need to write a test, e.g. `myTest`, which returns some value indicating pass/fail, e.g. a `Boolean`. Then we can add the following to our program:
This will only type-check if `Equal myTest myTest` (the type of `Refl myTest`) unifies with `Equal myTest True`, which will only be the case if `myTest` evaluates to `True`.
We can achieve this in dependently-typed languages like Idris. First we define a datatype 'Equal x y', which will represent the proposition that expression 'x' is equal to expression 'y':
There are two things to note:- There is only one way to construct a value of type `Equal x y`, which is to use the constructor we've called `Refl`.
- `Refl` only takes one argument, `x` (of arbitrary type `_`), and it only constructs values of type `Equal x x`. This is called "reflexivity", thus the name `Refl`.
Hence if we use the type `Expr x y` anywhere in our program, there is only one possible value we can provide that might typecheck (`Refl x`), and that will only typecheck if `Expr x x` unifies with `Expr x y`, which will only happen if `x` and `y` are the same thing; i.e. if they are equal. Thus the name `Equal`.
This `Equal` type comes in the standard library of all dependently typed languages, and is widely used. To use it for testing we just need to write a test, e.g. `myTest`, which returns some value indicating pass/fail, e.g. a `Boolean`. Then we can add the following to our program:
This will only type-check if `Equal myTest myTest` (the type of `Refl myTest`) unifies with `Equal myTest True`, which will only be the case if `myTest` evaluates to `True`.