Content deleted Content added
m fix errant calculation of proportions Tags: Visual edit Mobile edit Mobile web edit |
Masterzora (talk | contribs) Fix CS1 template errors. Turn bare-url into proper citation. |
||
Line 8:
Functional programming is sometimes treated as synonymous with [[purely functional programming]], a subset of functional programming which treats all functions as [[Deterministic system|deterministic]] mathematical [[Function (mathematics)|functions]], or [[pure function]]s. When a pure function is called with some given arguments, it will always return the same result, and cannot be affected by any mutable [[State (computer science)|state]] or other [[Side effect (computer science)|side effects]]. This is in contrast with impure [[Procedure (computer science)|procedures]], common in [[imperative programming]], which can have side effects (such as modifying the program's state or taking input from a user). Proponents of purely functional programming claim that by restricting side effects, programs can have fewer [[Software bug|bugs]], be easier to [[Debugging|debug]] and [[Software testing|test]], and be more suited to [[formal verification]].<ref name="hudak1989">{{cite journal |last=Hudak |first=Paul |author-link=Paul Hudak |title=Conception, evolution, and application of functional programming languages |journal=ACM Computing Surveys |volume=21 |issue=3 |pages=359–411 |date=September 1989 |url=http://www.dbnet.ece.ntua.gr/~adamo/languages/books/p359-hudak.pdf |doi=10.1145/72551.72554 |s2cid=207637854 |accessdate=2013-08-10 |archivedate=2016-01-31 |archiveurl=https://web.archive.org/web/20160131083528/http://www.dbnet.ece.ntua.gr/~adamo/languages/books/p359-hudak.pdf |url-status=deviated }}</ref><ref name="hughesWhyFPMatters"/>
Functional programming has its roots in [[academia]], evolving from the [[lambda calculus]], a formal system of computation based only on functions. Functional programming has historically been less popular than imperative programming, but many functional languages are seeing use today in industry and education, including [[Common Lisp]], [[Scheme (programming language)|Scheme]],<ref name="clinger1987"/><ref name="hartheimer1987"/><ref name="kidd2007"/><ref name="cleis2006"/> [[Clojure]], [[Wolfram Language]],<ref name="reference.wolfram.com">{{cite web |title=Wolfram Language Guide: Functional Programming |url=http://reference.wolfram.com/language/guide/FunctionalProgramming.html |year=2015 |access-date=2015-08-24}}</ref><ref name="Amath-CO"/> [[Racket (programming language)|Racket]],<ref name="racket-video-games"/> [[Erlang (programming language)|Erlang]],<ref name="erlang-faq"/><ref name="armstrong2007"/><ref name="larson2009"/> [[Elixir (programming language)|Elixir]],<ref>{{Cite web|title=The Elixir Programming Language|url=https://elixir-lang.org/|access-date=2021-02-14}}</ref> [[OCaml]],<ref name="minksy2008"/><ref name="leroy2007"/> [[Haskell]],<ref name="haskell-industry"/><ref name="hudak2007"/> and [[F Sharp (programming language)|F#]].<ref name="quantFSharp">{{cite conference |last=Mansell |first=Howard |title=Quantitative Finance in F# |url=http://cufp.galois.com/2008/abstracts.html#MansellHoward |year=2008 |conference=CUFP 2008 |access-date=2009-08-29 |archivedate=2015-07-08 |archiveurl=https://web.archive.org/web/20150708125937/http://cufp.galois.com/2008/abstracts.html#MansellHoward |url-status=dead }}</ref><ref name="businessAppsFSharp">{{cite conference |last=Peake |first=Alex |title=The First Substantial Line of Business Application in F# |url=http://cufp.galois.com/2009/abstracts.html#AlexPeakeAdamGranicz |year=2009 |conference=CUFP 2009 |access-date=2009-08-29 |archive-url=https://web.archive.org/web/20091017070140/http://cufp.galois.com/2009/abstracts.html#AlexPeakeAdamGranicz |archive-date=2009-10-17 |url-status=dead }}</ref> [[Lean (proof assistant)|Lean]] is a functional programming language commonly used for verifying mathematical theorems.<ref>
== History ==
Line 108:
* If the entire language does not allow side-effects, then any evaluation strategy can be used; this gives the compiler freedom to reorder or combine the evaluation of expressions in a program (for example, using [[deforestation (computer science)|deforestation]]).
While most compilers for imperative programming languages detect pure functions and perform common-subexpression elimination for pure function calls, they cannot always do this for pre-compiled libraries, which generally do not expose this information, thus preventing optimizations that involve those external functions. Some compilers, such as [[GNU Compiler Collection|gcc]], add extra keywords for a programmer to explicitly mark external functions as pure, to enable such optimizations. [[Fortran 95]] also lets functions be designated ''pure''.<ref name=fortran95>{{cite
=== Recursion ===
Line 133:
The usual implementation strategy for lazy evaluation in functional languages is [[graph reduction]].<ref>[http://research.microsoft.com/~simonpj/papers/slpj-book-1987/index.htm The Implementation of Functional Programming Languages]. Simon Peyton Jones, published by Prentice Hall, 1987</ref> Lazy evaluation is used by default in several pure functional languages, including [[Miranda (programming language)|Miranda]], [[Clean (programming language)|Clean]], and [[Haskell]].
{{Harvnb|Hughes|1984}} argues for lazy evaluation as a mechanism for improving program modularity through [[separation of concerns]], by easing independent implementation of producers and consumers of data streams.<ref name="hughesWhyFPMatters">{{cite web |url=http://www.cse.chalmers.se/~rjmh/Papers/whyfp.html |title=Why Functional Programming Matters |author-link=John Hughes (computer scientist) |first=John |last=Hughes |year=1984}}</ref> Launchbury 1993 <!-- a cite arguing more strongly against lazy evaluation would be preferable here, if someone knows of one. --> describes some difficulties that lazy evaluation introduces, particularly in analyzing a program's storage requirements, and proposes an [[operational semantics]] to aid in such analysis.<ref name=launchbury1993>{{cite
=== Type systems ===
Line 143:
Some research-oriented functional languages such as [[Coq (software)|Coq]], [[Agda (theorem prover)|Agda]], [[Cayenne (programming language)|Cayenne]], and [[Epigram (programming language)|Epigram]] are based on [[intuitionistic type theory]], which lets types depend on terms. Such types are called [[dependent type]]s. These type systems do not have decidable type inference and are difficult to understand and program with.<ref>{{cite journal |last=Huet |first=Gérard P. |date=1973 |title=The Undecidability of Unification in Third Order Logic |journal=Information and Control |doi=10.1016/s0019-9958(73)90301-x |volume=22 |issue=3 |pages=257–267}}</ref><ref>{{cite thesis |type=Ph.D. |last=Huet |first=Gérard |date=Sep 1976 |title=Resolution d'Equations dans des Langages d'Ordre 1,2,...ω |language=fr |publisher=Universite de Paris VII}}</ref><ref>{{cite book |last=Huet |first=Gérard |date=2002 |editor1-last=Carreño |editor1-first=V. |editor2-last=Muñoz |editor2-first=C. |editor3-last=Tahar |editor3-first=S. |chapter=Higher Order Unification 30 years later |title=Proceedings, 15th International Conference TPHOL |volume=2410 |pages=3–12 |publisher=Springer |series=LNCS |chapter-url=http://pauillac.inria.fr/~huet/PUBLIC/Hampton.pdf}}</ref><ref>{{cite journal |first=J. B. |last=Wells |title=Typability and type checking in the second-order lambda-calculus are equivalent and undecidable |citeseerx=10.1.1.31.3590 |journal=Tech. Rep. 93-011 |year=1993 |pages=176–185}}</ref> But dependent types can express arbitrary propositions in [[higher-order logic]]. Through the [[Curry–Howard isomorphism]], then, well-typed programs in these languages become a means of writing formal [[mathematical proof]]s from which a compiler can generate [[formal verification|certified code]]. While these languages are mainly of interest in academic research (including in [[formalized mathematics]]), they have begun to be used in engineering as well. [[Compcert]] is a [[compiler]] for a subset of the [[C (programming language)|C programming language]] that is written in Coq and formally verified.<ref>{{cite web |url=http://compcert.inria.fr/doc/index.html |title=The Compcert verified compiler |last=Leroy|first=Xavier|date=17 September 2018}}</ref>
A limited form of dependent types called [[generalized algebraic data type]]s (GADT's) can be implemented in a way that provides some of the benefits of dependently typed programming while avoiding most of its inconvenience.<ref>{{cite journal |url=http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/ |title=Simple unification-based type inference for GADTs |first1=Simon |last1=Peyton Jones |first2=Dimitrios |last2=Vytiniotis |first3=Stephanie |last3=Weirich |author3-link= Stephanie Weirich |author4=Geoffrey Washburn |journal=Icfp 2006 |pages=50–61 |date=April 2006}}</ref> GADT's are available in the [[Glasgow Haskell Compiler]], in [[OCaml]]<ref>{{Cite web|title=OCaml Manual|url=https://caml.inria.fr/pub/docs/manual-ocaml/gadts.html|access-date=2021-03-08|website=caml.inria.fr}}</ref> and in [[Scala (programming language)|Scala]],<ref>{{Cite web|title=Algebraic Data Types|url=https://docs.scala-lang.org/scala3/book/types-adts-gadts.html|access-date=2021-03-08|website=Scala Documentation}}</ref> and have been proposed as additions to other languages including Java and C#.<ref>{{cite
=== Referential transparency ===
Line 205:
Immutability of data can in many cases lead to execution efficiency by allowing the compiler to make assumptions that are unsafe in an imperative language, thus increasing opportunities for [[inline expansion]].<ref>{{cite journal |title=Immutability specification and its applications |author1=Igor Pechtchanski |author2=Vivek Sarkar |journal=Concurrency and Computation: Practice and Experience |volume=17 |issue=5–6 |pages=639–662 |year=2005 |doi=10.1002/cpe.853 |s2cid=34527406}}</ref> Even if the involved copying that may seem implicit when dealing with persistent immutable data structures might seem computationally costly, some functional programming languages, like [[Clojure]] solve this issue by implementing mechanisms for safe memory sharing between ''formally'' ''immutable'' data.<ref>{{Cite web |title=An In-Depth Look at Clojure Collections |url=https://www.infoq.com/articles/in-depth-look-clojure-collections/ |access-date=2024-04-29 |website=InfoQ |language=en}}</ref> [[Rust (programming language)|Rust]] distinguishes itself by its approach to data immutability which involves immutable [[Reference (computer science)|references]]<ref>{{Cite web |title=References and Borrowing - The Rust Programming Language |url=https://doc.rust-lang.org/book/ch04-02-references-and-borrowing.html |access-date=2024-04-29 |website=doc.rust-lang.org}}</ref> and a concept called ''lifetimes.''<ref>{{Cite web |title=Validating References with Lifetimes - The Rust Programming Language |url=https://doc.rust-lang.org/book/ch10-03-lifetime-syntax.html |access-date=2024-04-29 |website=doc.rust-lang.org}}</ref>
Immutable data with separation of identity and state and [[Shared-nothing architecture|shared-nothing]] schemes can also potentially be more well-suited for [[Parallel computing|concurrent and parallel]] programming by the virtue of reducing or eliminating the risk of certain concurrency hazards, since concurrent operations are usually [[Linearizability|atomic]] and this allows eliminating the need for locks. This is how for example <code>java.util.concurrent</code> classes are implemented, where some of them are immutable variants of the corresponding classes that are not suitable for concurrent use.<ref>{{Cite web |title=Concurrent Collections (The Java™ Tutorials > Essential Java Classes > Concurrency) |url=https://docs.oracle.com/javase/tutorial/essential/concurrency/collections.html |access-date=2024-04-29 |website=docs.oracle.com}}</ref> Functional programming languages often have a concurrency model that instead of shared state and synchronization, leverages [[message passing]] mechanisms (such as the [[actor model]], where each actor is a container for state, behavior, child actors and a message queue).<ref>{{Cite web |date=2023-01-28 |title=Understanding The Actor Model To Build Non-blocking, High-throughput Distributed Systems - Scaleyourapp |url=https://scaleyourapp.com/actor-model/ |access-date=2024-04-29 |website=scaleyourapp.com |language=en-US}}</ref><ref>{{Cite book |last=Cesarini |first=Francesco |title=Erlang programming: a concurrent approach to software development |last2=Thompson |first2=Simon |publisher=O'Reilly Media, Inc. |year=2009 |isbn=
[[Lazy evaluation]] may also speed up the program, even asymptotically, whereas it may slow it down at most by a constant factor (however, it may introduce [[memory leak]]s if used improperly). Launchbury 1993<ref name=launchbury1993/> discusses theoretical issues related to memory leaks from lazy evaluation, and O'Sullivan ''et al.'' 2008<ref>{{cite web |url=http://book.realworldhaskell.org/read/profiling-and-optimization.html#x_eK1 |title=Chapter 25. Profiling and optimization |publisher=Book.realworldhaskell.org |access-date=2011-06-20}}</ref> give some practical advice for analyzing and fixing them.
Line 399:
* Graham, Paul. ''ANSI Common LISP''. Englewood Cliffs, New Jersey: [[Prentice Hall]], 1996.
* MacLennan, Bruce J. ''Functional Programming: Practice and Theory''. Addison-Wesley, 1990.
*{{cite book |last1=Michaelson |first1=Greg |title=An Introduction to Functional Programming Through Lambda Calculus |date=10 April 2013 |publisher=Courier Corporation |isbn=978-0-486-28029-5 |language=en}}
* {{cite book|last1=O'Sullivan|first1=Brian|last2=Stewart|first2=Don|last3=Goerzen|first3=John |title=Real World Haskell |url=http://book.realworldhaskell.org/read/ |year=2008|publisher=O'Reilly}}
* Pratt, Terrence W. and [[Marvin Victor Zelkowitz]]. ''Programming Languages: Design and Implementation''. 3rd ed. Englewood Cliffs, New Jersey: [[Prentice Hall]], 1996.
| |||