Should the following program be accepted by ghc?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
9 messages Options
Reply | Threaded
Open this post in threaded view
|

Should the following program be accepted by ghc?

Bruno Oliveira-5
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
Reply | Threaded
Open this post in threaded view
|

Should the following program be accepted by ghc?

Martin Sulzmann

[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
Reply | Threaded
Open this post in threaded view
|

Re: Should the following program be accepted by ghc?

Stefan O'Rear
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
Reply | Threaded
Open this post in threaded view
|

Re: Should the following program be accepted by ghc?

Don Stewart-2
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
Reply | Threaded
Open this post in threaded view
|

RE: Should the following program be accepted by ghc?

Simon Peyton Jones
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
Reply | Threaded
Open this post in threaded view
|

Re: Should the following program be accepted by ghc?

J.N. Oliveira
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
This is saying that  f  is injective. So perhaps the standard  
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
Reply | Threaded
Open this post in threaded view
|

Re: Should the following program be accepted by ghc?

Derek Elkins
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
Reply | Threaded
Open this post in threaded view
|

Re: Should the following program be accepted by ghc?

Bruno Oliveira-5
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
Reply | Threaded
Open this post in threaded view
|

Re: Should the following program be accepted by ghc?

Bugzilla from jonathanccast@fastmail.fm
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