Surprising lack of generalisation

newer
Request for Nominations to the GHC...

Tom Ellis

10 Feb 2021 10 Feb '21

11:31 a.m.

Dear all, I don't understand why the type of pBD defined in the where clause of pFG cannot be inferred to a general type in the presence of TypeFamilies. In particular I don't understand why nonetheless the type of pBD definied in the where clause of pF (only slightly simpler) *can* be inferred. Can anyone explain? Thanks Tom {-# LANGUAGE TypeFamilies #-} -- This code came up in the context of writing a parser, but that's -- not terribly important import Prelude hiding ((<$>)) data B = B data D f = F f | GF AP f | DF AM f data AM = AM data AP = AP pB :: Parser B pB = Parser -- Works fine pF :: Parser (D B) pF = pBD GF AP <|> pBD DF AM where pBD f p = f p <$> pB -- Shows the (presumably) inferred type for pBD pFWithType :: Parser (D B) pFWithType = pBD GF AP <|> pBD DF AM where pBD :: (t -> B -> b) -> t -> Parser b pBD f p = f p <$> pB -- One would hope this type would be inferred too pFGWithType :: Parser B -> Parser (D B) pFGWithType pBArg = pBD GF AP <|> pBD DF AM where pBD :: (t -> B -> b) -> t -> Parser b pBD f p = f p <$> pBArg -- But omitting it leads to a type error if TypeFamilies is enabled. -- There is no error if TypeFamilies is not enabled. pFG :: Parser B -> Parser (D B) pFG pBArg = pBD GF AP <|> pBD DF AM where pBD f p = f p <$> pBArg -- The specifics of the parser don't matter data Parser a = Parser (<|>) :: Parser a -> Parser a -> Parser a (<|>) _ _ = Parser (<$>) :: (a -> b) -> Parser a -> Parser b (<$>) _ _ = Parser

Show replies by date

Richard Eisenberg

10 Feb 10 Feb

1:30 p.m.

This is the effect of -XMonoLocalBinds, which is implied by -XTypeFamilies (and also by -XGADTs). See https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_gene... https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_gene.... Happy to give more background -- let me know if that link doesn't answer your question. Richard

...

On Feb 10, 2021, at 6:31 AM, Tom Ellis wrote:

Dear all,

I don't understand why the type of pBD defined in the where clause of pFG cannot be inferred to a general type in the presence of TypeFamilies. In particular I don't understand why nonetheless the type of pBD definied in the where clause of pF (only slightly simpler) *can* be inferred.

Can anyone explain?

Thanks

Tom

{-# LANGUAGE TypeFamilies #-}

-- This code came up in the context of writing a parser, but that's -- not terribly important

import Prelude hiding ((<$>))

data B = B

data D f = F f | GF AP f | DF AM f

data AM = AM data AP = AP

pB :: Parser B pB = Parser

-- Works fine pF :: Parser (D B) pF = pBD GF AP <|> pBD DF AM where pBD f p = f p <$> pB

-- Shows the (presumably) inferred type for pBD pFWithType :: Parser (D B) pFWithType = pBD GF AP <|> pBD DF AM where pBD :: (t -> B -> b) -> t -> Parser b pBD f p = f p <$> pB

-- One would hope this type would be inferred too pFGWithType :: Parser B -> Parser (D B) pFGWithType pBArg = pBD GF AP <|> pBD DF AM where pBD :: (t -> B -> b) -> t -> Parser b pBD f p = f p <$> pBArg

-- But omitting it leads to a type error if TypeFamilies is enabled. -- There is no error if TypeFamilies is not enabled. pFG :: Parser B -> Parser (D B) pFG pBArg = pBD GF AP <|> pBD DF AM where pBD f p = f p <$> pBArg

-- The specifics of the parser don't matter data Parser a = Parser

(<|>) :: Parser a -> Parser a -> Parser a (<|>) _ _ = Parser

(<$>) :: (a -> b) -> Parser a -> Parser b (<$>) _ _ = Parser _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Tom Ellis

3:21 p.m.

I'm rather puzzled by that page. I"m not sure if I'm missing something. Firstly, I don't understand the definition of "variable is closed" and "binding group is fully generalised". Consider f = let x = x in () Is x closed? Well, according to the definition it is closed when * the variable is let-bound [It is] * one of the following holds: * the variable has an explicit type signature that has no free type variables [It does not] * its binding group is fully generalised (see next bullet) [OK, let's check the definition of "fully generalised"] Is x's binding group fully generalised? According to the definition is is fully generalised when * each of its free variables is either imported or closed, and [x is the only free variable. It is not imported. Is it closed? See below!] * the binding is not affected by the monomorphism restriction (Haskell Report, Section 4.5.5) [I don't believe it is -- no constrained variables are in play. See https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-930004....] Following these rules x is closed if and only if its binding group is fully generalised, and its binding group is fully generalised if and only if x is closed. At this point I don't know how to determine whether x is closed. Have I misinterpreted some part of this definition? Secondly, if I knew whether x is closed then what? Perhaps "fully generalised" is not just the name of a property that a binding group may have but something that is actually *performed* to the binding group, something to do with whether it is assigned a general type. Is that right? Tom On Wed, Feb 10, 2021 at 01:30:10PM +0000, Richard Eisenberg wrote:

