c980a2db73138f5b53e276e83867d3066ea8cc82
[ghc.git] / libraries / base / tests / CatEntail.hs
1 {-# LANGUAGE ConstraintKinds, GADTs, RankNTypes #-}
2 {-# LANGUAGE TypeOperators, KindSignatures #-}
3 module CatEntail where
4 import Prelude hiding (id, (.))
5 import GHC.Exts (Constraint)
6 import Control.Category
7
8 -- One dictionary to rule them all.
9 data Dict :: Constraint -> * where
10 Dict :: ctx => Dict ctx
11
12 -- Entailment.
13 -- Note the kind 'Constraint -> Constraint -> *'
14 newtype (|-) a b = Sub (a => Dict b)
15
16 (\\) :: a => (b => r) -> (a |- b) -> r
17 r \\ Sub Dict = r
18
19 reflexive :: a |- a
20 reflexive = Sub Dict
21
22 transitive :: (b |- c) -> (a |- b) -> a |- c
23 transitive f g = Sub $ Dict \\ f \\ g
24
25 instance Category (|-) where
26 id = reflexive
27 (.) = transitive