requirements-0.7.0.1: Abstraction to manage user defined Type Errors
Copyright(c) Juan García-Garland Marcos Viera 2019 2020
LicenseGPLv3
Maintainerjpgarcia@fing.edu.uy
Stabilityexperimental
PortabilityPOSIX
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Type.Require

Description

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"
Synopsis

Documentation

class Require (op :: Type) (ctx :: [ErrorMessage]) where Source #

Require class. Use this when a dependent type (a la Haskell) requires some type level property for a function to be defined to program nice type errors.

Associated Types

type ReqR op :: Type Source #

Methods

req :: Proxy ctx -> op -> ReqR op Source #

Instances

Instances details
(TypeError (('Text "Error: " :<>: m) :$$: ('Text "trace: " :<>: ShowCTX ctx)) :: Constraint) => Require (OpError m) ctx Source #

Failing and printing of an |OpError| requirement.

Instance details

Defined in Data.Type.Require

Associated Types

type ReqR (OpError m) Source #

Methods

req :: Proxy ctx -> OpError m -> ReqR (OpError m) Source #

data OpError (m :: ErrorMessage) :: Type Source #

OpError operation. A Require call to this operation produces a type error showing the argument message.

Instances

Instances details
(TypeError (('Text "Error: " :<>: m) :$$: ('Text "trace: " :<>: ShowCTX ctx)) :: Constraint) => Require (OpError m) ctx Source #

Failing and printing of an |OpError| requirement.

Instance details

Defined in Data.Type.Require

Associated Types

type ReqR (OpError m) Source #

Methods

req :: Proxy ctx -> OpError m -> ReqR (OpError m) Source #

type ReqR (OpError m) Source # 
Instance details

Defined in Data.Type.Require

type ReqR (OpError m) = ()

type family IsEmptyCtx (ms :: [ErrorMessage]) :: Bool where ... Source #

Equations

IsEmptyCtx '[] = True 
IsEmptyCtx (m ': ms) = False 
IsEmptyCtx _ = True 

type family IsEmptyMsg (m :: ErrorMessage) :: Bool where ... Source #

Equations

IsEmptyMsg (Text "") = True 
IsEmptyMsg (l :<>: r) = IsEmptyMsg l && IsEmptyMsg r 
IsEmptyMsg other = False 

type family ShowCTX (ctx :: k) :: ErrorMessage where ... Source #

Equations

ShowCTX ('[] :: [ErrorMessage]) = Text "" 
ShowCTX ((m :: ErrorMessage) ': (ms :: [ErrorMessage])) = m :$$: ShowCTX ms 
ShowCTX (m :: [ErrorMessage]) = Text "" 

type family FromEM (t :: ErrorMessage) :: Symbol where ... Source #

Equations

FromEM (Text t) = t 
FromEM _ = "" 

type family ShowTE (t :: k) :: ErrorMessage Source #

Show for types

Instances

Instances details
type ShowTE (t :: Type) Source # 
Instance details

Defined in Data.Type.Require

type ShowTE (t :: Type) = 'ShowType t
type ShowTE (t :: Symbol) Source # 
Instance details

Defined in Data.Type.Require

type ShowTE (t :: Symbol) = 'Text t

type RequireR (op :: Type) (ctx :: [ErrorMessage]) (res :: Type) = (Require op ctx, ReqR op ~ res) Source #

A common constraint is to have a |Requirement| to be fullfilled, and something to unify with the result of the operation.

data OpEq' (cmp :: Bool) t1 t2 Source #

type RequireEq (t1 :: k )(t2 :: k) (ctx:: [ErrorMessage]) = (Require (OpEq t1 t2) ctx ) --0, IfStuck (Equal t1 t2) (DelayError ('Text "error coso")) (NoErrorFcf))

Equality operator. data OpEq t1 t2

type RequireEq (t1 :: k) (t2 :: k) (ctx :: [ErrorMessage]) = (AssertEq t1 t2 ctx, t1 ~ t2) Source #

type family AssertEq (t1 :: k) (t2 :: k) ctx :: Constraint where ... Source #

Equations

AssertEq a a ctx = () 
AssertEq a b ctx = Require (OpError (((Text "\n " :<>: ShowTE a) :<>: Text "\n/= ") :<>: ShowTE b)) ctx 

data Exp (a :: k) where Source #

Constructors

Exp :: a -> Exp a 

type family Eval (exp :: Type) :: k Source #

Instances

Instances details
type Eval (EqMsg t1 t2) Source # 
Instance details

Defined in Data.Type.Require

type Eval (EqMsg t1 t2) = (('Text "\nEQMSG" :<>: ShowTE t1) :<>: 'Text "\n/= ") :<>: ShowTE t2

data CondEq (a :: k) (b :: k) where Source #

Constructors

CondEq :: a -> b -> CondEq a b 

data RequireEqResF (a :: k) (b :: k) where Source #

Constructors

RequireEqResF :: a -> b -> RequireEqResF a b 

data EqMsg (a :: k) (b :: k) where Source #

Constructors

EqMsg :: a -> b -> EqMsg a b 

Instances

Instances details
type Eval (EqMsg t1 t2) Source # 
Instance details

Defined in Data.Type.Require

type Eval (EqMsg t1 t2) = (('Text "\nEQMSG" :<>: ShowTE t1) :<>: 'Text "\n/= ") :<>: ShowTE t2

type family RequireEqWithMsg (t :: k) (t' :: k) (msg :: k -> k -> Type) (ctx :: [ErrorMessage]) :: Constraint Source #

Instances

Instances details
type RequireEqWithMsg (t :: k) (t' :: k) (f :: k -> k -> Type) ctx Source # 
Instance details

Defined in Data.Type.Require

type RequireEqWithMsg (t :: k) (t' :: k) (f :: k -> k -> Type) ctx = (AssertEq' t t' f ctx, t ~ t')

type family AssertEq' (t1 :: k) (t2 :: k) (f :: k -> k -> Type) ctx :: Constraint where ... Source #

Equations

AssertEq' a a f ctx = () 
AssertEq' a b f ctx = Require (OpError (Eval (f a b))) ctx 

data OpEq t1 t2 Source #

Equality operator.

type family RequireEqRes (t1 :: k) (t2 :: k) (ctx :: [ErrorMessage]) :: Constraint where ... Source #

implementation of Require instance for equality (the type family in the context implements the logic) instance RequireEqRes t1 t2 ctx => Require (OpEq t1 t2) ctx where type ReqR (OpEq t1 t2) = () req = undefined

comparisson of types, given a trivially satisfying constraint if they are equal, or requiring an |OpError| otherwise.

Equations

RequireEqRes t1 t2 ctx = If (t1 `Equal` t2) (() :: Constraint) (Require (OpError (((Text "\n " :<>: ShowTE t1) :<>: Text "\n/= ") :<>: ShowTE t2)) ctx) 

type family Equal (a :: k) (b :: k') :: Bool where ... Source #

Equations

Equal a a = True 
Equal a b = False 

type family Equ (a :: k) (b :: k) :: Bool Source #

overloaded type equality

appendCtx :: Proxy ctx -> Proxy ctx' -> Proxy (ctx :++ ctx') Source #

type family xs :++ ys where ... Source #

Equations

'[] :++ ys = ys 
(x ': xs) :++ ys = x ': (xs :++ ys)