[Haskell] Closed Projections on HLists?

[Jared Warren]

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 at 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