...

This is the effect of -XMonoLocalBinds, which is implied by -XTypeFamilies (and also by -XGADTs). See https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_gene... https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_gene....

Happy to give more background -- let me know if that link doesn't answer your question.

Richard

...
On Feb 10, 2021, at 6:31 AM, Tom Ellis wrote: Dear all,

I don't understand why the type of pBD defined in the where clause of pFG cannot be inferred to a general type in the presence of TypeFamilies. In particular I don't understand why nonetheless the type of pBD definied in the where clause of pF (only slightly simpler) *can* be inferred.

Can anyone explain?

Thanks

Tom

{-# LANGUAGE TypeFamilies #-}

-- This code came up in the context of writing a parser, but that's -- not terribly important

import Prelude hiding ((<$>))

data B = B

data D f = F f | GF AP f | DF AM f

data AM = AM data AP = AP

pB :: Parser B pB = Parser

-- Works fine pF :: Parser (D B) pF = pBD GF AP <|> pBD DF AM where pBD f p = f p <$> pB

-- Shows the (presumably) inferred type for pBD pFWithType :: Parser (D B) pFWithType = pBD GF AP <|> pBD DF AM where pBD :: (t -> B -> b) -> t -> Parser b pBD f p = f p <$> pB

-- One would hope this type would be inferred too pFGWithType :: Parser B -> Parser (D B) pFGWithType pBArg = pBD GF AP <|> pBD DF AM where pBD :: (t -> B -> b) -> t -> Parser b pBD f p = f p <$> pBArg

-- But omitting it leads to a type error if TypeFamilies is enabled. -- There is no error if TypeFamilies is not enabled. pFG :: Parser B -> Parser (D B) pFG pBArg = pBD GF AP <|> pBD DF AM where pBD f p = f p <$> pBArg

-- The specifics of the parser don't matter data Parser a = Parser

(<|>) :: Parser a -> Parser a -> Parser a (<|>) _ _ = Parser

(<$>) :: (a -> b) -> Parser a -> Parser b (<$>) _ _ = Parser

Richard Eisenberg

11 Feb 11 Feb

2:46 a.m.

...

On Feb 10, 2021, at 10:21 AM, Tom Ellis wrote:

Is x's binding group fully generalised? According to the definition is is fully generalised when

* each of its free variables is either imported or closed, and

[x is the only free variable. It is not imported. Is it closed? See below!]

I argue: x is not a free variable of the binding group, because it is bound by the binding group. It *is* free in the RHS, but that's not what the manual says to look for.

...

Following these rules x is closed if and only if its binding group is fully generalised, and its binding group is fully generalised if and only if x is closed. At this point I don't know how to determine whether x is closed. Have I misinterpreted some part of this definition?

I think so, but it seems a pretty easy mistake to make.

...

Secondly, if I knew whether x is closed then what? Perhaps "fully generalised" is not just the name of a property that a binding group may have but something that is actually *performed* to the binding group, something to do with whether it is assigned a general type. Is that right?

Yes, that's right. Though I'm not sure what the content of the word *fully* is in that description -- I don't know of *partial* generalization. Does this help? Richard

...

Tom

On Wed, Feb 10, 2021 at 01:30:10PM +0000, Richard Eisenberg wrote:

...
This is the effect of -XMonoLocalBinds, which is implied by -XTypeFamilies (and also by -XGADTs). See https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_gene... https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_gene....

Happy to give more background -- let me know if that link doesn't answer your question.

Richard

...
On Feb 10, 2021, at 6:31 AM, Tom Ellis wrote: Dear all,

I don't understand why the type of pBD defined in the where clause of pFG cannot be inferred to a general type in the presence of TypeFamilies. In particular I don't understand why nonetheless the type of pBD definied in the where clause of pF (only slightly simpler) *can* be inferred.

Can anyone explain?

Thanks

Tom

{-# LANGUAGE TypeFamilies #-}

-- This code came up in the context of writing a parser, but that's -- not terribly important

import Prelude hiding ((<$>))

data B = B

data D f = F f | GF AP f | DF AM f

data AM = AM data AP = AP

pB :: Parser B pB = Parser

-- Works fine pF :: Parser (D B) pF = pBD GF AP <|> pBD DF AM where pBD f p = f p <$> pB

-- Shows the (presumably) inferred type for pBD pFWithType :: Parser (D B) pFWithType = pBD GF AP <|> pBD DF AM where pBD :: (t -> B -> b) -> t -> Parser b pBD f p = f p <$> pB

-- One would hope this type would be inferred too pFGWithType :: Parser B -> Parser (D B) pFGWithType pBArg = pBD GF AP <|> pBD DF AM where pBD :: (t -> B -> b) -> t -> Parser b pBD f p = f p <$> pBArg

-- But omitting it leads to a type error if TypeFamilies is enabled. -- There is no error if TypeFamilies is not enabled. pFG :: Parser B -> Parser (D B) pFG pBArg = pBD GF AP <|> pBD DF AM where pBD f p = f p <$> pBArg

-- The specifics of the parser don't matter data Parser a = Parser

(<|>) :: Parser a -> Parser a -> Parser a (<|>) _ _ = Parser

(<$>) :: (a -> b) -> Parser a -> Parser b (<$>) _ _ = Parser

Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Tom Ellis

2:23 p.m.

On Thu, Feb 11, 2021 at 02:46:46AM +0000, Richard Eisenberg wrote:

...

...
On Feb 10, 2021, at 10:21 AM, Tom Ellis wrote:

Is x's binding group fully generalised? According to the definition is is fully generalised when

* each of its free variables is either imported or closed, and

[x is the only free variable. It is not imported. Is it closed? See below!]

I argue: x is not a free variable of the binding group, because it is bound by the binding group. It *is* free in the RHS, but that's not what the manual says to look for.

Aha, thank you Richard, now I understand the definition. If one unrolls the recursiveness present in the definition then it seems to be saying saying that a let-bound group is generalised if and only if every trail of free variable dependencies eventually stops at a let-bound variable with an explicit type signature. In my example pFG the let-bound function pBD is *not* generalised because its free variable pBArg is not itself let-bound. -- Does not type check because pBD is not generalised yet it is -- used at two different types pFG :: Parser B -> Parser (D B) pFG pBArg = pBD GF AP <|> pBD DF AM where pBD f p = f p <$> pBArg On the other hand, my intuition says that we can let bind pBArg to a new name with explicit type signature and thereby make pBD closed. And indeed we can! -- Does type check pFG1 :: Parser B -> Parser (D B) pFG1 pBArg = pBD GF AP <|> pBD DF AM where pBArg1 :: Parser B pBArg1 = pBArg pBD f p = f p <$> pBArg1 My next question then is "In pFG, the argument pBArg has been given a type (moreover a monomorphic type) by the type signature for pFG itself. Why does the definition of 'closed' require the variable to be let-bound? Wouldn't lambda-bound with a type implicitly provided by an explicit type signature for the lambda" be equally good?" The fact that a simple, seemingly redundant, binding (that of pBArg1) makes a program type check is rather surprising. Thanks, Tom [...]

...

...
On Wed, Feb 10, 2021 at 01:30:10PM +0000, Richard Eisenberg wrote:

...
This is the effect of -XMonoLocalBinds, which is implied by -XTypeFamilies (and also by -XGADTs). See https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_gene... https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_gene....

Happy to give more background -- let me know if that link doesn't answer your question.

Richard

...
On Feb 10, 2021, at 6:31 AM, Tom Ellis wrote: Dear all,

I don't understand why the type of pBD defined in the where clause of pFG cannot be inferred to a general type in the presence of TypeFamilies. In particular I don't understand why nonetheless the type of pBD definied in the where clause of pF (only slightly simpler) *can* be inferred.

Can anyone explain?

Thanks

Tom

{-# LANGUAGE TypeFamilies #-}

-- This code came up in the context of writing a parser, but that's -- not terribly important

import Prelude hiding ((<$>))

data B = B

data D f = F f | GF AP f | DF AM f

data AM = AM data AP = AP

pB :: Parser B pB = Parser

-- Works fine pF :: Parser (D B) pF = pBD GF AP <|> pBD DF AM where pBD f p = f p <$> pB

-- Shows the (presumably) inferred type for pBD pFWithType :: Parser (D B) pFWithType = pBD GF AP <|> pBD DF AM where pBD :: (t -> B -> b) -> t -> Parser b pBD f p = f p <$> pB

-- One would hope this type would be inferred too pFGWithType :: Parser B -> Parser (D B) pFGWithType pBArg = pBD GF AP <|> pBD DF AM where pBD :: (t -> B -> b) -> t -> Parser b pBD f p = f p <$> pBArg

-- But omitting it leads to a type error if TypeFamilies is enabled. -- There is no error if TypeFamilies is not enabled. pFG :: Parser B -> Parser (D B) pFG pBArg = pBD GF AP <|> pBD DF AM where pBD f p = f p <$> pBArg

-- The specifics of the parser don't matter data Parser a = Parser

(<|>) :: Parser a -> Parser a -> Parser a (<|>) _ _ = Parser

(<$>) :: (a -> b) -> Parser a -> Parser b (<$>) _ _ = Parser

Richard Eisenberg

3:03 p.m.

...

On Feb 11, 2021, at 9:23 AM, Tom Ellis wrote:

"In pFG, the argument pBArg has been given a type (moreover a monomorphic type) by the type signature for pFG itself. Why does the definition of 'closed' require the variable to be let-bound? Wouldn't lambda-bound with a type implicitly provided by an explicit type signature for the lambda" be equally good?"

I think so, yes. Full disclosure: before this thread, I had never looked closely at the MonoLocalBinds definition. For years, I was operating under a simpler premise: "a local binding group is closed if all variables free in the group are bound at top-level". That is, any binding group that capture variables from the local definition would not be generalized. This interpretation means that your definition within pFG1 would also not be generalized. But my working definition was too limited, as the manual explains. Bottom line: I think you're right that we could do more generalization. I'm not sure how easy this would be to implement (I don't know how GHC tracks this information off the top of my head), but I do think it's worth filing a ticket to see if we can easily do better. Good conversation! I've learned something here. Thanks, Richard

Oleg Grenrus

3:14 p.m.

I also worked under the relaxed interpretation, and it is surprising to me that GHC does better. if GHC will do even better, I'd try to first formulate what that better is. "a local binding group is closed if all variables free in the group are bound at top-level" is somewhat understandable, adding further exceptions makes more programs to type-check, but if specifications becomes more cumbersome verifying that implementations does what specification advertises becomes more difficult. The "the variable has an explicit type signature that has no free type variables" additions seems arbitrary, it's not motivated in the manual. How much of the "real code" will break if it is removed? - Oleg On 11.2.2021 17.03, Richard Eisenberg wrote:

...

...
On Feb 11, 2021, at 9:23 AM, Tom Ellis mailto:tom-lists-haskell-cafe-2017@jaguarpaw.co.uk> wrote:

"In pFG, the argument pBArg has been given a type (moreover a monomorphic type) by the type signature for pFG itself. Why does the definition of 'closed' require the variable to be let-bound? Wouldn't lambda-bound with a type implicitly provided by an explicit type signature for the lambda" be equally good?"

I think so, yes.

Full disclosure: before this thread, I had never looked closely at the MonoLocalBinds definition. For years, I was operating under a simpler premise: "a local binding group is closed if all variables free in the group are bound at top-level". That is, any binding group that capture variables from the local definition would not be generalized. This interpretation means that your definition within pFG1 would also not be generalized. But my working definition was too limited, as the manual explains.

Bottom line: I think you're right that we could do more generalization. I'm not sure how easy this would be to implement (I don't know how GHC tracks this information off the top of my head), but I do think it's worth filing a ticket to see if we can easily do better.

Good conversation! I've learned something here.

Thanks, Richard

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Richard Eisenberg

3:28 p.m.

...

On Feb 11, 2021, at 10:14 AM, Oleg Grenrus wrote:

The "the variable has an explicit type signature that has no free type variables" additions seems arbitrary, it's not motivated in the manual. How much of the "real code" will break if it is removed?

A very good question. But I think one that's better to ask in a ticket, so we don't lose these pieces. The question is: do we want to be dumb but predictable, or clever but capricious? Tom seems to be moving toward the latter, while Oleg seems to moving toward the former. I tend to prefer dumb but predictable, too, but I don't know how much code would break. Right now, I think we're dumb and capricious, so that's an unhappy place to be. Richard

1607

Age (days ago)

1608

Last active (days ago)

List overview

Download

7 comments

3 participants

participants (3)

Oleg Grenrus
Richard Eisenberg
Tom Ellis