I am pretty sure that this doesn't exist, but it's quite interesting. I've submitted a feature request here:
http://hackage.haskell.org/trac/ghc/ticket/2101 On 2/15/08, Louis-Julien Guillemette <[EMAIL PROTECTED]> wrote: > Hi all, > > I've been using GHC's type families somewhat extensively in my > type-preserving compiler (BTW, they work great), and quite often I > come across the need to prove lemmas about those functions. As far as > I understand there's currently no way to handle such lemmas purely at > the type level, and I have to encode them as term-level functions. > > I wonder if I'm missing something, or otherwise if there are plans to > provide some way to do this kind of type-level reasoning. > > Here's a simple example. > > I encode (de Bruijn) type contexts as lists of types of this form: > > (t0, (t1, (... , ()...))) > > I sometimes concatenate type contexts, and need a lemma stating that > appending an empty context leaves it unchanged (ts ++ [] == ts). > > type family Cat ts0 ts > type instance Cat () ts' = ts' > type instance Cat (s, ts) ts' = (s, Cat ts ts') > > That is, I need to coerce: > > Exp (Cat ts ()) > > into: > > Exp ts > > The way I presently do it is through a term-level function that > produces a witness that the two types are equivalent, like this: > > data Equiv s t where > Equiv :: (s ~ t) => Equiv s t > > cat_nil :: EnvRep ts -> Equiv (Cat ts ()) ts > cat_nil R0 = Equiv > cat_nil (Rs _ ts_r) = case cat_nil ts_r of Equiv -> Equiv > > coerce :: EnvRep ts -> Exp (Cat ts ()) -> Exp ts > coerce ts_r e = case cat_nil ts_r of Equiv -> e > > > Louis > > _______________________________________________ > Haskell mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell > _______________________________________________ Haskell mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell
