public
Last active

Introducing type variables in class constraint, using ConstraintKinds.

  • Download Gist
ConstraintCategory.hs
Haskell
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 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
-- * 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'

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.