Functional programming: Difference between revisions

Revision as of 07:50, 30 September 2024

Revision as of 02:27, 4 October 2024

Line 76:

[[John Backus]] presented [[FP (programming language)|FP]] in his 1977 [[Turing Award]] lecture "Can Programming Be Liberated From the [[Von Neumann architecture|von Neumann]] Style? A Functional Style and its Algebra of Programs".<ref name="Backus 1977">{{Cite journal |doi=10.1145/359576.359579| title=Can programming be liberated from the von Neumann style?: A functional style and its algebra of programs| journal=Communications of the ACM| volume=21| issue=8| pages=613–641| year=1978| last1=Backus |first1=J. |doi-access=free}}</ref> He defines functional programs as being built up in a hierarchical way by means of "combining forms" that allow an "algebra of programs"; in modern language, this means that functional programs follow the [[principle of compositionality]].{{Citation needed|reason=I dont completely agree with this interpretation of John Backus definition of functional programs, which I feel is widely misunderstood. As he is very sadly no longer alive, we can't ask him, but a reference for this interpretation, especially if it includes a justification, would be very beneficial.|date=February 2017}} Backus's paper popularized research into functional programming, though it emphasized [[function-level programming]] rather than the lambda-calculus style now associated with functional programming.

The 1973 language [[ML (programming language)|ML]] was created by [[Robin Milner]] at the [[University of Edinburgh]], and [[David Turner (computer scientist)|David Turner]] developed the language [[SASL (programming language)|SASL]] at the [[University of St Andrews]]. Also in Edinburgh in the 1970s, Burstall and Darlington developed the functional language [[NPL (programming language)|NPL]].<ref>R.M. Burstall. Design considerations for a functional programming language. Invited paper, Proc. Infotech State of the Art Conf. "The Software Revolution", Copenhagen, 45–57 (1977)</ref> NPL was based on [[Kleene's recursion theorem|Kleene Recursion Equations]] and was first introduced in their work on program transformation.<ref>R.M. Burstall and J. Darlington. A transformation system for developing recursive programs. Journal of the Association for Computing Machinery 24(1):44–67 (1977)</ref> Burstall, MacQueen and Sannella then incorporated the [[Polymorphism (computer science)|polymorphic]] type checking from ML to produce the language [[Hope (programming language)|Hope]].<ref>R.M. Burstall, D.B. MacQueen and D.T. Sannella. HOPE: an experimental applicative language. Proc.Proceedings 1980 LISP Conference, Stanford, 136–143 (1980).</ref> ML eventually developed into several dialects, the most common of which are now [[OCaml]] and [[Standard ML]].

In the 1970s, [[Guy L. Steele]] and [[Gerald Jay Sussman]] developed [[Scheme (programming language)|Scheme]], as described in the [[Lambda Papers]] and the 1985 textbook ''[[Structure and Interpretation of Computer Programs]]''. Scheme was the first dialect of lisp to use [[lexical scope|lexical scoping]] and to require [[tail-call optimization]], features that encourage functional programming.

Line 139:

<!-- expand this section!!! also split it into several sections -->

Especially since the development of [[Hindley–Milner type inference]] in the 1970s, functional programming languages have tended to use [[typed lambda calculus]], rejecting all invalid programs at compilation time and risking [[false positives and false negatives#False positive error|false positive errors]], as opposed to the [[untyped lambda calculus]], that accepts all valid programs at compilation time and risks [[false positives and false negatives#False negative error|false negative errors]], used in Lisp and its variants (such as [[Scheme (programming language)|Scheme]]), as they reject all invalid programs at runtime when the information is enough to not reject valid programs. The use of [[algebraic datatypesdata type]]s makes manipulation of complex data structures convenient; the presence of strong compile-time type checking makes programs more reliable in absence of other reliability techniques like [[test-driven development]], while [[type inference]] frees the programmer from the need to manually declare types to the compiler in most cases.

Some research-oriented functional languages such as [[Coq (software)|Coq]], [[Agda (theoremprogramming proverlanguage)|Agda]], [[CayenneLennart (programming language)Augustsson|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 language [[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 |lastlast1=Leroy|firstfirst1=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 conference |title=Generalized Algebraic Data Types and Object-Oriented Programming |first1=Andrew |last1=Kennedy |first2=Claudio V. |last2=Russo |conference=OOPSLA |date=October 2005 |publisher=[[Association for Computing Machinery|ACM]] |___location=San Diego, California |url=https://www.microsoft.com/en-us/research/publication/generalized-algebraic-data-types-and-object-oriented-programming/ |archive-url=https://web.archive.org/web/20061229164852/http://research.microsoft.com/~akenn/generics/gadtoop.pdf |archive-date=2006-12-29 |doi=10.1145/1094811.1094814 |isbn=9781595930316}}</ref>