This module implements a simple framework to manage Type Errors when doing type-level progamming in Haskell.

• General Description:

This was originally developed for the AspectAG library (attribute grammars in the form of an EDSL). Both in AspectAG and in our Record library (which is again, an abstraction synthesized from the AspectAG) are examples of how to use Require. Some simpler examples are presented in Example modules in this package.

Let us inline one in this documentation file:

Firstly, we define size-indexed vectors, the stapple example of a dependent Haskell type.

data Vec (n :: Nat) (a :: Type) :: Type where
  VNil :: Vec 0 a
  (:<) :: a -> Vec n a -> Vec (1 + n) a

And singletons for natutals:

data SNat (n :: Nat) where
  SZ :: SNat 0
  SS :: SNat n -> SNat (1 + n)

With this we can implement a get function, that takes the element in a given index of the vector. There are many ways to do that in a safe way:

• use a value of type 'Fin n' as the input for the index.

get :: Fin n -> Vec n a -> a

• use SNat but also define a GADT 'Lt :: Nat -> Nat -> Type' that encodes a proof that the index is smaller than the vector size.

get :: SNat n -> Lt n m -> Vec m a -> a

• use a SNat, with no proof argument, and let index overflows to be ill-typed. Since this is Haskell all type information is static, meaning that we will know at compile time if the index is out of bound.

get :: SNat n -> Vec m a -> a

In the latter approach is where |Require| fits. The require infrastructure allows us to have nice type errors when an out of bound lookup occurs, instead of something like 'no instance for ..'

We introduce an operation for the vector, the get operation. This is a product datatype having all information we need: an index and vector:

data OpGet (n :: Nat) (k :: Nat) (a :: Type) :: Type  where
   OpGet :: SNat n -> Vec k a -> OpGet n k a

This operation requires some properties about its arguments, in this case, that the index given is less than vector's length. A well-typed lookup will satisfy the constraint 'Require (OpGet n k a)'

We will decide according on the result of '(<=? (n + 1) k)' . Since typeclass resolution does not backtrack we need to have all informartion on the head of the instance. This is a well known trick. We build a wrapper where the first Boolean argument will contain the result of the comparisson:

data OpGet' (cmp :: Bool) (n :: Nat) (k :: Nat) (a :: Type) :: Type where
   OpGet' :: Proxy cmp -> SNat n -> Vec k a -> OpGet' cmp n k a

Then, the wrapper instance:

instance
  Require (OpGet' ((n + 1) <=? k) n k a) ctx
  =>
  Require (OpGet n k a) ctx where
  type ReqR (OpGet n k a) =
    ReqR (OpGet' (n + 1 <=? k) n k a)
  req proxy (OpGet (n :: SNat n) (v :: Vec k a)) =
    req proxy (OpGet' (Proxy @ (n + 1 <=? k)) n v)

Now we program the good cases, we show only the base case, the recursive case is an excercise for the reader:

instance
  Require (OpGet' 'True 0 k a) ctx where
  type ReqR (OpGet' 'True 0 k a) = a
  req _ (OpGet' _ SZ (a :< _)) = a

Finally, when (n + 1 <=? k ~ 'False) we have an ill-typed get operation. We build a |Require| instance for the |OpError| operation. When defining it, we have in scope n, k, and a, everything needed to write a good type error using TypeLits infraestructure.

instance
  Require (OpError (Text "Type error!" index out of bound")) ctx
  =>
  Require (OpGet' False n k a) ctx where
  type ReqR (OpGet' False n k a) = OpError (Text "lala")
  req = error "unreachable"