[Haskell] Closed Projections on HLists?

18 Nov 2004

      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 <warren@cs.queensu.ca>
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