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

[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 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

[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 = 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

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

[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 Witnesses"


--
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

[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 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

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

[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 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

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

[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 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

[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 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

[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 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

[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 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

[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
>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] Re: Comparing GADTs for Eq and Ord

[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.
>>
>> 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