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 =
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
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.
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
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
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
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
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
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
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
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
11 matches
Mail list logo