[Haskell] Closed Projections on HLists?

[oleg at pobox.com]

Jared Warren wrote:
> 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.
>
> 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?

If the inference is unique, then of course, we _can_ infer that the
empty list can only be projected onto the empty list. However any
non-empty list can be projected in several ways. How do we infer this
ambiguous result? Either we have to specify which projection result we
want, and the typechecker will tell us if that is possible. Or we
obtain the powerset of a list -- and then enumerate it. The current
HProject is written with the first approach in mind:

> class HProject l l'
>  where
>   hProject :: l -> l'

As we can see, there are no functional dependencies on the class -- as
there can't be, in general. A list can, in general, be projected in
many ways (and given a projection, there can be many lists it can be
obtained from). So, we have to be explicit: which list is to project
into what.

In general, that is the best one can do, right? There is however, a
special case: the empty list. The empty list can only be projected one
way -- and, so we would like the typechecker to infer that (rather
then wait for us to supply the result and then check it). If that
behavior is desirable, it can be obtained. The key is the ability to
specify functional dependencies on a per-instance basis.

Here's the complete code

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> -- Look, Ma! No overlapping instances!
>
> module Foo where
>
> import CommonMain hiding (HDeleteMany, hDeleteMany, TypeCast, 
> 			    typeCast, HProject, hProject)
> import TypeCastGeneric2
> import TypeEqTTypeable
> import TypeEqBoolTTypeable
> import TTypeable

> class HProject l l'
>  where
>   hProject :: l -> l'
>
> instance TypeCast HNil l' => HProject HNil l' where
>   hProject _ = typeCast HNil
> instance HProject (HCons a r) HNil
>  where
>   hProject l = HNil
> instance ( HList l', HOccurs' e (HCons a r), HProject (HCons a r) l')
>       => HProject (HCons a r) (HCons e l')
>  where
>   hProject l = HCons (hOccurs' l) (hProject l)
>
> list1 = (HCons 'a' (HCons True HNil))
>
>
> test1 = hProject list1 :: HNil
> test2 = hProject list1 :: (HCons Char HNil)
> test3 = hProject list1 :: (HCons Bool HNil)
>
> -- NB: No explicit type of the result given. The typechecker _does_
> -- infer it
> test4 = hProject HNil