Am Dienstag, 17. März 2009 11:49 schrieb Yandex:

data (a :=: a') where Refl :: a :=: a Comm :: (a :=: a') -> (a' :=: a) Trans :: (a :=: a') -> (a' :=: a'') -> (a :=: a'')

I don’t think, Comm and Trans should go into the data type. They are not axioms but can be proven. Refl says that each type equals itself. Since GADTs are closed, Martijn’s definition also says that two types can *only* be equal if they are actually the same. Here are the original definition and the proofs of comm and trans. Compiles fine with GHC 6.10.1. data (a :=: a') where Refl :: a :=: a comm :: (a :=: a') -> (a' :=: a) comm Refl = Refl trans :: (a :=: a') -> (a' :=: a'') -> (a :=: a'') trans Refl Refl = Refl Best wishes, Wolfgang

2009/3/17 Luke Palmer :

...

Here are the original definition and the proofs of comm and trans. Compiles fine with GHC 6.10.1.

   data (a :=: a') where

       Refl :: a :=: a

   comm :: (a :=: a') -> (a' :=: a)    comm Refl = Refl

   trans :: (a :=: a') -> (a' :=: a'') -> (a :=: a'')    trans Refl Refl = Refl

These two theorems should be in the package.

How about this? instance Category (:=:) where id = Refl Refl . Refl = Refl -- Dave Menendez http://www.eyrie.org/~zednenem/

Conor McBride wrote:

...

instance Category (:=:) where id = Refl Refl . Refl = Refl

That and the identity-on-objects functor to sets and functions.

Not sure what you mean by this, Conor. Can you please express this in Haskell code? Thanks, Martijn.

Am Dienstag, 17. März 2009 21:51 schrieben Sie:

On Tue, Mar 17, 2009 at 6:14 AM, Wolfgang Jeltsch wrote:

...

Am Dienstag, 17. März 2009 11:49 schrieb Yandex:

...

data (a :=: a') where Refl :: a :=: a Comm :: (a :=: a') -> (a' :=: a) Trans :: (a :=: a') -> (a' :=: a'') -> (a :=: a'')

I don’t think, Comm and Trans should go into the data type. They are not axioms but can be proven. Refl says that each type equals itself. Since GADTs are closed, Martijn’s definition also says that two types can *only* be equal if they are actually the same.

Here are the original definition and the proofs of comm and trans. Compiles fine with GHC 6.10.1.

data (a :=: a') where

Refl :: a :=: a

comm :: (a :=: a') -> (a' :=: a) comm Refl = Refl

trans :: (a :=: a') -> (a' :=: a'') -> (a :=: a'') trans Refl Refl = Refl

These two theorems should be in the package.

But they should not be data constructors. Best wishes, Wolfgang

On Tue, Mar 17, 2009 at 10:30 AM, Brent Yorgey wrote:

I don't understand your classes Eq1, Eq2, and Eq3.  How would you make an instance of Eq1 for, say, [] ?

You don't.

It seems you are confusing _value_ equality with _type_ equality?  A value of type a :=: a' is a proof that a and a' are the same type. But given values of type f a and f a', there is no way to decide whether a and a' are the same type (no matter what f is), since types are erased at runtime.

Not necessarily. Consider this example: data U a where UInt :: U Integer UBool :: U Bool instance Eq1 U where eq1 UInt UInt = Just Refl eq1 UBool UBool = Just Refl eq1 _ _ = Nothing data Expr a where EPrim :: U a -> a -> Expr a EIf :: Expr Bool -> Expr a -> Expr a -> Expr a EPlus :: Expr Integer -> Expr Integer -> Expr Integer ELess :: Expr Integer -> Expr Integer -> Expr Bool typeOf :: Expr a -> U a typeOf (EPrim u _) = u typeOf (EIf _ t _) = typeOf t typeOf (EPlus _ _) = UInt typeOf (ELess _ _) = UBool instance Eq1 Expr where eq1 lhs rhs = eq1 (typeOf lhs) (typeOf rhs) These types are very useful for construction of type-safe interpreters and compilers. -- ryan

Hi On 18 Mar 2009, at 15:00, Conal Elliott wrote:

I use these defs:

-- | Lift proof through a unary type constructor liftEq :: a :=: a' -> f a :=: f a' liftEq Refl = Refl

-- | Lift proof through a binary type constructor (including '(,)') liftEq2 :: a :=: a' -> b :=: b' -> f a b :=: f a' b' liftEq2 Refl Refl = Refl

-- | Lift proof through a ternary type constructor (including '(,,)') liftEq3 :: a :=: a' -> b :=: b' -> c :=: c' -> f a b c :=: f a' b' c' liftEq3 Refl Refl Refl = Refl

Makes you want kind polymorphism, doesn't it? Then we could just have (=$=) :: f :=: g -> a :=: b -> f a :=: g b Maybe the liftEq_n's are the way to go (although we called them "resp_n" when I was young), but they don't work for higher kinds. An alternative ghastly hack might be

data PackT2T (f :: * -> *)

(=$=) :: (PackT2T f :=: PackT2T g) -> (a :=: b) -> (f a :=: g b) Refl =$= Refl = Refl

But now you need a packer and an application for each higher kind. Or some bonkers type-level programming. This one will run and run... Cheers Conor

Ashley Yakeley wrote:

Have a look at these:

http://hackage.haskell.org/cgi-bin/hackage-scripts/package/witness http://hackage.haskell.org/cgi-bin/hackage-scripts/package/open-witness

Ah, nice! It seems most we came up with is already in there. Even Any which I use in my project but didn't think of putting in the package is there. No use anymore for a new package now, I guess. On the other hand, I can't find the comm, trans, coerce, subst and resp. Would it be an idea to add those to your package? Thanks, Martijn.