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