Re: [Haskell-cafe] Surprising lack of generalisation

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