4 ms·

The usual definitions of imperative vs functional are that imperative is built from Hoare triples and functional is built from lambda calculus. By those definit

The usual definitions of imperative vs functional are that imperative is built from Hoare triples and functional is built from lambda calculus. By those definitions, you cannot have a functional, imperative language.

austincheney 8y ago
When used properly the nested scope provided by lambda calculus allows shared variables accessible from outside a local function thereby accounting for the precondition of Hoare's triples without it being locally present or passed in. This is enough to satisfy both the functional nature of portablity/isolation and the imperative model by Hoare's logic. * https://en.wikipedia.org/wiki/Hoare_logic https://en.wikipedia.org/wiki/Hoare_logic * https://en.wikipedia.org/wiki/Imperative_programming https://en.wikipedia.org/wiki/Imperative_programming * https://en.wikipedia.org/wiki/Scope_(computer_science)#Lexical_scoping https://en.wikipedia.org/wiki/Scope_(computer_science)#Lexic...
- madhadron 8y ago
  > When used properly the nested scope provided by lambda calculus allows shared variables accessible from outside a local function thereby accounting for the precondition of Hoare's triples without it being locally present or passed in. Yes, you can express any Turing complete system in terms of any other Turing complete system. > This is enough to satisfy both the functional nature of portablity/isolation and the imperative model by Hoare's logic. I think you're missing the point. It's not about portability or isolation. It's about the mathematical system you use as the foundation of your semantics. Yes, you can implement a lambda calculus in turns of Hoare triples and you can implement Hoare triples in terms of lambda calculus. Or in terms of unification over Horn clauses or combinatory logic. What makes a language functional is that its semantics are defined as an extension of the lambda calculus. What makes a language logical is that its semantics are defined as an extension of unification over Horn clauses. All the benefits people suggest to using one style or another are theorems, not definitions.
  - austincheney 8y ago
    > It's about the mathematical system you use as the foundation of your semantics. I think you are conflating lexical scope with functional programming. Lexical scope applies even without functions, but functional programming requires functions. The difference between a scoped block and function is that functions have identity and the scoped block does not even though both benefit fully from lexical scope. What makes a language functional is whether components are composable via function. That could mean several different things, such as: lexical scope, first class citizens, recursion by reference, callbacks, and so forth. A simple way to thinking about it is things are well separated, sometimes atomically and sometimes in a taxonomical fashion, but that separation has identity. That is very different than an OOP model where things are extended and put together and that togetherness or extension has no identity.

austincheney 8y ago

When used properly the nested scope provided by lambda calculus allows shared variables accessible from outside a local function thereby accounting for the precondition of Hoare's triples without it being locally present or passed in. This is enough to satisfy both the functional nature of portablity/isolation and the imperative model by Hoare's logic. * https://en.wikipedia.org/wiki/Hoare_logic https://en.wikipedia.org/wiki/Hoare_logic * https://en.wikipedia.org/wiki/Imperative_programming https://en.wikipedia.org/wiki/Imperative_programming * https://en.wikipedia.org/wiki/Scope_(computer_science)#Lexical_scoping https://en.wikipedia.org/wiki/Scope_(computer_science)#Lexic...

madhadron 8y ago
> When used properly the nested scope provided by lambda calculus allows shared variables accessible from outside a local function thereby accounting for the precondition of Hoare's triples without it being locally present or passed in. Yes, you can express any Turing complete system in terms of any other Turing complete system. > This is enough to satisfy both the functional nature of portablity/isolation and the imperative model by Hoare's logic. I think you're missing the point. It's not about portability or isolation. It's about the mathematical system you use as the foundation of your semantics. Yes, you can implement a lambda calculus in turns of Hoare triples and you can implement Hoare triples in terms of lambda calculus. Or in terms of unification over Horn clauses or combinatory logic. What makes a language functional is that its semantics are defined as an extension of the lambda calculus. What makes a language logical is that its semantics are defined as an extension of unification over Horn clauses. All the benefits people suggest to using one style or another are theorems, not definitions.
- austincheney 8y ago
  > It's about the mathematical system you use as the foundation of your semantics. I think you are conflating lexical scope with functional programming. Lexical scope applies even without functions, but functional programming requires functions. The difference between a scoped block and function is that functions have identity and the scoped block does not even though both benefit fully from lexical scope. What makes a language functional is whether components are composable via function. That could mean several different things, such as: lexical scope, first class citizens, recursion by reference, callbacks, and so forth. A simple way to thinking about it is things are well separated, sometimes atomically and sometimes in a taxonomical fashion, but that separation has identity. That is very different than an OOP model where things are extended and put together and that togetherness or extension has no identity.