[Haskell-cafe] Surprising lack of generalisation

[Tom Ellis]

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.5.5]


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_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