Lambda the Ultimate

Often restricted data types are used as jails. For example, the IO monad in Haskell can't let any impure value escape. Sometimes however, even though it is not safe to release any value from the jail in general it is possible for some specific values.

As an example, for some type T one might want to allow a function of the type "(T a -> T b) -> (a -> b)", but not a function of the type "T a -> a".

Another example, which is trivial, is that one might allow data of the type,(using Coq's notation for types where the values are constrained by propositions), "{ x : IO a | forsome y, x = pure y }" to escape where pure is the function of the type "a -> IO a".

What is it called when a data type can't be extracted from but a more complex data type built up from it can?

I know many of you are fans of Haskell. Here, SJP shares some history and describes how the language is evolving to meet the needs of modern general purpose computing (so, things like concurrency, parallelism). It's pretty amazing how far Haskell has come and where it seems to be heading.


Enjoy,
C