A Functional Programming Influence Graph • Hacker News Board

Re: A Functional Programming Influence Graph

#31

Post by olliesaunders » Wed, May 02, 2012, 11:00 PM UTC

Locke1689 wrote: post #29

olliesaunders wrote: post #28

Anyone here use Qi, Mercury, or Agda? I’m interested in what people think of those languages.

Agda is a proof assistant. I've used Coq, but not Agda -- I imagine they're similar. You wouldn't use it for general development. Qi is interesting but the development community is much smaller than its competitors (mainly Haskell). You probably want to look into Shen, not Qi. Qi development has mostly stalled.

Why wouldn’t you use it Agda/Coq for general development? (Looking for reasons other than a presumed lack of libraries.)

Re: A Functional Programming Influence Graph

#32

Post by Locke1689 » Wed, May 02, 2012, 11:03 PM UTC

olliesaunders wrote: post #31

Locke1689 wrote: post #29

Earlier quoted context omitted.

Agda is a proof assistant. I've used Coq, but not Agda -- I imagine they're similar. You wouldn't use it for general development. Qi is interesting but the development community is much smaller than its competitors (mainly Haskell). You probably want to look into Shen, not Qi. Qi development has mostly stalled.

Why wouldn’t you use it Agda/Coq for general development? (Looking for reasons other than a presumed lack of libraries.)

It's very slow and every function must have formal properties, e.g. all functions are total and must formally be proved to terminate.

(As far as I know. I've only worked through Pierce's book.)

Re: A Functional Programming Influence Graph

#33

Post by davidmathers » Wed, May 02, 2012, 11:20 PM UTC

A presentation by SPJ left me with the impression that FP should be pointing to Miranda and several other languages that became Haskell, rather than to Haskell itself.

Re: A Functional Programming Influence Graph

#34

Post by Locke1689 » Wed, May 02, 2012, 11:36 PM UTC

olliesaunders wrote: post #30

chimeracoder wrote: post #27

Earlier quoted context omitted.

That'd may be hard, because there's no canonical 'original' Lisp (there were a few similar, but incomplete/incompatible versions), and more importantly, there's no clear definition of what even is a Lisp. I mean, from the ones shown, it's sort of obvious, but I'm thinking in general. Also, Common Lisp, Racket, and Clojure are different enough that they count as separate languages in their own right, rather than 'vari…

> more importantly, there's no clear definition of what even is a Lisp. How about: If you program in it using s-expressions, it’s a Lisp.

Qi uses S-Expressions but it's got strong typing, pattern matching, and optional lazy evaluation. Sounds a lot more like Haskell than Scheme to me.

I'm not sure there is such a thing as a "Lisp." If you mean S-expression language, just say s-expression language. Wedging in Lisp as a substitute conflates the issue.

Re: A Functional Programming Influence Graph

#35

Post by fusiongyro » Wed, May 02, 2012, 11:37 PM UTC

olliesaunders wrote: post #28

Anyone here use Qi, Mercury, or Agda? I’m interested in what people think of those languages.

I have tried Mercury a few times. Prolog sans REPL is no use to me. I'm interested in Agda but haven't put much effort into it.

Re: A Functional Programming Influence Graph

#36

Post by omaranto » Wed, May 02, 2012, 11:46 PM UTC

Locke1689 wrote: post #29

olliesaunders wrote: post #28

Anyone here use Qi, Mercury, or Agda? I’m interested in what people think of those languages.

Agda is a proof assistant. I've used Coq, but not Agda -- I imagine they're similar. You wouldn't use it for general development. Qi is interesting but the development community is much smaller than its competitors (mainly Haskell). You probably want to look into Shen, not Qi. Qi development has mostly stalled.

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.

Re: A Functional Programming Influence Graph

#37

Post by [deleted] » Thu, May 03, 2012, 2:33 AM UTC

dons wrote: post #3

turnersr wrote: post #2

I think www.classes.cs.uchicago.edu/current/22300-1/lectures/FP_history.pdf is a better graph because it focuses more on functional languages and the layout is easier to navigate.

a) it focuses /less/ on functional languages, since it includes many fewer. The nice one about this graph is that it is relatively complete.

[deleted]

Re: A Functional Programming Influence Graph

#38

Post by lukeschlather » Thu, May 03, 2012, 2:35 AM UTC

fogus wrote: post #4

turnersr wrote: post #2

I think www.classes.cs.uchicago.edu/current/22300-1/lectures/FP_history.pdf is a better graph because it focuses more on functional languages and the layout is easier to navigate.

That is a very nice graph. I was shooting for a more comprehensive graph, but as you see at the cost of comprehension.

Why did you include Fortran and Algol? I'm curious what warrants their inclusion, but not BASIC or ADA or a variety of other languages... they certainly don't meet the textbook definition of "functional."

Re: A Functional Programming Influence Graph

#39

Post by tikhonj » Thu, May 03, 2012, 3:18 AM UTC

olliesaunders wrote: post #30

chimeracoder wrote: post #27

Earlier quoted context omitted.

That'd may be hard, because there's no canonical 'original' Lisp (there were a few similar, but incomplete/incompatible versions), and more importantly, there's no clear definition of what even is a Lisp. I mean, from the ones shown, it's sort of obvious, but I'm thinking in general. Also, Common Lisp, Racket, and Clojure are different enough that they count as separate languages in their own right, rather than 'vari…

> more importantly, there's no clear definition of what even is a Lisp. How about: If you program in it using s-expressions, it’s a Lisp.

Logo is a Lisp and yet does not really use s-expressions, and even has infix operators.

Now, you might argue that means Logo is not a Lisp, but it is actually extremely similar to basic Scheme. You could turn an interpreter for one into an interpreter for the other with mostly minor tweaks. It's also a dialect of Lisp historically.

Re: A Functional Programming Influence Graph

#40

Post by Locke1689 » Thu, May 03, 2012, 5:00 AM UTC

omaranto wrote: post #36

Locke1689 wrote: post #29

Earlier quoted context omitted.

Agda is a proof assistant. I've used Coq, but not Agda -- I imagine they're similar. You wouldn't use it for general development. Qi is interesting but the development community is much smaller than its competitors (mainly Haskell). You probably want to look into Shen, not Qi. Qi development has mostly stalled.

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.