Commit 4f081c74 authored by Juan Pablo Garcia Garland's avatar Juan Pablo Garcia Garland
Browse files

agrega mensajes

parent 507edea0
......@@ -136,6 +136,8 @@ import Data.Proxy
import GHC.TypeLits
import Data.Type.Bool
import Data.Type.Equality
--import Type.Errors
-- | Require class. Use this when a /dependent type/ (/a la/ Haskell)
-- /requires/ some type level property for a function to be defined to
......@@ -165,6 +167,7 @@ instance (TypeError
type family IsEmptyCtx (ms :: [ErrorMessage]) :: Bool where
IsEmptyCtx '[] = True
IsEmptyCtx (m ': ms) = IsEmptyMsg m && IsEmptyCtx ms
IsEmptyCtx _ = True
type family IsEmptyMsg (m :: ErrorMessage) :: Bool where
IsEmptyMsg (Text "") = True
......@@ -172,28 +175,77 @@ type family IsEmptyMsg (m :: ErrorMessage) :: Bool where
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 instance ShowCTX (a :: Type) = 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 RequireCondWithMsg (t :: k) (msg :: k') (ctx :: [ErrorMessage])
--type instance RequireCondWithMsg (CondEq a b) (RequireEqRes)
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.
......@@ -202,10 +254,10 @@ data OpEq t1 t2
-- | 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.
......
> {-# LANGUAGE FlexibleContexts #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE TypeApplications #-}
> {-# 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..
> {-# 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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment