[Haskell-cafe] Surprising lack of generalisation

[Tom Ellis]

On Thu, Feb 11, 2021 at 02:46:46AM +0000, Richard Eisenberg wrote:
> > 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.

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