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 _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
[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 > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell _______________________________________________ Haskell mailing list [hidden email] 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 _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell signature.asc (196 bytes) Download Attachment |
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 _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
In reply to this post by Bruno Oliveira-5
| 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 _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
In reply to this post by Bruno Oliveira-5
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 interpretation leads implicitly to this class of functions. Cheers jno _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell smime.p7s (4K) Download Attachment |
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. _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
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. > > Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
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 _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
Free forum by Nabble | Edit this page |