[moved to haskell-cafe] Hmm, there's a problem here. Since type functions are open, it's not actually true that (forall ts. Cat ts () = ts), because someone could add, for example type instance Cat [a] () = [(a,a)] which makes the lemma no longer true. What you are doing in cat_nil is not proving that Cat ts () = ts, but rather that the form of ts is a particular form which makes that theorem hold, in particular, for all types ts of the form ts = (t1, (t2, ..., (tN, ()) ... )) Cat ts () = ts So for your lemma to hold, you need a new judgement "Valid ts": class Valid ts where cat_nil :: Equiv (Cat ts ()) ts -- other lemmas here instance Valid () where cat_nil = Equiv instance Valid x => Valid (a, x) where cat_nil = case (cat_nil :: Equiv (Cat x ()) x) of Equiv -> Equiv coerce :: forall f ts. Valid ts => f (Cat ts ()) -> f ts coerce x = case (cat_nil :: Equiv (Cat ts ()) ts) of Equiv -> x Also, I'm not sure if GHC can currently optimize away cat_nil; it's clear by construction that cat_nil is total, but if the compiler can't detect that it needs to run and make sure it returns Equiv and not _|_. Otherwise you get an unsound result: (given the type instance above) instance Valid [a] where cat_nil = cat_nil Oleg has pointed out this problem with GADTs as type witnesses here: http://okmij.org/ftp/Haskell/GADT-problem.hs -- ryan On 2/15/08, Ryan Ingram wrote:

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 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