[Haskell] Lemmas about type functions

[Ryan Ingram]

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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
>