[Haskell-cafe] Re: [Haskell] Lemmas about type functions
Ryan Ingram
ryani.spam at gmail.com
Fri Feb 15 19:50:08 EST 2008
[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 <ryani.spam at gmail.com> 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 <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
> >
>
More information about the Haskell-Cafe
mailing list