Existe algum motivo para ter um tipo bottom numa linguagem de programação?

44

Um tipo bottom é uma construção que aparece principalmente na teoria matemática de tipos. Também é chamado o tipo vazio. É um tipo que não tem valores, mas é um subtipo de todos os tipos.

Se o tipo de retorno de uma função for o tipo inferior, isso significa que ele não retorna. Período. Talvez faça um loop para sempre ou talvez cause uma exceção.

Qual é o sentido de ter esse tipo estranho em uma linguagem de programação? Não é tão comum, mas está presente em alguns, como Scala e Lisp.

    
por GregRos 24.03.2015 / 01:15
fonte

7 respostas

30

Vou dar um exemplo simples: C ++ vs Rust.

Aqui está uma função usada para lançar uma exceção no C ++ 11:

[[noreturn]] void ThrowException(char const* message,
                                 char const* file,
                                 int line,
                                 char const* function);

E aqui está o equivalente em Rust:

fn formatted_panic(message: &str, file: &str, line: isize, function: &str) -> !;

Em uma questão puramente sintática, a construção Rust é mais sensata. Observe que a construção C ++ especifica um tipo de retorno , embora também especifique que não retornará. Isso é um pouco estranho.

Em uma nota padrão, a sintaxe C ++ apareceu apenas no C ++ 11 (ela foi colocada no topo), mas vários compiladores vinham fornecendo várias extensões há algum tempo, de modo que as ferramentas de análise de terceiros precisavam ser programadas para reconhecer as várias maneiras pelas quais esse atributo poderia ser escrito. Ter isso padronizado é obviamente claramente superior.

Agora, quanto ao benefício?

O fato de uma função não retornar pode ser útil para:

  • otimização: pode-se remover qualquer código após ele (ele não retornará), não há necessidade de salvar os registros (pois não será necessário restaurá-los), ...
  • análise estática: elimina vários caminhos de execução potenciais
  • maintainability: (veja análise estática, mas por humanos)
por 24.03.2015 / 09:10
fonte
22

A resposta de Karl é boa. Aqui está um uso adicional que eu não acho que alguém tenha mencionado. O tipo de

if E then A else B

deve ser um tipo que inclua todos os valores no tipo A e todos os valores no tipo B . Se o tipo de B for Nothing , o tipo da expressão if poderá ser o tipo de A . Eu frequentemente declaro uma rotina

def unreachable( s:String ) : Nothing = throw new AssertionError("Unreachable "+s) 

para dizer que o código não deve ser alcançado. Como seu tipo é Nothing , unreachable(s) agora pode ser usado em qualquer if ou (mais frequentemente) switch sem afetar o tipo de resultado. Por exemplo

 val colour : Colour := switch state of
         BLACK_TO_MOVE: BLACK
         WHITE_TO_MOVE: WHITE
         default: unreachable("Bad state")

Scala tem esse tipo de Nada.

Outro caso de uso para Nothing (como mencionado na resposta de Karl) é List [Nothing] é o tipo de listas de cada membro cujos membros possuem tipo Nothing. Assim, pode ser o tipo da lista vazia.

A propriedade chave de Nothing que faz com que esses casos de uso funcionem é não que não tem valores (embora no Scala, por exemplo; não tenha valores), é que é um subtipo de qualquer outro tipo.

Suponha que você tenha um idioma em que cada tipo contenha o mesmo valor - vamos chamá-lo de () . Nessa linguagem, o tipo de unidade, que tem () como seu único valor, poderia ser um subtipo de cada tipo. Isso não faz com que seja um tipo de fundo no sentido que o OP significava; o OP ficou claro que um tipo bottom não contém valores. No entanto, como é um tipo que é um subtipo de cada tipo, pode desempenhar o mesmo papel que um tipo de fundo.

Haskell faz as coisas um pouco diferente. Em Haskell, uma expressão que nunca produz um valor pode ter o tipo forall a.a . Uma instância desse tipo de esquema se unirá com qualquer outro tipo, de modo que efetivamente atue como um tipo de fundo, mesmo que (padrão) Haskell não tenha noção de subtipagem. Por exemplo, a função error do prelúdio padrão possui o esquema de tipos forall a. [Char] -> a . Então você pode escrever

if E then A else error ""

e o tipo da expressão será o mesmo que o tipo de A , para qualquer expressão A .

A lista vazia em Haskell tem o esquema de tipos forall a. [a] . Se A for uma expressão cujo tipo é um tipo de lista,

if E then A else []

é uma expressão com o mesmo tipo que A . O tipo de [] é igual ao tipo [error ""] , que mostra que a lista vazia não é o único valor do seu tipo.

    
por 24.03.2015 / 11:53
fonte
17

Maybe it loops forever, or maybe it throws an exception.

Parece um tipo útil de se ter nessas situações, por mais raras que possam ser.

Além disso, mesmo que Nothing (nome do Scala para o tipo bottom) não tenha valores, List[Nothing] não tem essa restrição, o que o torna útil como o tipo de uma lista vazia. A maioria das linguagens contorna isso fazendo de uma lista vazia de strings um tipo diferente de uma lista vazia de inteiros, o que faz sentido, mas torna uma lista vazia mais detalhada para escrever, o que é uma grande desvantagem em uma linguagem orientada a listas.

    
por 24.03.2015 / 05:04
fonte
17

Os tipos formam um monoid de duas maneiras, juntos fazendo uma semiring . Isso é o que chamamos de tipos de dados algébricos . Para tipos finitos, este semicondutor está diretamente relacionado à semicondução de números naturais (incluindo zero), o que significa que você conta quantos valores possíveis o tipo possui (excluindo "valores não-terminais").

  • O tipo de fundo (eu chamarei Vacuous ) tem valores zero .
  • O tipo de unidade tem um valor. Vou chamar o tipo e seu valor único () .
  • Composição (que a maioria das linguagens de programação suporta diretamente, através de registros / structs / classes com campos públicos) é uma operação produto . Por exemplo, (Bool, Bool) tem quatro valores possíveis, a saber (False,False) , (False,True) , (True,False) e (True,True) .
    O tipo de unidade é o elemento de identidade da operação de composição. Por exemplo. ((), False) e ((), True) são os únicos valores do tipo ((), Bool) , portanto, esse tipo é isomórfico para Bool em si.
  • Tipos alternativos são um pouco negligenciados na maioria das linguagens (as linguagens OO suportam-nas com herança), mas não são menos úteis. Uma alternativa entre dois tipos A e B basicamente tem todos os valores de A , além de todos os valores de B , portanto tipo de soma . Por exemplo, Either () Bool tem três valores, eu os chamarei de Left () , Right False e Right True .
    O tipo bottom é o elemento de identidade da soma: Either Vacuous A tem somente valores da forma Right a , porque Left ... não faz sentido ( Vacuous não tem valores).

O que é interessante sobre esses monóides é que, quando você introduz funções em seu idioma, o categoria desses tipos com as funções de morfismos é uma categoria monoidal . Entre outras coisas, isso permite que você defina functores aplicativos e monads , que se revelam uma excelente abstração para cálculos gerais (possivelmente envolvendo efeitos colaterais etc.) dentro de termos puramente funcionais.

Agora, na verdade, você pode ir muito longe preocupando apenas um lado do problema (a composição monóide), então você realmente não precisa do tipo bottom explicitamente. Por exemplo, mesmo Haskell por um longo tempo não tem um tipo de fundo padrão. Agora, ele é chamado Void .

Mas quando você considera a imagem completa, como uma categoria fechada bicartesiana , o sistema de tipos é na verdade, equivalente a todo o cálculo lambda, então basicamente você tem a abstração perfeita sobre tudo o que é possível em uma linguagem Turing-completa. Ótimo para linguagens de domínio específico, por exemplo, há um projeto de sobre a codificação direta de circuitos eletrônicos dessa maneira .

Naturalmente, você pode dizer que isso é tudo bobagem geral dos teoristas . Você não precisa saber nada sobre a teoria das categorias para ser um bom programador, mas quando o faz, dá a você maneiras poderosas e ridiculamente gerais de raciocinar sobre código, além de provar invariantes.

mb21 me lembra de notar que isso não deve ser confundido com valores inferiores . Em idiomas preguiçosos como Haskell, o tipo every contém um "valor" inferior, denotado . Esta não é uma coisa concreta que você poderia explicitamente passar, em vez disso, é o que é "retornado", por exemplo, quando uma função faz um loop para sempre. Mesmo o tipo Void de Haskell “contém” o valor inferior, daí o nome. Sob essa luz, o tipo bottom de Haskell realmente tem um valor e seu tipo de unidade tem dois valores, mas na discussão da teoria de categorias isso é geralmente ignorado.

    
por 24.03.2015 / 18:09
fonte
2

