# Type of callcc (Programming Languages)

From Spivey's Corner

The monad of continuations defines

Mα = (α →Answer) →Answer

and with this definition of *M*, I said that *callcc* has type

callcc:: ((α →Mβ) →Mα) →Mα

So expanding the definition of *M*, that becomes

callcc:: ((α → (β →Answer) →Answer) → (α →Answer) →Answer) → (α →Answer) →Answer

Its definition is

callccgk=ghkwherehxk'=kx

This function therefore does have the desirable property that its type is longer than its definition. To check that the type follows from the definition, we should first observe that (for fixed α and β), *g* and *k* have the types

g:: (α → (β →Answer) →Answer) → (α →Answer) →Answerk:: α →Answer

So the local function *h* has the type α → γ → *Answer* for any type γ, because it ignores its argument *k'*. In particular, we can give it the type

h:: α → (β →Answer) →Answer.

Thus *g* *h* has type (α → *Answer*) → *Answer*, and *g* *h* *k* has type *Answer* as required.