Inferred type not as polymorphic as suggested

[danielkroeni]

Hi

I try to port the microlens package from Haskell to Frege. The following compiles with GHC:

{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE RankNTypes #-}

import Control.Applicative
import Control.Monad.Identity

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b
failing left right afb s = case pins t of
  [] -> right afb s
  _  -> un b afb
  where
    t = un b
    b = left sell s
    sell :: a -> Bazaar a b b
    sell w = Bazaar ($ w)
    pins f = getConst (f (\ra -> Const [Identity ra]))

data Bazaar a b t = Bazaar { un :: (forall f. Applicative f => (a -> f b) -> f t) }

instance Functor (Bazaar a b) where
  fmap f (Bazaar k) = Bazaar (fmap f . k)

instance Applicative (Bazaar a b) where
  pure a = Bazaar $ \_ -> pure a
  Bazaar mf <*> Bazaar ma = Bazaar $ \afb -> mf afb <*> ma afb

But this fails in Frege because the inferred type is not as polymorphic as it is expected:

import frege.data.wrapper.Identity
import frege.data.wrapper.Const

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b
failing left right afb s = case pins b of
   [] -> right afb s
   _  -> b afb       -- <---- HERE IT FAILS
  where
    (Bazaar b) = left sell s
    sell :: a -> Bazaar a b b
    sell w = Bazaar ($ w)
    pins f = Const.get (f (\ra -> Const [Identity ra]))


data Bazaar a b t = Bazaar { run :: forall f. Applicative f => (a -> f b) -> f t }

instance Functor (Bazaar a b) where
  fmap f (Bazaar k) = Bazaar (fmap f . k)

instance Applicative (Bazaar a b) where
  pure a = Bazaar (\_ -> pure a)
  Bazaar mf <*> Bazaar ma = Bazaar (\afb -> mf afb <*> ma afb)

Multiple messages at this line.
    -type error in expression b afb type is : Const [Identity a] t expected: f t
    -The inferred type must be at least as polymorphic as the annotated one.
    -type `Const [Identity t20370#a]` is not as polymorphic as suggested in the annotation where just `f` is 
     announced.
    -type error in expression afb type is : f b expected: Const [Identity a] b
    -The inferred type must be at least as polymorphic as the annotated one.
        ...

But this works:
(Note the change from matching on (Bazaar b) to accessing its content using b.run)

import frege.data.wrapper.Identity
import frege.data.wrapper.Const

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b
failing left right afb s = case pins b.run of
   [] -> right afb s
   _  -> b.run afb
  where
    b = left sell s
    sell :: a -> Bazaar a b b
    sell w = Bazaar ($ w)
    pins f = Const.get (f (\ra -> Const [Identity ra]))

data Bazaar a b t = Bazaar { run :: forall f. Applicative f => (a -> f b) -> f t }

instance Functor (Bazaar a b) where
  fmap f (Bazaar k) = Bazaar (fmap f . k)

instance Applicative (Bazaar a b) where
  pure a = Bazaar (\_ -> pure a)
  Bazaar mf <*> Bazaar ma = Bazaar (\afb -> mf afb <*> ma afb)

Is this a bug?

Thanks

[Ingo60]

No, it is not a bug, it is a consequence of Frege not generalizing let bindings.

Here is another way to remedy this:

failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b
failing left right afb s = case left sell s of
      Bazaar b -> case pins b of
                           [] -> right afb s
                           _  -> b afb       -- <---- works now
    where
       sell ∷ a → Bazaar a b b       -- not strictly needed
       sell w = Bazaar ($ w)
       pins f = Const.get (f (\ra -> Const [Identity ra]))

But the way you did it is superior, IMHO, and also matches the orginal code better.

Here is a small code that shows the basic issue:

foo = (myid true, myid 'c') where
    -- myid :: a -> a
    myid x = x

This will complain that Bool cannot be unified with Char.
However, in this case we can fix the situation by doing the generalisation by providing the type signature.

Note that it is not possible to give an annotation for b in your program, because we don't have scoped type variables in Frege.

Actually, Frege does here what GHC since 7.2 does with language pragma MonoLocalBindings, which is automaticaly activated whenever you have GADTs or type families (or -fglasgow-exts).
See the Haskel wiki for more info.

Incidentally, the original code defines t = un b and uses t as argument for pins and later uses un b (which corresponds to Frege b.run) explicitly, just two lines above the definition of t. You can tell now that you're an expert on let-generalisation that this is not just sloppiness of the author of the original Haskell code.

[danielkroeni]

Many thanks for your comprehensive answer. Next time I will ask on the mailing list before I open an issue.

Regarding sloppiness: The Haskell code I posted above which I claimed to be original was deformed by my own experiments. I am sorry for that.

The real original code looks like this:

failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b
failing left right afb s = case pins t of
  [] -> right afb s
  _  -> t afb
  where
    Bazaar t = left sell s
    sell w = Bazaar ($ w)
    pins f = getConst (f (\ra -> Const [Identity ra]))

newtype Bazaar a b t = Bazaar (forall f. Applicative f => (a -> f b) -> f t)

It seems to me that your alternative remedy fits the original code better. Would you agree?

[Ingo60]

I am actually surprised .... unless MonoLocalBindings is off in Haskell.

Another very likely possibility is that they do it in a more clever way, so that the knowledge that t was a polymorphic function remains intact, even if t is let bound.

Anyway, in Frege please remember that if you want a let bound identifier have a polymorphic type, you need to give a type annotation. There is only the case where this identifier is used only once, because then it simply gets inlined, so there is not let binding with mono-type either.

(Yes, this somehow doesn't feel right. But it's not going to change.)

[danielkroeni]

Didn't you just explain to me that MonoLocalBindings is off per default unless "GADTs or type families (or -fglasgow-exts)" is enabled? The link you provided agrees with this as well.

(Yes, this somehow doesn't feel right. But it's not going to change.)

Is there a technical reason or is it your philosophical stance on the matter? I am just curious.
Thanks again for your explanations.

[Ingo60]

Ok, but then I can't know whether they have -fglasgow-exts in their Makefile. But I see that I have to try it out for myself ....

For your question: SPJ points out in the paper "Lets shouldn't be generaliezd" that they found only very few cases where generalization was actually needed when they analyzed a huge code base. And in those cases, the fix was trivial. (Just like in our case.)

So, considering this and the facts that generalization is modestly expensive in the type checker and that more thane necessary general code can be very much slower at runtime compared with code specialized for a known type and especially when type classes are involved, I thought it was a good idea to follow SPJ here. Especially since we maybe want to have GADTs, too, in the future.

And here then comes the philosophical part: I find the multitude of language options a bit overdone in GHC. As it stands, it could happen that you write some code, it works fine, then later you add some data type with GADTs and turn the respective language option on, and -- boom -- code might fail to compile that previously did, even if it actually doesn't involve GADTs.

So my take on the matter is that there should be as few language options as possible, and certainly none that imply others, which may have surprising effects.

[danielkroeni]

But I see that I have to try it out for myself ....

No, you don't have to.

cortex:Desktop dk$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.10.2
cortex:Desktop dk$ cat failing.hs 
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE RankNTypes #-}

module Main where

import Control.Applicative
import Control.Monad.Identity

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b
failing left right afb s = case pins t of
  [] -> right afb s
  _  -> t afb
  where
    Bazaar t = left sell s
    sell w = Bazaar ($ w)
    pins f = getConst (f (\ra -> Const [Identity ra]))

infixl 5 `failing`

newtype Bazaar a b t = Bazaar (forall f. Applicative f => (a -> f b) -> f t)

instance Functor (Bazaar a b) where
  fmap f (Bazaar k) = Bazaar (fmap f . k)

instance Applicative (Bazaar a b) where
  pure a = Bazaar $ \_ -> pure a
  Bazaar mf <*> Bazaar ma = Bazaar $ \afb -> mf afb <*> ma afb

main :: IO ()
main = putStrLn "This compiles fine."
cortex:Desktop dk$ ghc failing.hs
[1 of 1] Compiling Main             ( failing.hs, failing.o )
Linking failing ...
cortex:Desktop dk$ 

It even compiles with MonoLocalBinds enabled!

cortex:Desktop dk$ cat failing.hs 
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MonoLocalBinds #-}

module Main where

import Control.Applicative
import Control.Monad.Identity

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b
failing left right afb s = case pins t of
  [] -> right afb s
  _  -> t afb
  where
    Bazaar t = left sell s
    sell w = Bazaar ($ w)
    pins f = getConst (f (\ra -> Const [Identity ra]))

infixl 5 `failing`

newtype Bazaar a b t = Bazaar (forall f. Applicative f => (a -> f b) -> f t)

instance Functor (Bazaar a b) where
  fmap f (Bazaar k) = Bazaar (fmap f . k)

instance Applicative (Bazaar a b) where
  pure a = Bazaar $ \_ -> pure a
  Bazaar mf <*> Bazaar ma = Bazaar $ \afb -> mf afb <*> ma afb

main :: IO ()
main = putStrLn "This compiles fine."
cortex:Desktop dk$ ghc failing.hs
[1 of 1] Compiling Main             ( failing.hs, failing.o )
Linking failing ...
cortex:Desktop dk$ 

Especially since we maybe want to have GADTs, too, in the future.

GADTs would be welcome!

As it stands, it could happen that you write some code, it works fine, then later you add some data type with GADTs and turn the respective language option on, and -- boom -- code might fail to compile that previously did, even if it actually doesn't involve GADTs.

I'm convinced! When working with software I don't like surprising effects either. I understand your line of reasoning and it is okay for me to use the proposed workaround.
Thanks again.

[danielkroeni]

The LetGeneralisationInGhc7 link you mentioned states that MonoLocalBinds is now default.

Here's the rule. With -XMonoLocalBinds (the default), a binding without a type signature is generalised only if all its free variables are closed.

A binding is closed if and only if

• It has a type signature, and the type signature has no free variables; or
• It has no type signature, and all its free variables are closed, and it is unaffected by the monomorphism restriction. And hence it is fully generalised.

Since sell w = Bazaar ($ w) is closed because it has no free variables and left and s are closed because they have a type signature it follows that Bazaar t = left sell s is closed as well and thus will be generalised. Does this make any sense?

It takes a while to become an expert in let-bindings..

[Ingo60]

Well, this explains the difference. Frege rules are much simpler: If it does have a type signature, it is already as general as the user wants it. So just check that type. Otherwise, give it a mono-type. That's all!