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 <guillelj@iro.umontreal.ca> 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 Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell