Help me understand `newtype AppM` from the Halogen tutorial

Help
,
#1

PureScript beginner here.

I’m building a small PureScript/Node application and I’m trying to use the ReaderT pattern which is also popular in Haskell and which is used in the excellent Halogen Real World Guide.

As I was going through the implementation of AppM I noticed that the types didn’t really line up, at least no in my head.

I started by lining up the signature for the new MonadAsk instance that we’re creating:

MonadAsk r m -- from Pursuit
MonadAsk e AppM -- what we're building

So m ~ AppM.

But the typed hole for asks from gives me (ReaderT Env Aff a). Since asks :: MonadAsk r m => (r -> a) -> m a, I concluded that

asks from :: m               a
?a        :: ReaderT Env Aff a

…and therefore m ~ ReaderT Env Aff. Now there are two options. Either I’ve kinda sorta understood how this works and the newtype being a newtype just “vanishes” and therefore the AppM in MonadAsk e AppM is really equivalent to its content, MonadAsk e ReaderT Env Aff or I have some really profound misunderstanding here.

Here’s the full snippet with hopefully all the required context.

newtype AppM a
  = AppM (ReaderT Env Aff a)

instance monadAskAppM :: TypeEquals e Env => MonadAsk e AppM where
  ask :: AppM e
  ask = AppM $ (asks from :: ?a)
#2

In this instance, asks from does have the type ReaderT e Aff Env, but that type is still distinct from AppM Env. Newtypes don’t “vanish”; the reason this works is that the AppM constructor takes you from ReaderT Env Aff a to AppM a. Note that these two m type variables are separate - they are bound in different places and so they don’t both need to be substituted with the same type.

#3

So where is the m in asks from :: m a bound and why does it have ReaderT e Aff Env? It’s been a while that I wrote Haskell and apparently all this intuitive knowledge is lost again.

#4

The type of asks from is

forall r s m.
  MonadAsk r m =>
  TypeEquals r s =>
  m s

and this m is bound in the type of asks from. When we use asks from inside another expression, we can choose the types we want for m, r, and s, as long as we can provide the necessary instances. In this case, we are using asks from as the argument to the AppM constructor, whose type is

forall a. ReaderT Env Aff a -> AppM a

which means that for this m, we will need to choose ReaderT Env Aff. The m in the MonadAsk instance we are defining is bound in the definition of the MonadAsk class, and is irrelevant here.

3 Likes
#5

I suppose “irrelevant” is maybe a bit strong. The m from MonadAsk is not relevant when checking that asks from is an acceptable argument to AppM. It is relevant, however, when checking that the definition of ask has the correct type according to the instance arguments, i.e. AppM e. In essence, the m from the MonadAsk class definition is only there to ensure that ask returns something in the right monad.

2 Likes
#6

Okay thanks, that was the missing puzzle piece. I had somehow maneuvered myself into this dead end where I mistakenly thought that m was the same for both the asks from call and also the overall instance. But it makes complete sense now that the m is something different in asks from, considering that we’re passing the result of asks from to AppM, which expects a ReaderT Env Aff a as its argument.

And therefore the MonadAsk r m as it applies to asks has m ~ ReaderT Env Aff whereas for the instance I’m creating, m ~ AppM.

Thanks for clearing this up!

2 Likes