É útil para análise estática documentar o fato de que um caminho de código específico não está acessível. Por exemplo, se você escrever o seguinte em C #:

int F(int arg) {
 if (arg != 0)
  return arg + 1; //some computation
 else
  Assert(false); //this throws but the compiler does not know that
}
void Assert(bool cond) { if (!cond) throw ...; }

O compilador irá reclamar que F não retorna nada em pelo menos um caminho de código. Se Assert fosse marcado como não retornando, o compilador não precisaria avisar.

    
por 24.03.2015 / 13:38
fonte
2

Em alguns idiomas, null tem o tipo bottom, já que o subtipo de todos os tipos define bem para quais idiomas usar null (apesar da leve contradição de ter null sendo ele mesmo e uma função que retorna, evitando argumentos comuns sobre por que bot deve ser desabitada).

Ele também pode ser usado como um pega-tudo em tipos de função ( any -> bot ) para lidar com o despacho que deu errado.

E alguns idiomas permitem que você realmente resolva bot como um erro, que pode ser usado para fornecer erros de compilador personalizados.

    
por 24.03.2015 / 02:41
fonte
1

Sim, este é um tipo bastante útil; enquanto seu papel seria principalmente interior ao sistema de tipos, há alguma ocasião em que o tipo de fundo apareceria abertamente.

Considere uma linguagem estaticamente tipada na qual os condicionais são expressões (então a construção if-then-else também funciona como o operador ternário de C e amigos, e pode haver uma declaração de caso multi-way similar. Linguagem de programação funcional tem isso, mas também acontece em certas linguagens imperativas (desde ALGOL 60). Então, todas as expressões de ramificação devem, em última instância, produzir o tipo de expressão condicional inteira. Pode-se simplesmente exigir que seus tipos sejam iguais (e acho que este é o caso para o operador ternário em C), mas isso é excessivamente restritivo, especialmente quando o condicional também pode ser usado como declaração condicional (não retornando nenhum valor útil). Em geral, uma pessoa quer que cada expressão de ramificação seja (implicitamente) conversível para um tipo comum que será o tipo da expressão completa (possivelmente com restrições mais ou menos complicadas para permitir que esse tipo comum seja efetivamente encontrado pelo complier, cf. C ++, mas não vou entrar nesses detalhes aqui).

Existem dois tipos de situações em que um tipo geral de conversão permitirá a flexibilidade necessária de tais expressões condicionais. Um já foi mencionado, onde o tipo de resultado é o tipo de unidade void ; isto é naturalmente um super-tipo de todos os outros tipos, e permitir que qualquer tipo seja (trivialmente) convertido para ele torna possível usar a expressão condicional como declaração condicional. O outro envolve casos em que a expressão retorna um valor útil, mas um ou mais ramos são incapazes de produzir um. Eles geralmente levantam uma exceção ou envolvem um salto, e exigir que eles (também) produzam um valor do tipo de expressão inteira (de um ponto inacessível) seria inútil. É esse tipo de situação que pode ser tratada com graça, dando-se cláusulas, saltos e chamadas para a criação de exceções que terão esse efeito, o tipo inferior, o tipo que pode ser (trivialmente) convertido em qualquer outro tipo.

Eu sugiro escrever um tipo de fundo como * para sugerir sua conversibilidade para tipos arbitrários. Ele pode servir a outros propósitos úteis internamente, por exemplo, ao tentar deduzir um tipo de resultado para uma função recursiva que não declara nenhum, o tipo inferencer poderia atribuir o tipo * a qualquer chamada recursiva para evitar uma situação de galinha e ovo ; o tipo real será determinado por ramificações não recursivas, e as recursivas serão convertidas para o tipo comum das não recursivas. Se houver nenhuma ramificação não recursiva, o tipo permanecerá * e indicará corretamente que a função não tem como retornar da recursão. Além disso e como tipo de exceção de lançamento de funções, pode-se usar * como tipo de componente de seqüências de comprimento 0, por exemplo, da lista vazia; novamente, se algum elemento for selecionado de uma expressão do tipo [*] (lista necessariamente vazia), então o tipo resultante * indicará corretamente que isso nunca poderá retornar sem um erro.

    
por 24.03.2015 / 13:46
fonte