Skip to content

@sebastiaanvisser /ConstraintCategory.hs
Last active

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Introducing type variables in class constraint, using ConstraintKinds.
-- * Introducing type variables in class constraint, using ConstraintKinds.
-- * (Using ghc-7.6.3)
{-# LANGUAGE ConstraintKinds, GADTs, TypeFamilies #-}
module ConstraintCategory where
import GHC.Exts (Constraint)
-- Version of Category that can put constraints on the i/o of the category.
class Category cat where
type C cat a b c :: Constraint
cid :: C cat a b c => cat a a
(!) :: C cat a b c
=> cat b c
-> cat a b
-> cat a c
-- Two functions combined in a single data type, all variables nicely curried.
data Curried g i f o = Curried (g -> i) (f -> o)
-- A `Curried` packed into a GADT, now the type variables are nicely packed
-- pairwise which *might* allow us to write a constraint `Category` instance
-- for it.
data Uncurried f o where
Uncurried :: Curried g i f o -> Uncurried (f, g) (o, i)
-- Writing a composition function for `Uncurried` is easy by unpacking,
-- composing the functions, and packing again.
compose
:: Uncurried (p, j) (o, i)
-> Uncurried (f, g) (p, j)
-> Uncurried (f, g) (o, i)
compose (Uncurried (Curried f g))
(Uncurried (Curried h i))
= Uncurried (Curried (f . h) (g . i))
-- But NOW... I want to be able to make the `Uncurried` an instance of the
-- constraint Category type class above. Is it possible to give a proper
-- constraint `C` for it? I'm not able to.
-- Unfortunately, this won't type check:
instance Category Uncurried where
type C Uncurried a b c = ( a ~ (f, g)
, b ~ (p, j)
, c ~ (o, i)
)
cid = undefined
(!) = compose
-- Because I cannot just introduce new type variables in the constraint:
-- ConstraintCategory.hs:47:35: Not in scope: type variable `f'
-- ConstraintCategory.hs:47:38: Not in scope: type variable `g'
-- ConstraintCategory.hs:48:35: Not in scope: type variable `p'
-- ConstraintCategory.hs:48:38: Not in scope: type variable `j'
-- ConstraintCategory.hs:49:35: Not in scope: type variable `o'
-- ConstraintCategory.hs:49:38: Not in scope: type variable `i'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.