A Functional Programming Influence Graph • Hacker News Board

Re: A Functional Programming Influence Graph

#41

Post by DanWaterworth » Thu, May 03, 2012, 6:32 AM UTC

Locke1689 wrote: post #40

omaranto wrote: post #36

Earlier quoted context omitted.

In the dependently typed family of languages it's a little bit arbitrary to divide between programming languages and proof assistants since everyone in this space can be made to play both roles in a pinch. I think most people think of Coq as more on the proof assistant side and Agda more on the programming language side.

Sort of. Dependent types doesn't explain Coq's requirement for pure, total functions. Unless this restriction is weakened I cannot see it as being useful in any general-purpose domain. Agda may be looser.

> Dependent types doesn't explain Coq's requirement for pure, total functions.

That's where you are wrong. Partial functions introduce the bottom value and then you can 'prove' arbitrary incorrect things.

Re: A Functional Programming Influence Graph

#42

Post by Locke1689 » Thu, May 03, 2012, 7:23 AM UTC

DanWaterworth wrote: post #41

Locke1689 wrote: post #40

Earlier quoted context omitted.

Sort of. Dependent types doesn't explain Coq's requirement for pure, total functions. Unless this restriction is weakened I cannot see it as being useful in any general-purpose domain. Agda may be looser.

> Dependent types doesn't explain Coq's requirement for pure, total functions. That's where you are wrong. Partial functions introduce the bottom value and then you can 'prove' arbitrary incorrect things.

I'm not sure what you're saying. I was saying that simply being dependently typed doesn't necessitate pure total functions. Obviously, these features can be considered either highly suggested or necessary for ITPs. There are a number of ways you can get around totality with dependent types.

Re: A Functional Programming Influence Graph

#43

Post by idupree » Thu, May 03, 2012, 7:39 AM UTC

kibwen wrote: post #19

Perhaps there ought to be a single square to represent all languages that aren't traditionally considered functional languages, to represent the influence that functional languages have had on the rest of the language ecosystem. For example, I'd say Erlang's concurrency model influenced both Go and Rust (and Rust would inherit from both SML and Haskell as well).

Python borrowed list-comprehensions from Haskell et al.

Lexically scoped closures are from Scheme* and virtually all modern languages have them now. (Well, C++ and Java are late on the lambda boat, but C++11 and it seems Java 8 are getting them.) That's a huge influence.

* Scheme was the first Lisp to gain lexical scope, and C of course has lexical scope but not closures, but what's the full history here? It's also part of the lambda calculus.

Re: A Functional Programming Influence Graph

#44

Post by soc88 » Fri, May 04, 2012, 6:46 PM UTC

fogus wrote: post #11

dons wrote: post #9

Earlier quoted context omitted.

My guess was that it was going to be the container library, rather than the language itself. If libraries are included, then Clojure-inspired HAMTs are in Haskell as well. But really, Clojure, Haskell and Scala are all just implementing Bagwell's ideas, http://lampwww.epfl.ch/papers/idealhashtrees.pdf whose feasibility was shown in Clojure. See e.g. for Haskell, originally as http://www.haskell.org/pipermail/haskell-…

> My guess was that it was going to be the > container library, rather than the language itself. This walks a thin line for sure and in Scala the line is almost microscopic. I'll keep it for now since my reasoning was the same as the Erlang->Scala influence. A core language library that is rarely viewed as other than a core feature.

I disagree with that. There is great attention between language features and functionality shipped in the standard library. This http://clojure.com/blog/2012/04/19/take5-daniel-spiewak.html might also be of interest.