Commit 5d5d7514 authored by Juan Pablo Garcia Garland's avatar Juan Pablo Garcia Garland
Browse files

add Require + doc

parent 2365af5f
# Revision history for Require
## 0.5.3.0 -- YYYY-mm-dd
* First version. Released on an unsuspecting world.
-- Initial Require.cabal generated by cabal init. For further
-- documentation, see http://haskell.org/cabal/users-guide/
name: Require
version: 0.6.0.0
synopsis: Abstraction to manage user defined Type Errors
-- description:
license: GPL-3
license-file: LICENSE
author: Juan García-Garland
maintainer: jpgarcia@fing.edu.uy
-- copyright:
category: Development
build-type: Simple
extra-source-files: CHANGELOG.md
cabal-version: >=1.10
library
exposed-modules: Data.Type.Require
-- other-modules:
-- other-extensions:
build-depends: base >=4.12 && <4.13
hs-source-dirs: src
default-language: Haskell2010
import Distribution.Simple
main = defaultMain
{-|
Module : Data.Type.Require
Description : A small framework to manage user defined type errors.
Copyright : (c) Juan García-Garland, Marcos Viera, 2019, 2020
License : GPLv3
Maintainer : jpgarcia@fing.edu.uy
Stability : experimental
Portability : POSIX
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 PHER library (which is again, an abstraction
synthesized from the AspectAG) are examples of how to use
'Require'. The name 'Require' comes from TODO.
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 'GHC.TypeLits'
infraestructure.
TODO
> 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"
-}
{-# 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 Data.Type.Require
where
import Data.Kind
import Data.Proxy
import GHC.TypeLits
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.
class
Require (op :: Type) (ctx :: [ErrorMessage]) where
type ReqR op :: Type
req :: Proxy ctx -> op -> ReqR op
-- | OpError operation. A 'Require' call to this operation produces a
-- type error showing the argument message.
data OpError (m :: ErrorMessage) :: Type where {}
-- | Failing and printing of an |OpError| requirement.
instance (TypeError
(Text "Error: " :<>: m :$$:
Text "trace: " :<>: ShowCTX ctx))
=>
Require (OpError m) ctx where
type ReqR (OpError m) = ()
req _ _ = error "unreachable"
-- | Formatting of context printing.
type family ShowCTX (ctx :: [ErrorMessage]) :: ErrorMessage where
ShowCTX '[] = Text ""
ShowCTX (m ': ms) = m :$$: ShowCTX ms
-- | TODO
type family ShowEM (m :: ErrorMessage) :: ErrorMessage
-- | Show for types
type family ShowT (t :: k) :: ErrorMessage
type instance ShowT (t :: Type) = ShowType t
type instance ShowT (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, t1 ~ t2)
-- Exported operators.
-- | Equality operator.
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
-- | comparisson of types, given a trivially satisfying constraint if
-- they are equal, or requiring an |OpError| otherwise.
type family RequireEqRes (t1 :: k) (t2 :: k)
(ctx :: [ErrorMessage]) :: Constraint where
RequireEqRes t1 t2 ctx = If (t1 `Equal` t2) (() :: Constraint)
(Require (OpError (Text "\n " :<>: ShowT t1 :<>: Text "\n/= " :<>: ShowT t2)) ctx)
type family Equal (a :: k) (b :: k') :: Bool where
Equal a a = True
Equal a b = False
-- | overloaded type equality
type family Equ (a :: k) (b :: k) :: Bool
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