requirements 0.7.0.1 → 0.7.0.2

raw patch · 4 files changed

+28/−319 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• requirements.cabal +16/−3
• src/Data/Type/Require.hs +12/−15
• src/Figures.lhs +0/−151
• src/Vector.lhs +0/−150

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                requirements-version:             0.7.0.1+version:             0.7.0.2 synopsis:            Abstraction to manage user defined Type Errors description:         requirements is a framework to build user-defined type errors.                      Users condense the arguments of functions that can raise a@@ -21,8 +21,21 @@  library   exposed-modules:     Data.Type.Require-  other-modules:       Figures, Vector-  -- other-extensions:+  --other-modules:       Figures, Vector+  other-extensions:  UndecidableInstances  +                  ,  MultiParamTypeClasses +                  ,  FlexibleContexts      +                  ,  ConstraintKinds       +                  ,  FlexibleInstances     +                  ,  TypeOperators         +                  ,  TypeFamilies          +                  ,  DataKinds             +                  ,  PolyKinds             +                  ,  KindSignatures        +                  ,  GADTs                 +                  ,  TypeApplications      +                  ,  ScopedTypeVariables   +   build-depends:       base >=4.12 && <4.18   hs-source-dirs:      src   default-language:    Haskell2010

@@ -163,8 +163,7 @@  type family IsEmptyCtx (ms :: [ErrorMessage]) :: Bool where   IsEmptyCtx '[] = True-  IsEmptyCtx (m ': ms) = False -- IsEmptyMsg m && IsEmptyCtx ms-  IsEmptyCtx _ = True+  IsEmptyCtx (m ': ms) = False  type family IsEmptyMsg (m :: ErrorMessage) :: Bool where   IsEmptyMsg (Text "") = True@@ -172,9 +171,9 @@   IsEmptyMsg other = False  -- -- | Formatting of context printing.-type family ShowCTX (ctx :: k)  :: ErrorMessage where-  ShowCTX ('[] :: [ErrorMessage]) = Text ""-  ShowCTX ((m :: ErrorMessage) ': (ms :: [ErrorMessage])) = m :$$: ShowCTX ms+type family ShowCTX (ctx :: [ErrorMessage])  :: ErrorMessage where+  ShowCTX ((m :: ErrorMessage) ': (ms :: [ErrorMessage]))+    = m :$$: ShowCTX ms   ShowCTX (m :: [ErrorMessage]) = Text ""    @@ -216,15 +215,15 @@   -data Exp (a :: k) where Exp :: a -> Exp a+data Exp (a :: Type) where Exp :: a -> Exp a type family Eval (exp :: Type) :: k -data CondEq (a ::k) (b :: k) where+data CondEq (a ::Type) (b :: Type) where   CondEq :: a -> b -> CondEq a b-data RequireEqResF (a ::k) (b :: k) where+data RequireEqResF (a :: Type) (b :: Type) where   RequireEqResF :: a -> b -> RequireEqResF a b -data EqMsg (a::k)(b::k) where EqMsg :: a -> b -> EqMsg a b+data EqMsg (a::Type)(b::Type) where EqMsg :: a -> b -> EqMsg a b type instance Eval (EqMsg t1 t2) =     (Text "\nEQMSG" :<>: ShowTE t1                        :<>: Text "\n/= " :<>: ShowTE t2)@@ -234,12 +233,11 @@   (ctx :: [ErrorMessage]) :: Constraint type instance RequireEqWithMsg t t' f ctx =   (AssertEq' t t' f ctx, t ~ t')-   --If (t `Equal` t') (()::Constraint) (Require (OpError (Eval (f t t'))) ctx))-type family AssertEq' (t1 :: k)(t2 :: k) (f :: k -> k -> Type) ctx :: Constraint+type family AssertEq' (t1 :: k)(t2 :: k)+                      (f :: k -> k -> Type) ctx :: Constraint   where   AssertEq' a a f ctx = ()-  AssertEq' a b f ctx = Require (OpError (Eval (f a b))-                                ) ctx+  AssertEq' a b f ctx = Require (OpError (Eval (f a b))) ctx  -- Exported operators. @@ -261,7 +259,7 @@     (Require (OpError (Text "\n   " :<>: ShowTE t1                        :<>: Text "\n/= " :<>: ShowTE t2)) ctx) -type family Equal (a :: k) (b :: k') :: Bool where+type family Equal (a :: k) (b :: k) :: Bool where   Equal a a = True   Equal a b = False @@ -272,7 +270,6 @@  appendCtx :: Proxy ctx -> Proxy ctx' -> Proxy (ctx :++ ctx') appendCtx Proxy Proxy = Proxy-  type family (:++) xs ys where   '[] :++ ys = ys

