An established problem in functional programming is the question of evaluation
order (see Hudak, ยง2.2).
Haskell offers seq; which allows the programmer to magically introduce
dependencies in evaluation order and thence subvert lazy evaluation.
Sometimes this is necessary; see the foldl foldl' example.
Much like all dynamically typed languages are poor statically typed languages, typed functional programming languages (corresponding to intuitionistic logic) are subsumed by linear logic. Girard articulates this unity in the logical context. Let us gloss the functional programming side of things.
If we wish to preserve global uniqueness of names during \(\beta\)-reduction, we have to \(\alpha\)-rename before each substitution. Consider:
Haskell puts all side effects in the IO monad, which passes around the
RealWorld. This is unsatisfactory for a number of reasons, and Haskellers have spilled much ink on effects systems.
As I recently noted, there are
distinctions in how one handles effects at the logical level: in particular,
randomness is different from array writes.
C has a reputation for being a "hacker" language, in contrast to say Haskell, which is abstract with ties to logic and category theory. There is even the quip "C is a portable assembler".
next