Looking back to that denotative future

[atravers]

@hellwolf

Could we at last simply let Haskell/Agda only do the declarative part, and let the runtime written by c++/rust/zig in the imperative language soup to figure out the dirty job of how to actually run them?

Actually, some implementations of early functional languages did use that arrangement:

One way to deal with this is the so called standard solution The purely
functional reduction machine is attached to a von Neumann host machine and an
imperative environment deals with I/O and interactive programs.

Functional programming and the language TALE (page 6 of 88).

It certainly seems to make sense: at that time, there were very few palatable ingredients for the “imperative language soup” - why would anyone allow that glop to ruin their delectable new declarative or denotative language? Imperativity begone!

But Haskell isn’t arranged in this way. Futhermore, languages which started with that arrangement rarely sustain it e.g. adding support for imperativity like I/O to Dhall have already been contemplated twice:

• Proposal: "Do notation" syntax - Dhall discussion

• A (failed) attempt at doing IO with Dhall - Dhall discussion

So the next time anyone suggests that shifting semantically imperative mechanisms out of the programming model and into the implementation is the solution, ask them to explain:

• why it didn’t work before,

• and why it should work now.