@@ -1,151 +0,0 @@-> {-# LANGUAGE FlexibleContexts #-}-> {-# LANGUAGE DataKinds #-}-> {-# LANGUAGE TypeOperators #-}-> {-# LANGUAGE FlexibleInstances #-}-> {-# LANGUAGE GADTs #-}-> {-# LANGUAGE UndecidableInstances #-}-> {-# LANGUAGE TypeFamilies #-}-> {-# LANGUAGE MultiParamTypeClasses #-}-> {-# LANGUAGE TypeApplications #-}-> {-# LANGUAGE ScopedTypeVariables #-}-> {-# LANGUAGE AllowAmbiguousTypes #-}-> {-# OPTIONS -Wno-missing-methods #-}--> module Figures where--> import Data.Type.Require-> import GHC.TypeLits-> import Data.Type.Bool-> import Data.Type.Equality-> import Data.Proxy--> data Color = RGB Nat Nat Nat--> type instance Equ (RGB r g b) (RGB r' g' b')->   = r == r' && g == g' && b == b'--> data Dim = R2 | R3-> type instance ShowTE R2 = Text "R2"-> type instance ShowTE R3 = Text "R3"--> data family Figure (d :: Dim) (c :: Color)---> data instance Figure R2 c->   = Circle Double Double Double -- center, radius? not important--> data instance Figure R3 c->   = Sphere Double Double Double Double---> combine :: Figure d c -> Figure d c -> Figure d c-> combine f g = undefined--combine (Circle 1 1 1) (Sphere 1 1 1 1) ->--• Couldn't match type ‘'R3’ with ‘'R2’-  Expected type: Figure 'R2 c-  Actual type: Figure 'R3 c---> data OpEqDim  (d :: Dim)  (d' :: Dim)-> data OpEqDim' (b :: Bool) (d :: Dim)   (d' :: Dim)-> data OpEqCol  (c :: Color) (c' :: Color)-> data OpEqCol' (b :: Bool) (c :: Color) (c' :: Color)--> data OpCombine d d' c c' where->   OpCombine :: Figure d c -> Figure d' c' -> OpCombine d d' c c'--> instance->   ( Require (OpEqDim d d') ctx->   , Require (OpEqCol c c') ctx->   )->   =>->   Require (OpCombine d d' c c') ctx where->   type ReqR (OpCombine d d' c c') =->     Figure d c->   req ctx (OpCombine f g) =->     undefined--> instance->   (Require (OpEqDim' (d == d') d d')) ctx->   =>->   Require (OpEqDim d d') ctx where->   type ReqR (OpEqDim d d') = ReqR (OpEqDim' (d == d') d d')--> instance Require (OpEqDim' 'True  d d') ctx where {}--> instance->   Require (OpError->   (Text "Dimensional error:" :$$: Text "cannot combine figure of dimension "->   :<>: ShowTE d :<>: Text " and dimension " :<>: ShowTE d')) ctx->   => Require (OpEqDim' 'False d d') ctx---> instance->   (Require (OpEqCol' (Equ c c') c c')) ctx->   =>->   Require (OpEqCol c c') ctx where->   type ReqR (OpEqCol c c') = ReqR (OpEqCol' (Equ c c') c c')--> instance Require (OpEqCol' 'True  c c') ctx where {}---an sloppy error:--> instance->   Require (OpError->   (Text "Error, combined images must be of the same color")) ctx->   => Require (OpEqCol' 'False c c') ctx---> combine' f f' = req (Proxy @( '[ Text "combining"] )) (OpCombine f f')--combine' (Circle 1 1 1) (Sphere 1 1 1 1) ->--• Error: Dimensional error:-         cannot combine figure of dimension R2 and dimension R3-  trace: combining..----combine' (Circle 1 1 1 :: Figure R2 (RGB 1 1 1))-         (Circle 1 1 1 :: Figure R2 (RGB 1 1 2)) ->--• Error: Error, combined images must be of the same color-  trace: combining..--> f1 = (Circle 2 2 2 :: Figure R2 (RGB 1 1 1))-> f2 = (Sphere 2 2 2 2:: Figure R3 (RGB 1 1 1))--> f = CFigure $ \Proxy  -> f1-> f' = CFigure $ \Proxy -> f2--> f'' = traceFig->    (\(_ :: Proxy (Text "tracefig!!!!!" : ctx)) -> Proxy :: Proxy ctx ) $ f'--> tr = traceFig->    (\(_ :: Proxy (ctx)) -> Proxy :: Proxy (Text "tracefig!!!!!" : ctx) )--> data CFigure d c (ctx :: [ErrorMessage])->  = CFigure {mkCFig :: Proxy ctx -> Figure d c}---> combine''->   :: (Require (OpEqDim' (d == d') d d') (Text "lalo" :ctx),->       Require (OpEqCol' (Equ c c') c c') (Text "lalo" : ctx)) =>->      CFigure d c ctx -> CFigure d' c' ctx -> CFigure d c ctx-> combine'' (CFigure f1) (CFigure f2)->   = CFigure $ \(a :: Proxy ctx) ->->           req (Proxy :: Proxy (Text "lalo" : ctx))->               (OpCombine (f1 a) (f2 a))---> traceFig :: (Proxy ctx' -> Proxy ctx) -> CFigure d c ctx -> CFigure d c ctx'-> traceFig fctx (CFigure f) = CFigure $ f . fctx----Error:-- > g = combine'' (tr $ tr f) (tr $ tr f'') -- (tr $ tr $ tr $ combine'' f f) f''

@@ -1,150 +0,0 @@--> {-# LANGUAGE UndecidableInstances  #-}-> {-# LANGUAGE MultiParamTypeClasses #-}-> {-# LANGUAGE FlexibleContexts      #-}-> {-# LANGUAGE ConstraintKinds       #-}-> {-# LANGUAGE FlexibleInstances     #-}-> {-# LANGUAGE TypeOperators         #-}-> {-# LANGUAGE TypeFamilies          #-}-> {-# LANGUAGE DataKinds             #-}-> {-# LANGUAGE PolyKinds             #-}-> {-# LANGUAGE KindSignatures        #-}-> {-# LANGUAGE GADTs                 #-}-> {-# LANGUAGE TypeApplications      #-}-> {-# LANGUAGE ScopedTypeVariables   #-}--> module Vector where--> import Data.Kind-> import Data.Proxy-> import GHC.TypeLits (Symbol, ErrorMessage(..))--> import Data.Type.Bool-> import Data.Type.Equality-> import Data.Type.Require--Firstly, we define size-indexed vectors, the stapple example of a-dependent Haskell type.--> data Nat = Z | S Nat-> type family Lt (m :: Nat) (n :: Nat) :: Bool where->   Lt Z     (S n) = True->   Lt _      Z    = False->   Lt (S m) (S n) = Lt m n--> infixr 3 :< --> data Vec (n :: Nat) (a :: Type) :: Type where->   VNil :: Vec Z a->   (:<) :: a -> Vec n a -> Vec (S n) a--And singletons for natutals:--> data SNat (n :: Nat) where->   SZ :: SNat Z->   SS :: SNat n -> SNat (S 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 '(Lt n 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' (Lt n k) n k a) ctx->   =>->   Require (OpGet n k a) ctx where->   type ReqR (OpGet n k a) =->     ReqR (OpGet' (Lt n k) n k a)->   req proxy (OpGet (n :: SNat n) (v :: Vec k a)) =->     req proxy (OpGet' (Proxy @ (Lt n k)) n v)--Now we program the good cases:--> instance->   Require (OpGet' 'True Z k a) ctx where->   type ReqR (OpGet' 'True Z k a) = a->   req _ (OpGet' _ SZ (a :< _)) = a--> instance->   Require (OpGet n k a) ctx->   => ->   Require (OpGet' 'True (S n) (S k) a) ctx where->   type ReqR (OpGet' 'True (S n) (S k) a) =->     ReqR (OpGet n k a)->   req ctx (OpGet' _ (SS n) (_ :< as)) = req ctx (OpGet n as)- --Finally, when (Lt n 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 'GHC.TypeLits'-infraestructure.---> instance->   Require (OpError->     (Text "Type error!, index out of bound:" :$$:->     Text "Trying to lookup the " :<>: ShowTE n :<>: Text "th index" :$$:->     Text "in a vector of size " :<>: ShowTE k->     )->           ) ctx->   =>->   Require (OpGet' False n k a) ctx where->   type ReqR (OpGet' False n k a) = OpError (Text "lala")->   req = error "unreachable"--> get n v = req (Proxy @ '[Text "getting"]) (OpGet n v)---> vecEx = 'a' :< 'b' :< 'c' :< 'd' :< VNil-> a = get SZ vecEx-> c = get (SS $ SS SZ) vecEx--< e = get (SS $ SS $ SS $ SS SZ) vecEx----> -  • Error: Type error!, index out of bound:-           Trying to lookup the ShowTE ('S ('S ('S ('S 'Z))))th index-           in a vector of size ShowTE ('S ('S ('S ('S 'Z))))-    trace: getting