When is a generic function not generic?

Question

I'm working on a Haskell server using scotty and persistent. Many handlers need access to the database connection pool, so I've taken to passing the pool around throughout the app, in this sort of fashion:

main = do
    runNoLoggingT $ withSqlitePool ":memory:" 10 $ \pool ->
        liftIO $ scotty 7000 (app pool)

app pool = do
    get "/people" $ do
        people <- liftIO $ runSqlPool getPeople pool
        renderPeople people
    get "/foods" $ do
        food <- liftIO $ runSqlPool getFoods pool
        renderFoods food

where getPeople and getFoods are appropriate persistent database actions that return [Person] and [Food] respectively.

The pattern of calling liftIO and runSqlPool on a pool becomes tiresome after a while - wouldn't it be great if I could refactor them into a single function, like Yesod's runDB, which would just take the query and return the appropriate type. My attempt at writing something like this is:

runDB' :: (MonadIO m) => ConnectionPool -> SqlPersistT IO a -> m a
runDB' pool q = liftIO $ runSqlPool q pool

Now, I can write this:

main = do
    runNoLoggingT $ withSqlitePool ":memory:" 10 $ \pool ->
        liftIO $ scotty 7000 $ app (runDB' pool)

app runDB = do
    get "/people" $ do
        people <- runDB getPeople
        renderPeople people
    get "/foods" $ do
        food <- runDB getFoods
        renderFoods food

Except that GHC complains:

Couldn't match type `Food' with `Person'
Expected type: persistent-2.1.1.4:Database.Persist.Sql.Types.SqlPersistT
                 IO
                 [persistent-2.1.1.4:Database.Persist.Class.PersistEntity.Entity
                    Person]
  Actual type: persistent-2.1.1.4:Database.Persist.Sql.Types.SqlPersistT
                 IO
                 [persistent-2.1.1.4:Database.Persist.Class.PersistEntity.Entity
                    Food]
In the first argument of `runDB', namely `getFoods'

It seems like GHC is saying that in fact the type of runDB becomes specialised somehow. But then how are functions like runSqlPool defined? Its type signature looks similar to mine:

runSqlPool :: MonadBaseControl IO m => SqlPersistT m a -> Pool Connection -> m a

but it can be used with database queries that return many different types, as I was doing originally. I think there's something fundamental I'm misunderstanding about types here, but I have no idea how to find out what it is! Any help would be greatly appreciated.

EDIT:

at Yuras' suggestion, I've added this:

type DBRunner m a = (MonadIO m) => SqlPersistT IO a -> m a
runDB' :: ConnectionPool -> DBRunner m a
app :: forall a. DBRunner ActionM a -> ScottyM ()

which required -XRankNTypes for the typedef. However, the compiler error is still identical.

EDIT:

Victory to the commentors. This allows the code to compile:

app :: (forall a. DBRunner ActionM a) -> ScottyM ()

For which I'm grateful, but still mystified!

The code is currently looking like this and this.

Neoteny

Try to add type signature to app with explicit forall and most likely you'd see what is wrong. – Valaree

@Valaree I think part of this problem is that I currently have a very poor understanding of explicit forall, but I shall endeavor to do so. – Neoteny

I guess it should be app :: (forall a. DBRunner ActionM a) -> ScottyM (). – Theatheaceous

@TomEllis should I have any particular extension enabled for that? It still gives me the same error. EDIT: okay, apologies - I had my handlers in separate functions. After adding type signatures there, and enabling more extensions (RankNTypes and FlexibleContexts) as required I'm starting to see new errors. Will report back. – Neoteny

Can you post your complete code? I'd like to try things out but I don't want to guess what your imports are, etc.. – Theatheaceous

@TomEllis I'm working on this, but the runDB stuff hasn't been pushed because obviously it isn't working :P. I can try to make a minimal example if you'd like. – Neoteny

@TomEllis it appears to be working now! I'll edit my question with current code. I'm still fairly mystified. – Neoteny

I would also suggest getting rid of the type and just using app :: MonadIO m => (forall a. SqlPersistT IO a -> m a) -> ScottyM (). I don't think the constraint has to be inside the forall. – Theatheaceous

@TomEllis I prefer having some sort of typedef to keep things brief and readable, especially since it will appear in the type of every handler (of which there are many :P). I'm going to see if I can stick the forall in the typedef too... – Neoteny

Possible duplicate of #3071636? But to keep things in place: your first runDB call in app set the type variable a in DBRunner m a to Entity People. Therefore, the type checker assumes runDB :: DBRunner ActionM (Entity People). However, your second use of runDB implies runDB :: DBRunner ActionM (Entity Food)! Oh noez! You have to tell GHC that runDB should take any a. And that's done with (forall a . DBRunner ActionM a) ->. Note the parentheses, the forall may not float out. – Brout

@Brout that question looks very familiar from back when I was reading about forall in connection with ST. Seems it didn't sink in - but I'm still confused why runDB needs forall but runSqlPool doesn't. – Neoteny

Because runSqlPool comes from the top level. If you try to pass it in as an argument you will experience the same problem. Alternatively if you write runDB = runDB' pool and app both inside a where clause in the body of the main then you will not need Rank2Types. – Theatheaceous

"SQlite"? :( That should be either "Sqlite" or "SQLite". – Ovular

Answer 1

It seems like GHC is saying that in fact the type of runDB becomes specialised somehow.

Your guess is right. Your original type was app :: (MonadIO m) => (SqlPersistT IO a -> m a) -> ScottyM (). This means that your runDB argument of type SqlPersistT IO a -> m a can be used at any one type a. However, the body of app wants to use the runDB argument at two different types (Person and Food) so instead we need to pass an argument that can work for any number of different types in the body. Thus app needs the type

app :: MonadIO m => (forall a. SqlPersistT IO a -> m a) -> ScottyM ()

(I would suggest keeping the MonadIO constraint outside the forall but you can also put it inside.)

EDIT:

What's going on behind the scenes is the following:

(F a -> G a) -> X means forall a. (F a -> G a) -> X, which means /\a -> (F a -> G a) -> X. /\ is the type-level lambda. That is, the caller gets to pass in a single type a and a function of type F a -> G a for that particular choice of a.

(forall a. F a -> G a) -> X means (/\a -> F a -> G a) -> X and the caller has to pass in a function which the callee can specialise to many choices of a.

Theatheaceous

But how does that interact with the intuitive way that having a generic function can act on multiple types? Why can runSqlPool return different types? Is there a forall somewhere in persistent's bowels that I just can't see? – Neoteny

@DanielBuckmaster: Nah. runSqlPool works for the same reason f = head ["Hi"] ++ (show $ head [1..5]) works. However, if you were to use runSqlPool as a parameter in order to get different a, you would encounter the same issue - the a gets fixed at the first encounter. – Brout

@Brout I see, so passing it as a parameter fixes its type. That makes sense, and I have to pass runDB because it relies on a pool that is constructed at runtime. I could not define runDB (with no ') as a library function, only runDB'. That's the difference with runSqlPool, I guess. – Neoteny

Answer 2

Lets play the game:

Prelude> let f str = (read str, read str)
Prelude> f "1" :: (Int, Float)
(1,1.0)

Works as expected.

Prelude> let f str = (read1 str, read1 str) where read1 = read
Prelude> f "1" :: (Int, Float)
(1,1.0)

Works too.

Prelude> let f read1 str = (read1 str, read1 str)
Prelude> f read "1" :: (Int, Float)

<interactive>:21:1:
    Couldn't match type ‘Int’ with ‘Float’
    Expected type: (Int, Float)
      Actual type: (Int, Int)
    In the expression: f read "1" :: (Int, Float)
    In an equation for ‘it’: it = f read "1" :: (Int, Float)

But this doesn't. What the difference?

The last f has the next type:

Prelude> :t f
f :: (t1 -> t) -> t1 -> (t, t)

So it doesn't work for clear reason, both elements of the tuple should have the same type.

The fix is like that:

Prelude> :set -XRankNTypes 
Prelude> let f read1 str = (read1 str, read1 str); f :: (Read a1, Read a2) => (forall a . Read a => str -> a) -> str -> (a1, a2)
Prelude> f read "1" :: (Int, Float)
(1,1.0)

Unlikely I can come with good explanation of RankNTypes, so I'd not even try. There is enough resources in web.

Valaree

Thanks, this is the sort of logic I'm trying to go through in my head. I'll look up RankNTypes to see if I can make sense of it. – Neoteny

Answer 3

To really answer the title question that apparently continues to mystify you: Haskell always chooses the most generic rank-1 type for a function, when you don't supply an explicit signature. So for app in the expression app (runDB' pool), GHC would attempt to have type

app :: DBRunner ActionM a -> ScottyM ()

which is in fact shorthand for

app :: forall a. ( DBRunner ActionM a -> ScottyM () )

This is rank-1 polymorphic, because all type variables are introduced outside of the signature (there is no quantification going on in the signature itself; the argument DBRunner ActionM a is in fact monomorphic since a is fixed at that point). Actually, it is the most generic type possible: it can work with a polymorphic argument like (runDB' pool), but would also be ok with monomorphic arguments.

But it turns out the implementation of app can't offer that generality: it needs a polymorphic action, otherwise it can't feed two different types of a values to that action. Therefore you need to manually request the more specific type

app :: (forall a. DBRunner ActionM a) -> ScottyM ()

which is rank-2, because it has a signature which contains a rank-1 polymorphic argument. GHC can't really know this is the type you want – there's no well defined “most general possible rank-n type” for an expression, since you can always push in extra quantifiers. So you must manually specify the rank-2 type.

Wilton

This, combined with Tom Ellis's explanation of forall as introducing a type-level lambda, has really helped me. Thanks for going to the trouble! – Neoteny