[Haskell-cafe] Re: Comparing GADTs for Eq and Ord

2008-09-16 Thread apfelmus
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 =

Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord

2008-09-16 Thread Tom Hawkins
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

[Haskell-cafe] Re: Comparing GADTs for Eq and Ord

2008-09-15 Thread apfelmus
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.

Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord

2008-09-15 Thread Tom Hawkins
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

Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord

2008-09-15 Thread Dan Weston
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

Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord

2008-09-15 Thread Ryan Ingram
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

Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord

2008-09-15 Thread Ganesh Sittampalam
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

Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord

2008-09-15 Thread Jason Dagit
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

Re: [Haskell-cafe] Re: Comparing GADTs for Eq and Ord

2008-09-15 Thread Ryan Ingram
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

[Haskell-cafe] Re: Comparing GADTs for Eq and Ord

2008-09-15 Thread Ashley Yakeley
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

[Haskell-cafe] Re: Comparing GADTs for Eq and Ord

2008-09-15 Thread Ashley Yakeley
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