Type of callcc (Programming Languages)
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.