Editing Functional programming (section)

=== Type systems ===
{{main|Type system}}
<!-- 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 data 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 (programming language)|Agda]], [[Lennart 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]] that is written in Coq and formally verified.<ref>{{cite web |url=http://compcert.inria.fr/doc/index.html |title=The Compcert verified compiler |last1=Leroy|first1=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>