requirements 0.6.0.0 → 0.7.0.0
raw patch · 4 files changed
+375/−21 lines, 4 filesdep ~base
Dependency ranges changed: base
Files
- requirements.cabal +10/−7
- src/Data/Type/Require.hs +68/−14
- src/Figures.lhs +147/−0
- src/Vector.lhs +150/−0
requirements.cabal view
@@ -2,24 +2,27 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: requirements-version: 0.6.0.0+version: 0.7.0.0 synopsis: Abstraction to manage user defined Type Errors-description: Require framework, 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+ domain-specific error into a curried data type, the operator.+ The Require constraint predicates over operators. Ill-formed+ operators require the Error operator. license: GPL-3 license-file: LICENSE author: Juan García-Garland maintainer: jpgarcia@fing.edu.uy-copyright: 2019, 2020 Juan García-Garland, Marcos Viera +-- copyright: category: Development build-type: Simple extra-source-files: CHANGELOG.md---source-repository: https://gitlab.fing.edu.uy/aspectag/require cabal-version: >=1.10 library- exposed-modules: Data.Type.Require- -- other-modules:+ exposed-modules: Data.Type.Require+ other-modules: Figures, Vector -- other-extensions:- build-depends: base >=4.11.0 && < 4.15+ build-depends: base >=4.12 && <4.17 hs-source-dirs: src default-language: Haskell2010
src/Data/Type/Require.hs view
@@ -137,6 +137,7 @@ import Data.Type.Bool import Data.Type.Equality + -- | 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.@@ -154,8 +155,6 @@ -- | Failing and printing of an |OpError| requirement. instance (TypeError (Text "Error: " :<>: m :$$:- If (IsEmptyCtx ctx)- (Text "") (Text "trace: " :<>: ShowCTX ctx))) => Require (OpError m) ctx where@@ -164,7 +163,8 @@ type family IsEmptyCtx (ms :: [ErrorMessage]) :: Bool where IsEmptyCtx '[] = True- IsEmptyCtx (m ': ms) = IsEmptyMsg m && IsEmptyCtx ms+ IsEmptyCtx (m ': ms) = False -- IsEmptyMsg m && IsEmptyCtx ms+ IsEmptyCtx _ = True type family IsEmptyMsg (m :: ErrorMessage) :: Bool where IsEmptyMsg (Text "") = True@@ -172,29 +172,75 @@ IsEmptyMsg other = False -- -- | Formatting of context printing.-type family ShowCTX (ctx :: [ErrorMessage]) :: ErrorMessage where- ShowCTX '[] = Text ""- ShowCTX (m ': ms) = m :$$: ShowCTX ms- +type family ShowCTX (ctx :: k) :: ErrorMessage where+ ShowCTX ('[] :: [ErrorMessage]) = Text ""+ ShowCTX ((m :: ErrorMessage) ': (ms :: [ErrorMessage])) = m :$$: ShowCTX ms+ ShowCTX (m :: [ErrorMessage]) = Text ""+ -type family FromText (t :: ErrorMessage) :: Symbol where- FromText (Text t) = t+type family FromEM (t :: ErrorMessage) :: Symbol where+ FromEM (Text t) = t+ FromEM _ = "" -- | Show for types type family ShowTE (t :: k) :: ErrorMessage type instance ShowTE (t :: Type) = ShowType t type instance ShowTE (t :: Symbol) = Text t + -- | A common constraint is to have a |Requirement| to be fullfilled, -- and something to unify with the result of the operation. type RequireR (op :: Type) (ctx:: [ErrorMessage]) (res :: Type) = (Require op ctx, ReqR op ~ res) -- | +--type RequireEq (t1 :: k )(t2 :: k) (ctx:: [ErrorMessage])+-- = (Require (OpEq t1 t2) ctx ) --0,+ -- IfStuck (Equal t1 t2) (DelayError ('Text "error coso")) (NoErrorFcf))+++-- Exported operators.++-- | Equality operator.+--data OpEq t1 t2++data OpEq' (cmp :: Bool) t1 t2+ type RequireEq (t1 :: k )(t2 :: k) (ctx:: [ErrorMessage])- = (Require (OpEq t1 t2) ctx, t1 ~ t2)+ = (AssertEq t1 t2 ctx , t1 ~ t2) +type family AssertEq (t1 :: k)(t2 :: k) ctx :: Constraint where+ AssertEq a a ctx = ()+ AssertEq a b ctx = Require (OpError (Text "\n " :<>: ShowTE a+ :<>: Text "\n/= " :<>: ShowTE b)) ctx +++data Exp (a :: k) where Exp :: a -> Exp a+type family Eval (exp :: Type) :: k++data CondEq (a ::k) (b :: k) where+ CondEq :: a -> b -> CondEq a b+data RequireEqResF (a ::k) (b :: k) where+ RequireEqResF :: a -> b -> RequireEqResF a b++data EqMsg (a::k)(b::k) where EqMsg :: a -> b -> EqMsg a b+type instance 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+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+ where+ AssertEq' a a f ctx = ()+ AssertEq' a b f ctx = Require (OpError (Eval (f a b))+ ) ctx+ -- Exported operators. -- | Equality operator.@@ -202,10 +248,10 @@ -- | 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+--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.@@ -223,3 +269,11 @@ type family Equ (a :: k) (b :: k) :: Bool emptyCtx = Proxy :: Proxy '[ Text ""]++appendCtx :: Proxy ctx -> Proxy ctx' -> Proxy (ctx :++ ctx')+appendCtx Proxy Proxy = Proxy+++type family (:++) xs ys where+ '[] :++ ys = ys+ (x ': xs) :++ ys = x ': (xs :++ ys)
+ src/Figures.lhs view
@@ -0,0 +1,147 @@+> {-# LANGUAGE FlexibleContexts #-}+> {-# LANGUAGE DataKinds #-}+> {-# LANGUAGE TypeOperators #-}+> {-# LANGUAGE FlexibleInstances #-}+> {-# LANGUAGE GADTs #-}+> {-# LANGUAGE UndecidableInstances #-}+> {-# LANGUAGE TypeFamilies #-}+> {-# LANGUAGE MultiParamTypeClasses #-}+> {-# LANGUAGE TypeApplications #-}+> {-# LANGUAGE ScopedTypeVariables #-}+> {-# LANGUAGE AllowAmbiguousTypes #-} -- this is for the colour c++> 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+++> g = combine'' (tr $ tr f) (tr $ tr f'') -- (tr $ tr $ tr $ combine'' f f) f''
+ src/Vector.lhs view
@@ -0,0 +1,150 @@++> {-# 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