Joint constraint for HList elements

Suppose we have the following definition for HList:

data HL spec where HLNil :: HL () HLCons :: h -> HL t -> HL (h, t) 

Is it possible to somehow provide a joint restriction on its elements?

As an example, the following attempt is to restrict elements to Show instances that do not work with Couldn't match type `Char' with `Int' :

 class HLSpecEach spec item instance HLSpecEach () item instance (HLSpecEach t item, h ~ item) => HLSpecEach (h, t) item a :: (Show item, HLSpecEach spec item) => HL spec -> Int a = undefined b :: HL (Int, (Char, ())) b = undefined c = ab 
+6
source share
1 answer

Easy to do if you have constraint types and family types. First, let me say that I prefer to use DataKinds for clarity

 data HList ls where HNil :: HList '[] HCons :: x -> HList xs -> HList (x ': xs) type family ConstrainAll (c :: * -> Constraint) (ls :: [*]) :: Constraint type instance ConstrainAll c '[] = () type instance ConstrainAll c (x ': xs) = (cx, ConstrainAll c xs) showAll :: ConstrainAll Show xs => HList xs -> [String] showAll HNil = [] showAll (HCons x xs) = (show x) : showAll xs 

if you do not use new extensions, it is possible, but much uglier. One option is to define custom classes for everything

 class ShowAll ls where showAll :: HList ls -> [Show] instance ShowAll () where showAll _ = [] instance (ShowAll xs, Show x) => ShowAll (x,xs) showAll (HCons x xs) = (show x) : (showAll xs) 

which I find ugly. A smarter approach is to fake constraint types

 class Constrained tag aType where isConstained :: tag aType data HListT tag ls where HNilT :: HListT tag () HConsT :: x -> tag x -> HListT tag xs -> HListT tag (x,xs) data Proxy (f :: * -> *) = Proxy class ConstainedAll tag ls where tagThem :: Proxy tag -> HList ls -> HListT tag ls instance ConstainedAll tag () where tagThem _ _ = HNilT instance (ConstainedAll tag xs, Constrained tag x) => ConstainedAll tag (x,xs) where tagThem p (HCons x xs) = HConsT x isConstained (tagThem p xs) 

which can then be used as

 data Showable x where Showable :: Show x => Showable x instance Show x => Constrained Showable x where isConstained = Showable --inferred type showAll' :: HListT Showable xs -> [String] showAll' HNilT = [] showAll' (HConsT x Showable xs) = (show x) : showAll' xs --inferred type: showAll :: ConstainedAll Showable xs => HList xs -> [String] showAll xs = showAll' (tagThem (Proxy :: Proxy Showable) xs) example = showAll (HCons "hello" (HCons () HNil)) 

which should (with a health check) work with any GHC with GADT, MPTC, flexible contexts / instances, and gender signatures (you can easily get rid of the latter).

EDIT: in GHC 7.6+ you should use

 type family ConstrainAll (c :: k -> Constraint) (ls :: [k]) :: Constraint 

( k instead of * ) and enable PolyKinds, but this will not work with the GGC 7.4 PolyKinds implementation (hence the monomorphic code). Similarly, defining

 data HList f ls where HNil :: HList f '[] HCons :: !(fx) -> !(HList f xs) -> HList f (x ': xs) 

avoids code duplication when you need things like a lazy or strict HList list or when you need a dictionary list or generic type options with higher quality, etc.

+4
source

Source: https://habr.com/ru/post/943586/


All Articles