GetWiki
function type
ARTICLE SUBJECTS
being →
database →
ethics →
fiction →
history →
internet →
language →
linux →
logic →
method →
news →
policy →
purpose →
religion →
science →
software →
truth →
unix →
wiki →
ARTICLE TYPES
essay →
feed →
help →
system →
wiki →
ARTICLE ORIGINS
critical →
forked →
imported →
original →
function type
please note:
- the content below is remote from Wikipedia
- it has been imported raw for GetWiki
In computer science and mathematical logic, a function type (or arrow type or exponential) is the type of a variable or parameter to which a function has or can be assigned, or an argument or result type of a higher-order function taking or returning a function.A function type depends on the type of the parameters and the result type of the function (it, or more accurately the unapplied type constructor {{nowrap|· â ·}}, is a higher-kinded type). In theoretical settings and programming languages where functions are defined in curried form, such as the simply typed lambda calculus, a function type depends on exactly two types, the domain A and the range B. Here a function type is often denoted {{math|A â B}}, following mathematical convention, or {{math|B'A}}, based on there existing exactly {{math|B'A}} (exponentially many) set-theoretic functions mappings A to B in the category of sets. The class of such maps or functions is called the exponential object. The act of currying makes the function type adjoint to the product type; this is explored in detail in the article on currying.The function type can be considered to be a special case of the dependent product type, which among other properties, encompasses the idea of a polymorphic function.- the content below is remote from Wikipedia
- it has been imported raw for GetWiki
Programming languages
The syntax used for function types in several programming languages can be summarized, including an example type signature for the higher-order function composition function:{| class=wikitableWith first-class functions, parametric polymorphism | C Sharp (programming language)>C#| Func | 2=csharp|Func compose(Func f, Func g);}} |
Haskell (programming language)>Haskell| α -> Ï | 2=haskell|compose :: (b -> c) -> (a -> b) -> a -> c}} |
2=ocaml|compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c}} |
Scala (programming language)>Scala| (α1,α2,...,αn) => Ï | 2=scala|1=def compose[A, B, C](f: B => C, g: A => B): A => C }} |
2=sml|compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c}} |
Swift (programming language)>Swift| α -> Ï | 2=swift|func compose(f: (B) -> C, g: (A) -> B) -> (A) -> C}} |
Rust (programming language)>Rust| fn(α1,α2,...,αn) -> Ï | 2=rust|fn compose(f: fn(A) -> B, g: fn(B) -> C) -> fn(A) -> C}} |
With first-class functions, without parametric polymorphism | Go (programming language)>Go| func(α1,α2,...,αn) Ï | 2=go|var compose func(func(int)int, func(int)int) func(int)int}} |
C++, Objective-C, with Blocks (C language extension)>blocks| Ï (^)(α1,α2,...,αn) | 2=objc|int (^compose(int (^f)(int), int (^g)(int)))(int);}} |
Without first-class functions, parametric polymorphism | C (programming language)>C| Ï (*)(α1,α2,...,αn) | 2=c|int (*compose(int (*f)(int), int (*g)(int)))(int);}} |
2=cpp|function compose;}} |
Denotational semantics
The function type in programming languages does not correspond to the space of all set-theoretic functions. Given the countably infinite type of natural numbers as the domain and the booleans as range, then there are an uncountably infinite number (2âµ0 = c) of set-theoretic functions between them. Clearly this space of functions is larger than the number of functions that can be defined in any programming language, as there exist only countably many programs (a program being a finite sequence of a finite number of symbols) and one of the set-theoretic functions effectively solves the halting problem.Denotational semantics concerns itself with finding more appropriate models (called domains) to model programming language concepts such as function types. It turns out that restricting expression to the set of computable functions is not sufficient either if the programming language allows writing non-terminating computations (which is the case if the programming language is Turing complete). Expression must be restricted to the so-called continuous functions (corresponding to continuity in the Scott topology, not continuity in the real analytical sense). Even then, the set of continuous function contains the parallel-or function, which cannot be correctly defined in all programming languages.See also
- Cartesian closed category
- Currying
- Exponential object, category-theoretic equivalent
- First-class function
- Function space, set-theoretic equivalent
References
- BOOK, Benjamin C., Pierce, Benjamin C. Pierce, Types and Programming Languages, 2002,weblink limited, The MIT Press, 99â100, 9780262162098,
- BOOK, John C., Mitchell, John C. Mitchell, Foundations for Programming Languages, The MIT Press,
- {{nlab|id=function+type|title=function type}}
- Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study. See section 1.2.
- content above as imported from Wikipedia
- "function type" does not exist on GetWiki (yet)
- time: 6:34pm EDT - Wed, Apr 24 2024
- "function type" does not exist on GetWiki (yet)
- time: 6:34pm EDT - Wed, Apr 24 2024
[ this remote article is provided by Wikipedia ]
LATEST EDITS [ see all ]
GETWIKI 23 MAY 2022
The Illusion of Choice
Culture
Culture
GETWIKI 09 JUL 2019
Eastern Philosophy
History of Philosophy
History of Philosophy
GETWIKI 09 MAY 2016
GetMeta:About
GetWiki
GetWiki
GETWIKI 18 OCT 2015
M.R.M. Parrott
Biographies
Biographies
GETWIKI 20 AUG 2014
GetMeta:News
GetWiki
GetWiki
© 2024 M.R.M. PARROTT | ALL RIGHTS RESERVED