Re: [Haskell-cafe] Surprising lack of generalisation

11 Feb 2021

      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