Re: [Haskell-cafe] Surprising lack of generalisation

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.

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

---

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.