# Type of callcc (Programming Languages)

Jump to navigation
Jump to search

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

*callcc**g**k*=*g**h**k**where**h**x**k'*=*k**x*

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*) →*Answer**k*:: α →*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.