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.
nm shows symbols defined in an executable. GHC includes library name in
symbols, so we can use this to inspect libraries that make it into the compiled
binary. GHC uses z-encoding so we pipe the output of nm into an ad-hoc invocation of sed, viz.
GHC embeds linker flags into the final ELF binary:
I turned to my own Jacinda to view the output of otool and was pleasantly surprised.
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.
next