[Haskell-cafe] Re: Comparing GADTs for Eq and Ord
Tom Hawkins wrote: apfelmus wrote: So, in other words, in order to test whether terms constructed with Equal are equal, you have to compare two terms of different type for equality. Well, nothing easier than that: (===) :: Expr a - Expr b - Bool Const === Const = True (Equal a b) === (Equal a' b') = a === a' b === b' _ === _ = False instance Eq (Expr a) where (==) = (===) OK. But let's modify Expr so that Const carries values of different types: data Expr :: * - * where Const :: a - Term a Equal :: Term a - Term a - Term Bool How would you then define: Const a === Const b = ... Well, Const :: a - Term a is too general anyway, you do need some information on a to be able to compare different Const terms. An Eq constraint on a is the minimum: Const :: Eq a = a - Term a But that's not enough for (===) of course, additional information as suggested by others is needed. Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord
Thanks for all the input. It helped me arrive at the following solution. I took the strategy of converting the parameterized type into an unparameterized type which can be easily compared for Eq and Ord. The unparameterized type enumerates the possible Const types with help from an auxiliary type class. -- The primary Expr type. data Expr a where Const :: ExprConst a = a - Expr a Equal :: Expr a - Expr a - Expr Bool -- An untyped Expr used to compute Eq and Ord of the former. -- Note each type of constant is enumerated. data UExpr = UConstBool Bool | UConstIntInt | UConstFloat Float | UEqual UExpr UExpr deriving (Eq, Ord) -- A type class to assist in converting Expr to UExpr. classExprConst a where uexprConst :: a - UExpr instance ExprConst Bool where uexprConst = UConstBool instance ExprConst Int where uexprConst = UConstInt instance ExprConst Float where uexprConst = UConstFloat -- The conversion function. uexpr :: Expr a - UExpr uexpr (Const a) = uexprConst a uexpr (Equal a b) = UEqual (uexpr a) (uexpr b) -- Finally the implementation of Eq and Ord for Expr. instance Eq (Expr a) where a == b = uexpr a == uexpr b instance Ord (Expr a) where compare a b = compare (uexpr a) (uexpr b) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Comparing GADTs for Eq and Ord
Jason Dagit wrote: Tom Hawkins wrote: How do I compare a GADT type if a particular constructor returns a concrete type parameter? For example: data Expr :: * - * where Const :: Expr a Equal :: Expr a - Expr a - Expr Bool -- If this read Expr a, the compiler has no problem. instance Eq (Expr a) where Const == Const = True (Equal a b) (Equal x y) = a == x b == y _ == _ = False GHC throws: Couldn't match expected type `a1' against inferred type `a2' `a1' is a rigid type variable bound by the constructor `Equal' at Test.hs:9:3 `a2' is a rigid type variable bound by the constructor `Equal' at Test.hs:9:18 Expected type: Expr a1 Inferred type: Expr a2 In the second argument of `(==)', namely `x' In the first argument of `()', namely `a == x' I believe I understand the reason for the problem; even though Equal has a type Expr Bool, two Equal expressions could have parameters of different types. But I'm not sure how to get around the problem. Any suggestions? Equal :: Expr a - Expr a - Expr Bool Makes the type parameter 'a' an existential type. You can think of it like this: data Expr a = Equal (forall a. Expr a Expr a) I think that forall is in the right place. You mean data ExprBool = forall a. Equal (Expr a) (Expr a) This means that when you use the (Equal a b) pattern the 'a' has to be instantiated to some distinct rigid type, and similarly (Equal x y) instantiates 'a' again to some distinct rigid type. This is where your a1 and a2 in the error message come from. So, in other words, in order to test whether terms constructed with Equal are equal, you have to compare two terms of different type for equality. Well, nothing easier than that: (===) :: Expr a - Expr b - Bool Const === Const = True (Equal a b) === (Equal a' b') = a === a' b === b' _ === _ = False instance Eq (Expr a) where (==) = (===) Chances are that the equality test with different types is more useful in the rest of your program as well. Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord
On Mon, Sep 15, 2008 at 3:11 PM, apfelmus [EMAIL PROTECTED] wrote: So, in other words, in order to test whether terms constructed with Equal are equal, you have to compare two terms of different type for equality. Well, nothing easier than that: (===) :: Expr a - Expr b - Bool Const === Const = True (Equal a b) === (Equal a' b') = a === a' b === b' _ === _ = False instance Eq (Expr a) where (==) = (===) OK. But let's modify Expr so that Const carries values of different types: data Expr :: * - * where Const :: a - Term a Equal :: Term a - Term a - Term Bool How would you then define: Const a === Const b = ... -Tom ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord
Take a look at http://www.haskell.org/haskellwiki/GHC/AdvancedOverlap Tom Hawkins wrote: On Mon, Sep 15, 2008 at 3:11 PM, apfelmus [EMAIL PROTECTED] wrote: So, in other words, in order to test whether terms constructed with Equal are equal, you have to compare two terms of different type for equality. Well, nothing easier than that: (===) :: Expr a - Expr b - Bool Const === Const = True (Equal a b) === (Equal a' b') = a === a' b === b' _ === _ = False instance Eq (Expr a) where (==) = (===) OK. But let's modify Expr so that Const carries values of different types: data Expr :: * - * where Const :: a - Term a Equal :: Term a - Term a - Term Bool How would you then define: Const a === Const b = ... -Tom ___ 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] Re: Comparing GADTs for Eq and Ord
On Mon, Sep 15, 2008 at 2:25 PM, Tom Hawkins [EMAIL PROTECTED] wrote: OK. But let's modify Expr so that Const carries values of different types: data Expr :: * - * where Const :: a - Term a Equal :: Term a - Term a - Term Bool How would you then define: Const a === Const b = ... You can't. But you can do so slightly differently: import Data.Typeable data Expr :: * - * where Const :: (Eq a, Typeable a) = a - Term a Equal :: Term a - Term a - Term Bool (===) :: Expr a - Expr b - Bool Const a === Const b = case cast a of Nothing - False Just a' - a' == b Equal l1 r1 === Equal l2 r2 = l1 === l2 r1 === r2 _ === _ = False You can also represent Const as follows: Const :: TypeRep a - a - Term a There are many papers that talk about using GADTs to reify types in this fashion to allow safe typecasting. They generally all rely on the base GADT, TEq; every other GADT can be defined in terms of TEq and existential types. data TEq :: * - * - * where Refl :: TEq a a As an example, here is Expr defined in this fashion: data Expr a = (Eq a, Typeable a) = Const a | forall b. Equal (TEq a Bool) (Expr b) (Expr b) equal :: Expr a - Expr a - Expr Bool equal = Equal Refl -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord
On Mon, 15 Sep 2008, Tom Hawkins wrote: OK. But let's modify Expr so that Const carries values of different types: data Expr :: * - * where Const :: a - Term a Equal :: Term a - Term a - Term Bool How would you then define: Const a === Const b = ... Apart from the suggestions about Data.Typeable etc, one possibility is to enumerate the different possible types that will be used as parameters to Const in different constructors, either in Expr or in a new type. So IntConst :: Int - Expr Int, etc Or Const :: Const a - Expr a and IntConst :: Int - Const Int etc Not very pleasant though. Ganesh ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord
On Mon, Sep 15, 2008 at 2:50 PM, Ryan Ingram [EMAIL PROTECTED] wrote: There are many papers that talk about using GADTs to reify types in this fashion to allow safe typecasting. They generally all rely on the base GADT, TEq; every other GADT can be defined in terms of TEq and existential types. I just found that Tim Sheard has collected a nice list of papers on this subject: http://web.cecs.pdx.edu/~sheard/ Jason ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord
On Mon, Sep 15, 2008 at 2:53 PM, Ganesh Sittampalam [EMAIL PROTECTED] wrote: Apart from the suggestions about Data.Typeable etc, one possibility is to enumerate the different possible types that will be used as parameters to Const in different constructors, either in Expr or in a new type. So IntConst :: Int - Expr Int, etc Or Const :: Const a - Expr a and IntConst :: Int - Const Int etc Not very pleasant though. You can actually generalize this quite a bit, as I touched on slightly in my last post: data Expr a where Const :: TypeRep a - a - Expr a ... data TEq a b where Refl :: TEq a a data TypeRep a where TInt :: TypeRep Int TBool :: TypeRep Bool TList :: TypeRep a - TypeRep [a] TArrow :: TypeRep a - TypeRep b - TypeRep (a - b) -- etc. You can then implement the cast used in === in the following way: typeEq :: TypeRep a - TypeRep b - Maybe (TEq a b) typeEq TInt TInt = return Refl typeEq TBool TBool = return Refl typeEq (TList a) (TList b) = do Refl - typeEq a b return Refl typeEq (TArrow a1 a2) (TArrow b1 b2) = do Refl - typeEq a1 b1 Refl - typeEq a2 b2 return Refl -- etc. typeEq _ _ = fail Types do not match You can use these to write cast cast :: TypeRep a - TypeRep b - a - Maybe b cast ta tb = case typeEq ta tb of Just Refl - \a - Just a _- \_ - Nothing You need a little more work to support equality; the easiest way is to have an Eq constraint on Const, but you can also write a function similar to typeEq that puts an Eq constraint into scope if possible. Pay special attention to the cases in typeEq for TList and TArrow; they make particular use of the desugaring of patterns in do. A desugared version of TList: typeEq a0@(TList a) b0@(TList b) = typeEq a b = \x - case x of Refl - return Refl _ - fail pattern match error In the Maybe monad, inlining (=), return, and fail, this reduces to the following: case typeEq a b of Nothing - Nothing Just x - case x of Refl - Just Refl _ - Nothing When we call typeEq, we have a0 :: TypeRep a0, and b0 :: TypeRep b0, for some unknown types a0 and b0. Then the pattern match on TList unifies both of these types with [a1] and [b1] for some unknown types a1 and b1. We then call typeEq on a :: TypeRep a1, and b :: TypeRep b1. Now, on the right hand side of the Just x case, TEq a b has only one possible value, Refl, so the failure case won't ever be executed. However, the pattern match on Refl is important, because it unifies a1 and b1, which allows us to unify [a1] and [b1] and construct Refl :: TEq [a1] [b1] (which is the same as TEq a0 b0). -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Comparing GADTs for Eq and Ord
Tom Hawkins wrote: data Expr :: * - * where Const :: a - Term a Equal :: Term a - Term a - Term Bool Your basic problem is this: p1 :: Term Bool p1 = Equal (Const 3) (Const 4) p2 :: Term Bool p2 = Equal (Const yes) (Const no) p1 and p2 have the same type, but you're not going to be able to compare them unless you can compare an Int and a String. What do you want p1 == p2 to do? If you want to just say that different types are always non-equal, the simplest way is to create a witness type for your type-system. For instance: data MyType a where IntType :: MyType Int StringType :: MyType String Now you'll want to declare MyType as a simple witness: instance SimpleWitness MyType where matchWitness IntType IntType = Just MkEqualType matchWitness StringType StringType = Just MkEqualType matchWitness _ _ = Nothing You'll need to include a witness wherever parameter types cannot be inferred from the type of the object, as well as an Eq dictionary: data Term :: * - * where Const :: a - Term a Equal :: Eq a = MyType a - Term a - Term a - Term Bool Now you can do: instance Eq a = Eq (Term a) where (Const p1) == (Const p2) = p1 == p2 (Equal w1 p1 q1) (Equal w2 p2 q2) = case matchWitness w1 w2 of MkEqualType - (p1 == p2) (q1 == q2) _ - False -- because the types are different _ == _ = False Note: I haven't actually checked this. Use cabal install witness to get SimpleWitness and EqualType. -- Ashley Yakeley ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Comparing GADTs for Eq and Ord
Ryan Ingram wrote: There are many papers that talk about using GADTs to reify types in this fashion to allow safe typecasting. They generally all rely on the base GADT, TEq; every other GADT can be defined in terms of TEq and existential types. Ah, yes. See my paper Witnesses and Open Witnesses http://semantic.org/stuff/Open-Witnesses.pdf -- Ashley Yakeley ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
