Skip to content

Instantly share code, notes, and snippets.

@beala

beala/cont_with_holes.md

Last active January 23, 2016 21:37
Show Gist options
  • Save beala/3361b984a46fe15a446e to your computer and use it in GitHub Desktop.
Save beala/3361b984a46fe15a446e to your computer and use it in GitHub Desktop.
Download ZIP
My experience using typed holes to implement Cont.
Raw
cont_with_holes.md

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 Conts 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!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment