Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
An example of an 'Indexed Arrow' typeclass, based on answers to https://stackoverflow.com/questions/56001863/how-to-work-with-types-that-change-under-composition
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, PolyKinds, GADTs #-}
module Example where
import qualified Control.Arrow
import qualified Prelude
import Prelude hiding (id, (.))
import qualified Control.Category
-- | Example type: A Qfun is a function with a Quality: Either 'Good' or 'Bad'.
newtype Qfun (q :: Quality) a b = UnsafeMkQfun { applyQfun :: a -> b }
data Quality = Good | Bad
-- | The composition of a Qfun is only Good if both of its components are Good.
type family ComposeQuality (q1 :: Quality) (q2 :: Quality) :: Quality where
ComposeQuality 'Good 'Good = 'Good
ComposeQuality _ _ = 'Bad
-- | Behaves to `Control.Category` but has an extra `index` kind parameter,
-- | whose type-value might change under composition.
class IndexedCategory (ic :: index -> * -> * -> *) where
type ComposeIndexes (index1 :: index) (index2 :: index) :: index -- ^ The resulting type under composition
id :: ic (index' :: index) a a
(.) :: ic i1 b c -> ic i2 a b -> ic (ComposeIndexes i1 i2) a c
(>>>) :: IndexedCategory ic => ic i1 a b -> ic i2 b c -> ic (ComposeIndexes i2 i1) a c
a >>> b = b . a
class (IndexedCategory ic) => IndexedArrow ic where
type DefaultIndex ic :: index
arr :: (index ~ DefaultIndex ic) => (a -> b) -> ic index a b
first :: ic index b c -> ic index (b, d) (c, d)
-- | Wrapper to lift normal categories to 'indexed' categories.
-- | We use the singleton kind `()` as 'index'.
newtype FreeIndexed (c :: * -> * -> *) (single :: ()) a b = FreeIndexed { getCat :: c a b }
instance Control.Category.Category c => IndexedCategory (FreeIndexed c) where
type ComposeIndexes a b = '()
id = FreeIndexed Control.Category.id
(FreeIndexed a) . (FreeIndexed b) = FreeIndexed (a Control.Category.. b)
instance Control.Arrow.Arrow c => IndexedArrow (FreeIndexed c) where
type DefaultIndex (FreeIndexed c) = '()
arr fun = FreeIndexed (Control.Arrow.arr fun)
first (FreeIndexed cat) = FreeIndexed (Control.Arrow.first cat)
instance IndexedCategory Qfun where
type ComposeIndexes q1 q2 = ComposeQuality q1 q2
id = UnsafeMkQfun Prelude.id
(UnsafeMkQfun f) . (UnsafeMkQfun g) = UnsafeMkQfun (f Prelude.. g)
instance IndexedArrow Qfun where
type DefaultIndex Qfun = 'Bad
arr = UnsafeMkQfun
first (UnsafeMkQfun fun) = UnsafeMkQfun (Control.Arrow.first fun)
inc :: Num a => Qfun 'Good a a
inc = UnsafeMkQfun (+1)
dec :: Num a => Qfun 'Bad a a
dec = arr (\x -> x - 1)
-- | The commented type signature will make the code not compile:
-- incDecComposition :: Num a => Qfun 'Good a a
incDecComposition :: Num a => Qfun 'Bad a a
incDecComposition = inc >>> dec
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment