Tipo de função - Function type

Em ciência da computação e lógica matemática , um tipo de função (ou tipo de seta ou exponencial ) é o tipo de uma variável ou parâmetro ao qual uma função tem ou pode ser atribuída, ou um argumento ou tipo de resultado de uma função de ordem superior recebendo ou retornando uma função.

Um tipo de função depende do tipo dos parâmetros e do tipo de resultado da função (ele, ou mais precisamente o construtor de tipo não aplicado · → ·, é um tipo de tipo superior ). Em configurações teóricas e linguagens de programação , onde as funções são definidas no formulário de curry , como o cálculo lambda simplesmente tipado , um tipo de função depende exatamente dois tipos, o domínio A eo gama B . Aqui, um tipo de função é frequentemente denotado A → B , seguindo uma convenção matemática, ou B A , com base na existência de exatamente B A (exponencialmente muitos) mapeamentos de funções teóricas de conjuntos de A a B na categoria de conjuntos . A classe de tais mapas ou funções é chamada de objeto exponencial . O ato de currying torna o tipo de função adjacente ao tipo de produto ; isso é explorado em detalhes no artigo sobre currying.

O tipo de função pode ser considerado um caso especial do tipo de produto dependente , que entre outras propriedades, engloba a ideia de uma função polimórfica .

Linguagens de programação

A sintaxe usada para tipos de função em várias linguagens de programação pode ser resumida, incluindo um exemplo de assinatura de tipo para a função de composição de função de ordem superior:

Língua Notação Assinatura de tipo de exemplo
Com funções de primeira classe ,
polimorfismo paramétrico 		C # Func<α1,α2,...,αn,ρ> Func<A,C> compose(Func<B,C> f, Func<A,B> g);
Haskell α -> ρ compose :: (b -> c) -> (a -> b) -> a -> c
OCaml α -> ρ compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c
Scala (α1,α2,...,αn) => ρ def compose[A, B, C](f: B => C, g: A => B): A => C
ML padrão α -> ρ compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c
Rápido α -> ρ func compose<A,B,C>(f: (B) -> C, g: (A) -> B) -> (A) -> C
Ferrugem fn(α1,α2,...,αn) -> ρ fn compose<A, B, C>(f: fn(A) -> B, g: fn(B) -> C) -> fn(A) -> C
Com funções de primeira classe ,
sem polimorfismo paramétrico 		Ir func(α1,α2,...,αn) ρ var compose func(func(int)int, func(int)int) func(int)int
C ++ , Objective-C , com blocos ρ (^)(α1,α2,...,αn) int (^compose(int (^f)(int), int (^g)(int)))(int);
Sem funções de primeira classe ,
polimorfismo paramétrico 		C ρ (*)(α1,α2,...,αn) int (*compose(int (*f)(int), int (*g)(int)))(int);
C ++ 11 Não Único.

std::function<ρ (α1,α2,...,αn)> é o tipo mais geral (veja abaixo).

function<function<int(int)>(function<int(int)>, function<int(int)>)> compose;

Ao examinar o exemplo de assinatura de tipo de, por exemplo, C #, o tipo da função composeé realmente Func<Func<A,B>,Func<B,C>,Func<A,C>>.

Devido ao apagamento de tipo no C ++ 11 std::function, é mais comum usar modelos para parâmetros de função de ordem superior e tipo inference ( auto) para encerramentos .

Semântica denotacional

O tipo de função em linguagens de programação não corresponde ao espaço de todas as funções teóricas de conjuntos. Dado o tipo infinito contável de números naturais como o domínio e os booleanos como intervalo, então existe um número infinito incontável (2 ℵ 0 = c ) de funções teóricas de conjuntos entre eles. Claramente, este espaço de funções é maior do que o número de funções que podem ser definidas em qualquer linguagem de programação, pois existem apenas muitos programas contáveis ​​(um programa sendo uma sequência finita de um número finito de símbolos) e uma das funções teóricas dos conjuntos resolve efetivamente o problema da parada .

A semântica denotacional se preocupa em encontrar modelos mais apropriados (chamados domínios ) para modelar conceitos de linguagem de programação, como tipos de função. Acontece que restringir a expressão ao conjunto de funções computáveis também não é suficiente se a linguagem de programação permitir a escrita de cálculos não-terminais (que é o caso se a linguagem de programação for Turing completa ). A expressão deve ser restrita às chamadas funções contínuas (correspondendo a continuidade na topologia Scott , não continuidade no sentido analítico real). Mesmo assim, o conjunto de função contínua contém a função paralela ou , que não pode ser definida corretamente em todas as linguagens de programação.

Veja também

Referências

  • Pierce, Benjamin C. (2002). Tipos e linguagens de programação . The MIT Press. pp.  99 –100.
  • Mitchell, John C. Fundamentos para linguagens de programação . The MIT Press.
  • tipo de função em nLab
  • Teoria dos Tipos de Homotopia: Fundamentos Univalentes da Matemática , Programa de Fundamentos Univalentes, Instituto de Estudos Avançados . Consulte a seção 1.2 .