[Haskell-cafe] Surprising lack of generalisation

[Richard Eisenberg]

> On Feb 10, 2021, at 10:21 AM, Tom Ellis <tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk> 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_generalisation.html <https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_generalisation.html>.
>> 
>> 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 <tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk> 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.