Re: [Haskell-cafe] Type equality proof
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
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
etc.
On Tue, Mar 17, 2009 at 3:39 AM, Martijn van Steenbergen
mart...@van.steenbergen.nl wrote:
Olá café,
With the recent generic programming work and influences from type-dependent
languages such as Agda, the following data type seems to come up often:
data (a :=: a') where
Refl :: a :=: a
Everyone who needs it writes their own version; I'd like to compile a
package with this data type and related utilities, if such a package doesn't
exist already (I couldn't find one). Below is what I have so far; I'd much
appreciate it if you added your ideas of what else the package should
contain.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Eq where
data (a :=: a') where
Refl :: a :=: a
class Eq1 f where
eq1 :: f a - f a' - Maybe (a :=: a')
class Eq2 f where
eq2 :: f a b - f a' b' - Maybe (a :=: a', b :=: b')
class Eq3 f where
eq3 :: f a b c - f a' b' c' - Maybe (a :=: a', b :=: b', c :=: c')
Thank you,
Martijn.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Type equality proof
Olá café,
With the recent generic programming work and influences from
type-dependent languages such as Agda, the following data type seems to
come up often:
data (a :=: a') where
Refl :: a :=: a
Everyone who needs it writes their own version; I'd like to compile a
package with this data type and related utilities, if such a package
doesn't exist already (I couldn't find one). Below is what I have so
far; I'd much appreciate it if you added your ideas of what else the
package should contain.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Eq where
data (a :=: a') where
Refl :: a :=: a
class Eq1 f where
eq1 :: f a - f a' - Maybe (a :=: a')
class Eq2 f where
eq2 :: f a b - f a' b' - Maybe (a :=: a', b :=: b')
class Eq3 f where
eq3 :: f a b c - f a' b' c' - Maybe (a :=: a', b :=: b', c :=: c')
Thank you,
Martijn.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
data (a :=: a') where
Refl :: a :=: a
Comm :: (a :=: a') - (a' :=: a)
Trans :: (a :=: a') - (a' :=: a'') - (a :=: a'')
Martijn van Steenbergen wrote:
Olá café,
With the recent generic programming work and influences from
type-dependent languages such as Agda, the following data type seems
to come up often:
data (a :=: a') where
Refl :: a :=: a
Everyone who needs it writes their own version; I'd like to compile a
package with this data type and related utilities, if such a package
doesn't exist already (I couldn't find one). Below is what I have so
far; I'd much appreciate it if you added your ideas of what else the
package should contain.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Eq where
data (a :=: a') where
Refl :: a :=: a
class Eq1 f where
eq1 :: f a - f a' - Maybe (a :=: a')
class Eq2 f where
eq2 :: f a b - f a' b' - Maybe (a :=: a', b :=: b')
class Eq3 f where
eq3 :: f a b c - f a' b' c' - Maybe (a :=: a', b :=: b', c :=: c')
Thank you,
Martijn.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
On Tue, Mar 17, 2009 at 11:39:05AM +0100, Martijn van Steenbergen wrote:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Eq where
data (a :=: a') where
Refl :: a :=: a
class Eq1 f where
eq1 :: f a - f a' - Maybe (a :=: a')
class Eq2 f where
eq2 :: f a b - f a' b' - Maybe (a :=: a', b :=: b')
class Eq3 f where
eq3 :: f a b c - f a' b' c' - Maybe (a :=: a', b :=: b', c :=: c')
I don't understand your classes Eq1, Eq2, and Eq3. How would you make
an instance of Eq1 for, say, [] ?
instance Eq1 [] where
eq1 xs ys = ???
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.
Maybe you mean for eq1 to have a type like
eq1 :: (f a :=: f a') - (a :=: a') ?
But actually, you don't need a type class for that either;
eq1 :: (f a :=: f a') - (a :=: a')
eq1 Refl = Refl
type checks just fine.
-Brent
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
On Tue, Mar 17, 2009 at 10:30 AM, Brent Yorgey byor...@seas.upenn.edu 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
On Tue, Mar 17, 2009 at 6:14 AM, Wolfgang Jeltsch g9ks1...@acme.softbase.org 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. Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
2009/3/17 Luke Palmer lrpal...@gmail.com: 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 d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
Hi On 17 Mar 2009, at 21:06, David Menendez wrote: 2009/3/17 Luke Palmer lrpal...@gmail.com: 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 That and the identity-on-objects functor to sets and functions. Mutter mutter Leibniz Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
Ryan Ingram wrote: These types are very useful for construction of type-safe interpreters and compilers. That's exactly what I have in mind. In my specific case I want to compare the constructors of the GADT representing a datatype family in the multirec package: data AST a where Stmt :: AST Stmt Expr :: AST Expr Martijn. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
Martijn van Steenbergen wrote: class Eq2 f where eq2 :: f a b - f a' b' - Maybe (a :=: a', b :=: b') Is that right, or does the following make more sense? class Eq2 f where eq2 :: f a b - f a' b' - (Maybe (a :=: a'), Maybe (b :=: b')) Thanks, Martijn. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
On 17 Mar 2009, at 21:44, Martijn van Steenbergen wrote: 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? Apologies for being glib and elliptic: filthy habit. That would be coerce :: (a :=: b) - (a - b) coerce Refl a = a taking arrows in the :=: category (aka the discrete category on *) to arrows in the - category, preserving the objects involved. It captures the main useful consequence of an equation between types. I guess the other thing you need is resp :: (a :=: b) - (f a :=: f b) resp Refl = Refl (any type constructor gives you a functor from the :=: category to itself). If you compose the two, you get Leibniz's characterization of equality -- that it's substitutive: subst :: a :=: b - (f a - f b) subst = coerce . resp Or you can start from subst and build the other two by careful instantiation of f. By the way, I see the motivation for your Eq1 class, which seems useful for the singleton GADTs which get used to give value-level representations to type-level stuff (combine with fmap coerce to get SYB-style cast), but I'm not quite sure where Eq2, etc, come in. Have you motivating examples for these? It's well worth striving for some sort of standard kit here. I should add that mentioning equality is the best way to start a fight at a gathering of more than zero type theorists. But perhaps there are fewer things to cause trouble in Haskell. So thanks for this, Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
