:i and :t give different types

newer
Fwd: [pdxfunc] pdxfunc meeting:...

older
User groups meeting all over the...

Chad Scherrer

7 Feb 2008 7 Feb '08

1:40 p.m.

Hello haskell-cafe, In ghci, I tried to get info for Data.Stream.Stream: $ ghci GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. Prelude> :m Data.Stream Prelude Data.Stream> :i Stream data Stream a where Stream :: forall a s. (Data.Stream.Unlifted s) => !s -> Step a s -> !s -> Stream a -- Defined in Data.Stream instance Functor Stream -- Defined in Data.Stream This didn't seem right to me, so I asked tried this: Prelude Data.Stream> :t Stream Stream :: (Data.Stream.Unlifted s) => (s -> Step a s) -> s -> Stream a What's going on here? forall a s. (Data.Stream.Unlifted s) => !s -> Step a s -> !s -> Stream a and (Data.Stream.Unlifted s) => (s -> Step a s) -> s -> Stream a are completely different, right? And really, neither one makes much sense to me. I would have expected forall s. (Data.Stream.Unlifted s) => (s -> Step a s) -> s -> Stream a -- Chad

Show replies by date

Don Stewart

7 Feb 7 Feb

2:47 p.m.

chad.scherrer:

...

Hello haskell-cafe,

In ghci, I tried to get info for Data.Stream.Stream:

$ ghci GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. Prelude> :m Data.Stream Prelude Data.Stream> :i Stream data Stream a where Stream :: forall a s. (Data.Stream.Unlifted s) => !s -> Step a s -> !s -> Stream a -- Defined in Data.Stream

That's fine, and is the correct type. data Stream a = forall s. Unlifted s => Stream !(s -> Step a s) -- ^ a stepper function !s -- ^ an initial state

...

instance Functor Stream -- Defined in Data.Stream

This didn't seem right to me, so I asked tried this:

Prelude Data.Stream> :t Stream Stream :: (Data.Stream.Unlifted s) => (s -> Step a s) -> s -> Stream a

So that's the type of the Stream constructor, which introduces a new existentially typed Stream (the 'a').

...

What's going on here?

forall a s. (Data.Stream.Unlifted s) => !s -> Step a s -> !s -> Stream a and (Data.Stream.Unlifted s) => (s -> Step a s) -> s -> Stream a

One is the type, one is the constructor for the type.

...

are completely different, right? And really, neither one makes much sense to me. I would have expected

forall s. (Data.Stream.Unlifted s) => (s -> Step a s) -> s -> Stream a

For the constructor? This all looks right, as far as I can tell: $ ghci -fglasgow-exts Prelude> :m + Data.Stream Info about the data type: Prelude Data.Stream> :info Stream data Stream a where Stream :: forall a s. (Data.Stream.Unlifted s) => !s -> Step a s -> !s -> Stream a -- Defined in Data.Stream instance Functor Stream -- Defined in Data.Stream The type of the constructor Prelude Data.Stream> :t Stream Stream :: forall s a. (Data.Stream.Unlifted s) => (s -> Step a s) -> s -> Stream a The kind of the type: Prelude Data.Stream> :k Stream Stream :: * -> * -- Don

Ryan Ingram

2:55 p.m.

It looks like there is a bug with unparsing of bang-constructors in ghci: On 2/7/08, Don Stewart wrote:

...

data Stream a = forall s. Unlifted s => Stream !(s -> Step a s) -- ^ a stepper function !s -- ^ an initial state

...

Prelude Data.Stream> :info Stream data Stream a where Stream :: forall a s. (Data.Stream.Unlifted s) => !s -> Step a s -> !s -> Stream a

This last line should start with !(s -> Step a s) instead of !s -> Step a s. If that was fixed, everything looks correct. -- ryan

Don Stewart

2:57 p.m.

ryani.spam:

...

It looks like there is a bug with unparsing of bang-constructors in ghci:

On 2/7/08, Don Stewart wrote:

...
data Stream a = forall s. Unlifted s => Stream !(s -> Step a s) -- ^ a stepper function !s -- ^ an initial state

...
Prelude Data.Stream> :info Stream data Stream a where Stream :: forall a s. (Data.Stream.Unlifted s) => !s -> Step a s -> !s -> Stream a

This last line should start with !(s -> Step a s) instead of !s -> Step a s.

If that was fixed, everything looks correct.

Ah, yes, missing parens! Well spotted. So a pretty printer wibble in GHC? -- Don

Chad Scherrer

3:30 p.m.

On Feb 7, 2008 11:57 AM, Don Stewart wrote:

...

Ah, yes, missing parens! Well spotted.

So a pretty printer wibble in GHC?

-- Don

Yeah, that was my first concern, but then I noticed the quantification was different, so I'm still working through that one. It was confusing, since I assumed the implementations of :i and :t shared a lot of code. -- Chad

Jonathan Cast

9:44 p.m.

On 7 Feb 2008, at 12:30 PM, Chad Scherrer wrote:

...

On Feb 7, 2008 11:57 AM, Don Stewart wrote:

...
Ah, yes, missing parens! Well spotted.

So a pretty printer wibble in GHC?

-- Don

Yeah, that was my first concern, but then I noticed the quantification was different, so I'm still working through that one.

The quantification isn't different, just differently presented. In Haskell 98, there are never explicit foralls and any type is implicitly quantified over its free variables at the top level. So, in GHC a type without explicit foralls is quantified over its free variables at the top level. So the two types are in fact equal.

...

It was confusing, since I assumed the implementations of :i and :t shared a lot of code.

Apparently not :) jcc

Simon Peyton-Jones

8 Feb 8 Feb

12:55 p.m.

I have not been following closely but if Don thinks there's a bug there probably is. Can someone submit a bug report pls? Better still a patch! :-) Simon | -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of Don Stewart | Sent: 07 February 2008 19:58 | To: Ryan Ingram | Cc: haskell-cafe@haskell.org; Chad Scherrer | Subject: Re: [Haskell-cafe] :i and :t give different types | | ryani.spam: | > It looks like there is a bug with unparsing of bang-constructors in ghci: | > | > On 2/7/08, Don Stewart wrote: | > > data Stream a = forall s. Unlifted s => | > > Stream !(s -> Step a s) -- ^ a stepper function | > > !s -- ^ an initial state | > | > > Prelude Data.Stream> :info Stream | > > data Stream a where | > > Stream :: forall a s. | > > (Data.Stream.Unlifted s) => | > > !s -> Step a s -> !s -> Stream a | > | > This last line should start with !(s -> Step a s) instead of !s -> Step a s. | > | > If that was fixed, everything looks correct. | | Ah, yes, missing parens! Well spotted. | | So a pretty printer wibble in GHC? | | -- Don | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe

Chad Scherrer

1:28 p.m.

On Feb 8, 2008 9:55 AM, Simon Peyton-Jones wrote:

...

I have not been following closely but if Don thinks there's a bug there probably is. Can someone submit a bug report pls? Better still a patch! :-)

Simon

Ok, I filed a bug report.

6312

Age (days ago)

6313

Last active (days ago)

List overview

Download

7 comments

5 participants

participants (5)

Chad Scherrer
Don Stewart
Jonathan Cast
Ryan Ingram
Simon Peyton-Jones