I'm doing some work with heterogeneous sets as provided by the HList library <http://homepages.cwi.nl/~ralf/HList/>. My code uses projections of sets internally and I keep running into the open-world assumption when I ask the type checker to infer the result of projections. For example (in ghci):
*> hProject hNil No instance for (HProject HNil l') ...When obviously the only valid projection from the empty set is the empty set. Here is how HProject is currently implemented in HOccurs.hs: > class HProject l l' > where > hProject :: l -> l' > instance HProject l HNil > where > hProject l = HNil > instance ( HList l', HOccurs e l, HProject l l') > => HProject l (HCons e l') > where > hProject l = HCons (hOccurs l) (hProject l) The constraints on the non-trivial case seem to already use closed type classes; eg: *> hProject hNil :: HCons HNil HNil No instance for (Fail (TypeNotFound HNil)) My attempts to rewrite hProject to use the Fail class explicitly don't solve the problem. The best I have done is replace projections by membership in the powerset (implementation at the end of this message in case anybody's interested), but that just reduces the problem to trying to close HLookupByHNat when I try and get the appropriate subset out of the powerset. So what I'm wondering: is it possible to rewrite HProject in such a way as to allow the type checker to infer that the only possible projections from a list are its (non-proper) sublists? Jared Warren <[EMAIL PROTECTED]> School of Computing, Queen's University ----- An Implementation of Power Sets on Heterogeneous Lists By the algorithm from http://www.haskell.org/pipermail/haskell-cafe/2003-June/004465.html: > class HPowerSet xs yss | xs -> yss where > hPowerSet :: xs -> yss > > instance HPowerSet HNil (HCons HNil HNil) > where > hPowerSet _ = hCons hNil hNil > > instance (HPowerSet xs yss, > HMapConst (HPrepend x) yss zss, > HAppend yss zss wss) > => HPowerSet (HCons x xs) wss > where > hPowerSet (HCons x xs) = let yss = hPowerSet xs > in hAppend yss (hMap (HPrepend x) yss) Partially-applied hCons: > data HPrepend x = HPrepend x > instance HList ys => Apply (HPrepend x) ys (HCons x ys) > where > apply (HPrepend x) = hCons x An alias for hMap's constraint: > class HFoldr (HMap f) HNil xs ys => HMapConst f xs ys | f xs -> ys > instance HFoldr (HMap f) HNil xs ys => HMapConst f xs ys _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell