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