We don't have to wait for the type checkers to rule. The semantics
of GADTs is pretty clear (if it's implemented correctly is another
matter). If you write
data IsIntT x where
IsIntT :: IsIntT Int
then there is only one (non-bottom) value in the IsIntT families of
types and that is IsIntT::IsInt Int
And since Haskell uses nominal type equality there is no type equal
to Int that is not Int.
The fact that you can derive IsIntC looks like a good ole' bug to me.
-- Lennart
On Mar 28, 2007, at 23:22 , Stefan O'Rear wrote:
On Wed, Mar 28, 2007 at 12:03:41PM +0100, Chris Kuklewicz wrote:
Stefan O'Rear wrote:
On Tue, Mar 27, 2007 at 11:32:29AM +0100, Chris Kuklewicz wrote:
Stefan O'Rear wrote:
newtype Foo = Foo Int deriving(IsIntC)
Note that (Foo 2) + 2 is an attempt to add a Foo and an Int,
which cannot
possibly compile. So I replaced it with just a 2.
Why not? They are the same type, and I have Curry-Howard proof
of this fact.
Stefan
Foo is isomorphic to Int in structure. But it is not the same
type. Foo is a
new type that is distinct from Int. That means I get type safety
-- you cannot
pass an Int to a function that expects a Foo and vice versa.
Since (+) is
defined as (Num a => a->a->a) it cannot add type different types
and thus you
*cannot* add a Foo and an Int.
Well, I thought I had a non-bottom value of type IsIntT Foo, but when
I tried to seq it ghc crashed: http://hackage.haskell.org/trac/ghc/
ticket/1251
Let's postpone this discussion until the people who maintain the
typechecker have a chance to rule :)
Stefan
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
