It's not where -- let also works let { foo Prelude> let { foo x = x } in (foo 1, foo True) (1,True) Can you send the code you're trying that doesn't work? -Ross On Jul 16, 2009, at 3:40 PM, Andrew Coppin wrote:

Robert Greayer wrote:

...

f0 _ = (foo True, foo 'x') where foo = id

is well-typed.

Really? That actually works? How interesting... This suggests to me that where-clauses also do strange things to the type system.

...

whereas

f1 foo = (foo True, foo 'x')

requires 'foo' to be polymorphic in its first argument. This does require a higher rank type, which can't be inferred:

You could type f1 as f1 :: (forall a . a -> a) -> (Bool, Char)

and apply it to 'id'.

Or you could type it as something like: f1 :: (forall a . a -> ()) -> ((),())

and apply it to 'const ()'

...all of which is beyond Haskell-98, which is what I am limiting myself to at present.

(Actually, even that is a lie. I don't have type-classes yet...)

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Andrew Coppin wrote:

Awesome. So by attempting to implement Haskell's type system, I have discovered that I actually don't understand Haskell's type system. Who'd have thought it?

Clearly I must go consult the Report and check precisely what the rules are...

I just read section 4.5 of the Haskell 98 Report. Ouch! >_< I knew I'd be sorry I asked... Time for bed, I think!

Is "everything" an acceptable answer? -Ross On Jul 16, 2009, at 6:38 PM, Derek Elkins wrote:

On Thu, Jul 16, 2009 at 2:52 PM, Andrew Coppin wrote:

...

Ross Mellgren wrote:

...

It's not where -- let also works

Prelude> let { foo x = x } in (foo 1, foo True) (1,True)

Awesome. So by attempting to implement Haskell's type system, I have discovered that I actually don't understand Haskell's type system. Who'd have thought it?

Clearly I must go consult the Report and check precisely what the rules are...

The answer to your questions are on the back of this T-shirt. http://www.cafepress.com/skicalc.6225368 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Thu, Jul 16, 2009 at 08:52:40PM +0100, Andrew Coppin wrote:

Ross Mellgren wrote:

...

It's not where -- let also works

Prelude> let { foo x = x } in (foo 1, foo True) (1,True)

Awesome. So by attempting to implement Haskell's type system, I have discovered that I actually don't understand Haskell's type system. Who'd have thought it?

Clearly I must go consult the Report and check precisely what the rules are...

actually, the rules are pretty straightforward. It doesn't matter where something is bound, just _how_ it is bound. Let-bound names (which includes 'where' and top-level definitions) can be polymorphic. lambda-bound or case-bound names (names bound as an argument to a function or that appear in a pattern) can only be monomorphic. And that's all there is to it. (the monomorphism restriction complicates it a little, but we don't need to worry about that for now) As an extension, ghc and jhc allow arguments and case bound variables to be polymorphic but only when explicitly declared so by a user supplied type annotation. (the exact rules for what 'explicitly declared' means can be a little complicated when formalized, but they match up enough with intuition that it isn't a problem in practice). They will never infer such a type on their own. John -- John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/

Andrew,

That seems simple enough (although problematic to implement). However, the Report seems to say that it matters whether or not the bindings are muturally recursive [but I'm not sure precisely *how* it matters...]

It means that functions can only be used monomorphically within their own binding group. (That includes the definition of the function itself: functions cannot be polymorphically recursive. Of course, these restrictions do not apply in case of explicit type signatures. Even if this doesn't all make sense, immediately, it should give you something to google for. ;-)) Cheers, Stefan

On Thu, Jul 16, 2009 at 12:40 PM, Andrew Coppin

wrote:

Robert Greayer wrote:

...

f0 _ = (foo True, foo 'x') where foo = id

is well-typed.

Really? That actually works? How interesting... This suggests to me that where-clauses also do strange things to the type system.

You could think of it that way. You mentioned GADTs in your OP. Well, it turns out GADTs often do not play nicely with where/let and it happens to all be related. As I understand it, functions bind their parameters monomorphically and let/where bind things polymorphically. And then we have the misfeature known as the monomorphism restriction which adds special cases.

whereas

...

f1 foo = (foo True, foo 'x')

requires 'foo' to be polymorphic in its first argument. This does require a higher rank type, which can't be inferred:

You could type f1 as f1 :: (forall a . a -> a) -> (Bool, Char)

and apply it to 'id'.

Or you could type it as something like: f1 :: (forall a . a -> ()) -> ((),())

and apply it to 'const ()'

...all of which is beyond Haskell-98, which is what I am limiting myself to at present.

(Actually, even that is a lie. I don't have type-classes yet...)

Congrats on the type inference engine you're writing. It's on my list of things to do, and I was even reading up on TaPL a month or two back, but I put it down and haven't picked it up again yet. I think writing one would help flush out my understand of all this stuff. Jason