Should the following program be accepted by ghc?
Hello, I have been playing with ghc6.8.1 and type families and the following program is accepted without any type-checking error:
data a :=: b where Eq :: a :=: a
decomp :: f a :=: f b -> a :=: b decomp Eq = Eq
However, I find this odd because if you interpret "f" as a function and ":=:" as equality, then this is saying that if f a = f b then a = b but clearly this does not hold in general. For example: f 1 = 0 f 2 = 0 So, we have that "f 1 = f 2" but this does not imply that "1 = 2". Ofcourse, that before ghc6.8, we add no type-level functions so maybe it was ok to consider the program above. However, with open type functions the following program is problematic and crashes ghc in style:
type family K a
c :: K a :=: K b -> a :=: b c Eq = Eq
with the following error message: ghc-6.8.1: panic! (the 'impossible' happened) (GHC version 6.8.1 for i386-apple-darwin): Coercion.splitCoercionKindOf base:GHC.Prim.sym{(w) tc 34v} co_aoW{tv} [tv] <pred>main:Bug.K{tc rom} a{tv aoS} [sk] ~ main:Bug.K{tc rom} b{tv aoT} [sk] It seems to me that the "decomp" should be rejected in the first place? Maybe the fact that "decomp" is accepted is a bug in the compiler? Any comments? Cheers, Bruno Oliveira
[Whoever replies next pl move discussion to haskell-cafe] Bruno Oliveira writes:
Hello,
I have been playing with ghc6.8.1 and type families and the following program is accepted without any type-checking error:
data a :=: b where Eq :: a :=: a
decomp :: f a :=: f b -> a :=: b decomp Eq = Eq
However, I find this odd because if you interpret "f" as a function and ":=:" as equality, then this is saying that
if f a = f b then a = b
but clearly this does not hold in general. For example:
f 1 = 0 f 2 = 0
So, we have that "f 1 = f 2" but this does not imply that "1 = 2".
Ofcourse, that before ghc6.8, we add no type-level functions so maybe it was ok to consider the program above.
Correct. The decomposition law f a = f b ==> a = b applies only to ordinary type constructors (eg list [] etc). See the System FC paper for more details. There's a (silent) constraint imposed on the program
decomp :: f a :=: f b -> a :=: b decomp Eq = Eq
saying that f can only be instantiated with an ordinary type constructor. As far as I know, GHC obeys this restriction (Manuel, Simon and Tom who have implemented type families may be able to tell you more).
However, with open type functions the following program is problematic and crashes ghc in style:
type family K a
c :: K a :=: K b -> a :=: b c Eq = Eq
with the following error message:
ghc-6.8.1: panic! (the 'impossible' happened) (GHC version 6.8.1 for i386-apple-darwin): Coercion.splitCoercionKindOf base:GHC.Prim.sym{(w) tc 34v} co_aoW{tv} [tv] <pred>main:Bug.K{tc rom} a{tv aoS} [sk] ~ main:Bug.K{tc rom} b{tv aoT} [sk]
It seems to me that the "decomp" should be rejected in the first place? Maybe the fact that "decomp" is accepted is a bug in the compiler?
As said above, you are not allowed to instantiate f with a type family constructor. Therefore, decomp is fine. The above program text "crashes" becaue we canNOT deduce that K a = K b ==> a =b The decomposition law does NOT apply to type family constructors. Indeed, ghc shouldn't crash here and instead provide a more helpful error message. Martin
Any comments?
Cheers,
Bruno Oliveira _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
On Wed, Jan 16, 2008 at 01:02:43PM +0800, Martin Sulzmann wrote:
Bruno Oliveira writes:
I have been playing with ghc6.8.1 and type families and the following program is accepted without any type-checking error:
data a :=: b where Eq :: a :=: a ... Ofcourse, that before ghc6.8, we add no type-level functions so maybe it was ok to consider the program above. ... type family K a
Type families are unsupported, and their intersection with GADTs are unimplemented. Don't expect any program which uses both to do anything sane until 6.10. Stefan
stefanor:
On Wed, Jan 16, 2008 at 01:02:43PM +0800, Martin Sulzmann wrote:
Bruno Oliveira writes:
I have been playing with ghc6.8.1 and type families and the following program is accepted without any type-checking error:
data a :=: b where Eq :: a :=: a ... Ofcourse, that before ghc6.8, we add no type-level functions so maybe it was ok to consider the program above. ... type family K a
Type families are unsupported, and their intersection with GADTs are unimplemented. Don't expect any program which uses both to do anything sane until 6.10.
That being said, bug reports against the head version of GHC *are* welcome. But they're not an official feature of ghc 6.8, as Stefan hinted. -- Don
| I have been playing with ghc6.8.1 and type families and the following | program is accepted without any type-checking error: Martin's comments are spot on. FWIW, in the HEAD -- as Stefan says, type families are not *supposed* to work in 6.8.1 -- your program gives TF.hs:9:7: Couldn't match expected type `a' against inferred type `b' `a' is a rigid type variable bound by the type signature for `c' at TF.hs:8:7 `b' is a rigid type variable bound by the type signature for `c' at TF.hs:8:15 Expected type: a :=: b Inferred type: b :=: b In the expression: Eq In the definition of `c': c Eq = Eq That's fair enough. If you change K to be a 'data family', then decomposition works, and the program compiles. Bugs in type families against the HEAD are, as Don says, highly welcome. Simon
On Jan 16, 2008, at 2:08 AM, Bruno Oliveira wrote:
Hello,
I have been playing with ghc6.8.1 and type families and the following program is accepted without any type-checking error:
data a :=: b where Eq :: a :=: a
decomp :: f a :=: f b -> a :=: b decomp Eq = Eq
However, I find this odd because if you interpret "f" as a function and ":=:" as equality, then this is saying that
if f a = f b then a = b
This is saying that f is injective. So perhaps the standard interpretation leads implicitly to this class of functions. Cheers jno
On Wed, 2008-01-16 at 09:18 +0000, J.N. Oliveira wrote:
On Jan 16, 2008, at 2:08 AM, Bruno Oliveira wrote:
Hello,
I have been playing with ghc6.8.1 and type families and the following program is accepted without any type-checking error:
data a :=: b where Eq :: a :=: a
decomp :: f a :=: f b -> a :=: b decomp Eq = Eq
However, I find this odd because if you interpret "f" as a function and ":=:" as equality, then this is saying that
if f a = f b then a = b
This is saying that f is injective. So perhaps the standard interpretation leads implicitly to this class of functions.
Just like data constructors, type constructors are injective. f a doesn't simplify and so essentially you have structural equality of the type terms thus f a = f b is -equivalent- to a = b. Obviously type functions change this, just like normal value functions do at the value level.
Hello, Maybe a more slightly more honest type for "decomp" would be:) : decomp :: Injective f => f a :=: f b -> a :=: b Cheers, Bruno On Wed, 16 Jan 2008, Derek Elkins wrote:
On Wed, 2008-01-16 at 09:18 +0000, J.N. Oliveira wrote:
On Jan 16, 2008, at 2:08 AM, Bruno Oliveira wrote:
Hello,
I have been playing with ghc6.8.1 and type families and the following program is accepted without any type-checking error:
data a :=: b where Eq :: a :=: a
decomp :: f a :=: f b -> a :=: b decomp Eq = Eq
However, I find this odd because if you interpret "f" as a function and ":=:" as equality, then this is saying that
if f a = f b then a = b
This is saying that f is injective. So perhaps the standard interpretation leads implicitly to this class of functions.
Just like data constructors, type constructors are injective. f a doesn't simplify and so essentially you have structural equality of the type terms thus f a = f b is -equivalent- to a = b. Obviously type functions change this, just like normal value functions do at the value level.
On 16 Jan 2008, at 5:59 PM, Bruno Oliveira wrote:
Hello,
Maybe a more slightly more honest type for "decomp" would be:) :
decomp :: Injective f => f a :=: f b -> a :=: b
Perhaps. Although you *have* to have an implicit Injective constraint on all type constructor variables to pull of Haskell's first-order unification trick, so it's not a constraint that will be relaxed soon (or, most likely, ever). jcc
participants (8)
-
Bruno Oliveira -
Derek Elkins -
Don Stewart -
J.N. Oliveira -
Jonathan Cast -
Martin Sulzmann -
Simon Peyton-Jones -
Stefan O'Rear