This is a write up of my experience implementing the Functor, Applicative and Monad instances for
Cont
for the first time. What's notable is I used typed holes to guide me. By simply
responding to the types and ghci's feedback, I arrived at a correct implementation.
I start with the newtype
for Cont
(this is the only thing I looked up beforehand) and the
beginning of a Functor
instance. I know from the type of fmap
that I'll need to produce a Cont r b
, so I start with the Cont
constructor and a lambda with a hole
newtype Cont r a = Cont {runCont :: (a -> r) -> r}
instance Functor (Cont r) where
fmap f m = Cont $ \g -> _
Found hole ‘_’ with type: r
Where: ‘r’ is a rigid type variable bound by
the instance declaration at Cont.hs:6:10
Relevant bindings include
g :: b -> r (bound at Cont.hs:7:22)
m :: Cont r a (bound at Cont.hs:7:10)
f :: a -> b (bound at Cont.hs:7:8)
fmap :: (a -> b) -> Cont r a -> Cont r b (bound at Cont.hs:7:3)
In the expression: _
In the second argument of ‘($)’, namely ‘\ g -> _’
In the expression: Cont $ \ g -> _
ghci
tells me that I need to produce an r
, and that I have f
, g
, and m
available. I start
by unwrapping m
:
instance Functor (Cont r) where
fmap f m = let unM = runCont m in
Cont $ \g -> _
I still need to produce an r
, but unM
looks useful:
Relevant bindings include
g :: b -> r (bound at Cont.hs:8:22)
unM :: (a -> r) -> r (bound at Cont.hs:7:18)
m :: Cont r a (bound at Cont.hs:7:10)
f :: a -> b (bound at Cont.hs:7:8)
fmap :: (a -> b) -> Cont r a -> Cont r b (bound at Cont.hs:7:3)
unM
takes an a -> r
, and produces an r
, which is the type I need. Composing g
and f
will
give me an a -> r
so:
instance Functor (Cont r) where
fmap f m = let unM = runCont m in
Cont $ \g -> unM (g . f)
And I'm done.
Now for Applicative. I know pure
must produce a Cont r a
, so I again start with the Cont
constructor and half a lambda:
instance Applicative (Cont r) where
pure a = Cont $ \g -> _
ghci reports:
Found hole ‘_’ with type: r
Where: ‘r’ is a rigid type variable bound by
the instance declaration at Cont.hs:10:10
Relevant bindings include
g :: a -> r (bound at Cont.hs:11:20)
a :: a (bound at Cont.hs:11:8)
pure :: a -> Cont r a (bound at Cont.hs:11:3)
In the expression: _
In the second argument of ‘($)’, namely ‘\ g -> _’
In the expression: Cont $ \ g -> _
ghci almost writes the code for me: I need an r
and I have both an a
and and a -> r
in scope,
so I apply the two:
instance Applicative (Cont r) where
pure a = Cont $ \g -> g a
Now for <*>
. I start again with the Cont
constructor and half a lambda. I go ahead and unwrap
the two Cont
s that I have, remembering that I needed to do that in fmap
:
instance Applicative (Cont r) where
pure a = Cont $ \g -> g a
f <*> m = let unF = runCont f
unM = runCont m
in
Cont $ \g -> _
So once again I need an r
, but this time have quite a few things available to me:
Found hole ‘_’ with type: r
Where: ‘r’ is a rigid type variable bound by
the instance declaration at Cont.hs:10:10
Relevant bindings include
g :: b -> r (bound at Cont.hs:15:25)
unF :: ((a -> b) -> r) -> r (bound at Cont.hs:12:17)
unM :: (a -> r) -> r (bound at Cont.hs:13:17)
m :: Cont r a (bound at Cont.hs:12:9)
f :: Cont r (a -> b) (bound at Cont.hs:12:3)
(<*>) :: Cont r (a -> b) -> Cont r a -> Cont r b
(bound at Cont.hs:12:3)
In the expression: _
In the second argument of ‘($)’, namely ‘\ g -> _’
In the expression: Cont $ \ g -> _
I admit that I floundered here for a while. It looks like unF
could almost be appplied to unM
,
but the types don't quite line up. My breakthrough came when I tried applying unF
to half a
lambda.
instance Applicative (Cont r) where
pure a = Cont $ \g -> g a
f <*> m = let unF = runCont f
unM = runCont m
in
Cont $ \g -> unF (\g' -> _)
Found hole ‘_’ with type: r
Where: ‘r’ is a rigid type variable bound by
the instance declaration at Cont.hs:10:10
Relevant bindings include
g' :: a -> b (bound at Cont.hs:15:36)
g :: b -> r (bound at Cont.hs:15:25)
unF :: ((a -> b) -> r) -> r (bound at Cont.hs:12:17)
unM :: (a -> r) -> r (bound at Cont.hs:13:17)
m :: Cont r a (bound at Cont.hs:12:9)
f :: Cont r (a -> b) (bound at Cont.hs:12:3)
So I now have a g' :: a -> b
and g :: b -> r
. Those can produce an a -> r
when composed. This
is interesting because unM
can produce the type I need from an a -> r
. Putting those all
together:
instance Applicative (Cont r) where
pure a = Cont $ \g -> g a
f <*> m = let unF = runCont f
unM = runCont m
in
Cont $ \g -> unF (\g' -> unM (g . g'))
And I'm done.
For Monad, I start with the ususal tricks: (1) unwrapping anything of type Cont
, and (2) applying
Cont
to half a lambda:
instance Monad (Cont r) where
return = pure
m >>= f = let unM = runCont m
in
Cont $ \g -> _
As always, I need to produce an r
. I have a few things in scope:
Found hole ‘_’ with type: r
Where: ‘r’ is a rigid type variable bound by
the instance declaration at Cont.hs:17:10
Relevant bindings include
g :: b -> r (bound at Cont.hs:21:23)
unM :: (a -> r) -> r (bound at Cont.hs:19:17)
f :: a -> Cont r b (bound at Cont.hs:19:9)
m :: Cont r a (bound at Cont.hs:19:3)
(>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b
(bound at Cont.hs:19:3)
In the expression: _
In the second argument of ‘($)’, namely ‘\ g -> _’
In the expression: Cont $ \ g -> _
Remembering that applying unF
to a lambda with a hole was a breakthrough for Applicative, I go
ahead and try that on unM
instance Monad (Cont r) where
return = pure
m >>= f = let unM = runCont m
in
Cont $ \g -> unM (\g' -> _)
Found hole ‘_’ with type: r
Where: ‘r’ is a rigid type variable bound by
the instance declaration at Cont.hs:17:10
Relevant bindings include
g' :: a (bound at Cont.hs:21:34)
g :: b -> r (bound at Cont.hs:21:23)
unM :: (a -> r) -> r (bound at Cont.hs:19:17)
f :: a -> Cont r b (bound at Cont.hs:19:9)
m :: Cont r a (bound at Cont.hs:19:3)
(>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b
(bound at Cont.hs:19:3)
In the expression: _
In the first argument of ‘unM’, namely ‘(\ g' -> _)’
In the expression: unM (\ g' -> _)
It's not clear where to go from here, but I see that g' :: a
and f :: a -> Cont r b
. I apply
those and preemptively unwrap the resulting Cont r b
. I place a hole, knowing that the unwrapped
Cont
will need an argument:
instance Monad (Cont r) where
return = pure
m >>= f = let unM = runCont m
in
Cont $ \g -> unM (\g' -> runCont (f g') _ )
Found hole ‘_’ with type: b -> r
Where: ‘r’ is a rigid type variable bound by
the instance declaration at Cont.hs:17:10
‘b’ is a rigid type variable bound by
the type signature for
(>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b
at Cont.hs:19:5
Relevant bindings include
g' :: a (bound at Cont.hs:21:34)
g :: b -> r (bound at Cont.hs:21:23)
unM :: (a -> r) -> r (bound at Cont.hs:19:17)
f :: a -> Cont r b (bound at Cont.hs:19:9)
m :: Cont r a (bound at Cont.hs:19:3)
(>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b
(bound at Cont.hs:19:3)
In the second argument of ‘runCont’, namely ‘_’
In the expression: runCont (f g') _
In the first argument of ‘unM’, namely ‘(\ g' -> runCont (f g') _)’
I'm almost there! I need a b -> r
and lo and behold: g :: b -> r
.
instance Monad (Cont r) where
return = pure
m >>= f = let unM = runCont m
in
Cont $ \g -> unM (\g' -> runCont (f g') g )
Comparing these to implementations on [hackage](http://hackage.haskell.org/package/transformers-0.5.1.0/docs/src/Control-Monad-Trans-Cont. html#ContT), I appear to have gotten them correct. Incredible!