Existe uma razão para ter um tipo inferior em uma linguagem de programação?

49

Um tipo inferior é um construto que aparece principalmente na teoria matemática dos tipos. Também é chamado de 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 é o tipo inferior, isso significa que ele não retorna. Período. Talvez ele faça um loop para sempre, ou talvez gere 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.

GregRos
fonte
2
@ SargeBorsch: você tem certeza disso? Claro que não se pode em C definir explicitamente uma voiddados ...
Basile Starynkevitch
3
@BasileStarynkevitch não há valores do tipo voide o tipo de unidade deve ter um valor. Além disso, como você apontou, você não pode nem mesmo declarar um valor do tipo void, o que significa que não é nem um tipo, apenas uma caixa de canto especial no idioma.
Sarge Borsch
2
Sim, o C é bizarro nisso, especialmente na forma como os tipos de ponteiro e função são escritos. Mas voidem Java é quase o mesmo: não é realmente um tipo e não pode ter valores.
Sarge Borsch 24/03
3
Na semântica de idiomas com um tipo inferior, o tipo inferior não é considerado sem valores, mas sim com um valor, o valor inferior, representando uma computação que nunca é concluída (normalmente). Como o valor inferior é um valor de cada tipo, o tipo inferior pode ser um subtipo de cada tipo.
Theodore Norvell
4
@BasileStarynkevitch Common Lisp tem o tipo nulo que não possui valores. Ele também possui o tipo nulo, que possui apenas um valor, o símbolo nil(aka, ()), que é um tipo de unidade.
Joshua Taylor

Respostas:

33

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, o construto Rust é mais sensível. 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 do C ++ apareceu apenas com o C ++ 11 (foi abordada na parte superior), mas vários compiladores vinham fornecendo várias extensões há algum tempo, de modo que ferramentas de análise de terceiros precisavam ser programadas para reconhecer as várias maneiras esse atributo pode ser gravado. Tê-lo padronizado é obviamente claramente superior.


Agora, quanto ao benefício?

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

  • otimização: é possível remover qualquer código depois dele (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 em potencial
  • manutenibilidade: (veja análise estática, mas por seres humanos)
Matthieu M.
fonte
6
voidno seu exemplo C ++ define (parte de) o tipo da função - não o tipo de retorno. Ele restringe o valor que a função tem permissão return; qualquer coisa que possa ser convertida em nula (que não é nada). Se a função returns não deve ser seguida por um valor. O tipo integral da função é void () (char const*, char const*, int, char const *). + 1 para usar em char constvez de const char:-) #
24715
4
Isso não significa que faz mais sentido ter um tipo inferior, apenas que faz sentido anotar funções sobre se elas retornam ou não como parte do idioma. Na verdade, como as funções podem falhar ao retornar devido a diferentes razões, parece melhor codificar a razão de alguma maneira, em vez de usar um termo genérico, como o conceito relativamente recente de anotação de funções com base em seus efeitos colaterais.
22715 GregRos
2
Na verdade, há uma razão para tornar "não retorna" e "possui tipo de retorno X" independente: compatibilidade com versões anteriores para seu próprio código, pois a convenção de chamada pode depender do tipo de retorno.
Deduplicator
é [[noreturn]] par da sintaxe ou uma adição de funcionalidade?
Zaibis 25/03
11
[cont.] No geral, eu diria que uma discussão sobre as vantagens de ⊥ deve definir o que qualifica como uma implementação de ⊥; e não acho que um sistema de tipos que não possua ( a → ⊥) ≤ ( ab ) seja uma implementação útil de ⊥. Portanto, nesse sentido, o SysV x86-64 C ABI (entre outros) simplesmente não permite a implementação ⊥.
Alex Shpilkin
26

A resposta de Karl é boa. Aqui está um uso adicional que acho que ninguém mais mencionou. O tipo de

if E then A else B

deve ser um tipo que inclua todos os valores no tipo de Ae todos os valores no tipo de B. Se o tipo de Bfor Nothing, o tipo da ifexpressão pode ser o tipo de A. Eu frequentemente declaro uma rotina

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

dizer que não se espera que o código seja alcançado. Como seu tipo é Nothing, unreachable(s)agora pode ser usado em qualquer um if(ou mais frequentemente) switchsem 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 lista em que cada membro tem o tipo Nothing. Assim, pode ser o tipo da lista vazia.

A propriedade-chave Nothingque faz com que esses casos de uso funcionem não é que não tenha 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 (). Nesse idioma, o tipo de unidade, que tem ()como único valor, pode ser um subtipo de todo tipo. Isso não o torna um tipo de base no sentido que o OP significava; o OP ficou claro que um tipo inferior não contém valores. No entanto, como é um tipo que é um subtipo de todo tipo, pode desempenhar o mesmo papel que um tipo inferior.

Haskell faz as coisas de maneira um pouco diferente. Em Haskell, uma expressão que nunca produz um valor pode ter o esquema de tipos forall a.a. Uma instância desse esquema de tipo será unificada com qualquer outro tipo, portanto, atua efetivamente como um tipo inferior, mesmo que Haskell (padrão) não tenha noção de subtipagem. Por exemplo, a errorfunção do prelúdio padrão possui 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 possui o esquema de tipos forall a. [a]. Se Aé uma expressão cujo tipo é um tipo de lista, então

if E then A else []

é uma expressão do mesmo tipo que A.

Theodore Norvell
fonte
Qual é a diferença entre o tipo forall a . [a]e o tipo [a]em Haskell? As variáveis ​​de tipo já não são quantificadas universalmente nas expressões de tipo Haskell?
Giorgio
@Giorgio Em Haskell, a quantificação universal está implícita se estiver claro que você está procurando um esquema de tipos. Você não pode nem escrever forallno padrão Haskell 2010. Eu escrevi a quantificação explicitamente porque este não é um fórum do Haskell e algumas pessoas podem não estar familiarizadas com as convenções de Haskell. Portanto, não há diferença, exceto que isso forall a . [a]não é padrão, enquanto [a]é.
Theodore Norvell
19

Os tipos formam um monóide de duas maneiras, juntos formando um semicondutor . É o que se chama tipos de dados algébricos . Para tipos finitos, essa semicondução está diretamente relacionada à semântica de números naturais (incluindo zero), o que significa que você conta quantos valores possíveis o tipo possui (excluindo "valores não-determinantes").

  • O tipo inferior (eu o chamarei Vacuous) tem zero valores .
  • O tipo de unidade possui um valor. Vou chamar o tipo e seu valor único ().
  • A composição (que a maioria das linguagens de programação suporta diretamente, por meio de registros / estruturas / classes com campos públicos) é uma operação do produto . Por exemplo, (Bool, Bool)tem quatro valores possíveis, nomeadamente (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 Boolsi mesmo.
  • Tipos alternativos são um pouco negligenciados na maioria dos idiomas (os idiomas OO meio que os suportam com herança), mas não são menos úteis. Uma alternativa entre dois tipos Ae Bbasicamente tem todos os valores de A, mais todos os valores de B, portanto, o tipo de soma . Por exemplo, Either () Booltem três valores, eu vou chamá-los Left (), Right Falsee Right True.
    O tipo inferior é o elemento de identidade da soma: Either Vacuous Apossui apenas valores do formulário Right a, porque Left ...não faz sentido ( Vacuousnão possui valores).

O interessante desses monóides é que, quando você introduz funções na sua linguagem, a categoria desses tipos com as funções como morfismos é uma categoria monoidal . Entre outras coisas, isso permite definir functores e mônadas aplicáveis , que se tornam uma excelente abstração para cálculos gerais (possivelmente envolvendo efeitos colaterais etc.) em termos puramente funcionais.

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

Mas quando você considera a imagem completa, como uma categoria fechada bicartesiana , o sistema de tipos é realmente 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 completa de Turing. Ótimo para linguagens específicas de domínio incorporadas, por exemplo, existe um projeto sobre a codificação direta de circuitos eletrônicos dessa maneira .

Claro, você pode muito bem dizer que isso é um absurdo geral de todos os teóricos . Você não precisa conhecer a teoria das categorias para ser um bom programador, mas, quando o faz, oferece maneiras poderosas e ridiculamente gerais de raciocinar sobre código e provar invariantes.


mb21 me lembra que note que isso não deve ser confundido com valores inferiores . Em idiomas preguiçosos como Haskell, todo tipo contém um "valor" inferior, denotado . Isso não é algo concreto que você possa explicar explicitamente; é o que é "retornado", por exemplo, quando uma função faz um loop para sempre. Até o Voidtipo de Haskell “contém” o valor inferior, assim o nome. Sob essa luz, o tipo inferior de Haskell realmente tem um valor e seu tipo de unidade tem dois valores, mas na discussão da teoria da categoria isso geralmente é ignorado.

leftaroundabout
fonte
"O tipo inferior (eu o chamarei Void)", que não deve ser confundido com o valor bottom , que é membro de qualquer tipo em Haskell .
Mb21 #
18

Talvez ele faça um loop para sempre, ou talvez gere uma exceção.

Parece um tipo útil de ter nessas situações, por mais raros que sejam.

Além disso, mesmo que Nothing(o nome de Scala para o tipo inferior) não possa ter valores, List[Nothing]não possui essa restrição, o que a torna útil como o tipo de uma lista vazia. A maioria dos idiomas contorna isso, tornando uma lista vazia de seqüências de caracteres um tipo diferente de uma lista vazia de números 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.

Karl Bielefeldt
fonte
12
“A lista vazia de Haskell é um construtor de tipos”: certamente o mais relevante aqui é mais polimórfico ou sobrecarregado - ou seja, as listas vazias de diferentes tipos são valores distintos, mas []representam todos eles, e serão instanatiadas para o tipo específico, conforme necessário.
Peter LeFanu Lumsdaine
Curiosamente: Se você tentar criar uma matriz vazia no interpretador Haskell, você recebe um valor muito definido com um tipo muito indefinido: [a]. Da mesma forma, :t Left 1produz Num a => Either a b. A avaliação efetiva da expressão força o tipo de a, mas não o de b:Either Integer b
John Dvorak
5
A lista vazia é um construtor de valor . Um pouco confuso, o construtor de tipos envolvido tem o mesmo nome, mas a lista vazia em si é um valor, não um tipo (bem, há listas de nível de tipo também, mas esse é outro tópico). A parte que faz a lista vazia funcionar para qualquer tipo de lista é a implicada forallem seu tipo forall a. [a],. Existem algumas maneiras legais de pensar forall, mas leva algum tempo para realmente descobrir.
David
@PeterLeFanuLumsdaine Isso é exatamente o que significa ser um construtor de tipos. Significa apenas que é um tipo com um tipo diferente *.
GregRos
2
Em Haskell, []é um construtor de tipos e []é uma expressão que representa uma lista vazia. Mas isso não significa que "a lista vazia de Haskell é um construtor de tipos". O contexto deixa claro se []está sendo usado como um tipo ou como uma expressão. Suponha que você declare data Foo x = Foo | Bar x (Foo x); agora você pode usar Foocomo um construtor de tipos ou como um valor, mas é por acaso que você escolheu o mesmo nome para ambos.
Theodore Norvell
3

É útil para a 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 reclamará que Fnão retorna nada em pelo menos um caminho de código. Se Assertfosse marcado como não retornando, o compilador não precisaria avisar.

usr
fonte
2

Em algumas linguagens, nullpossui o tipo inferior, já que o subtipo de todos os tipos define bem para que linguagens usam nulo (apesar da leve contradição de nullser ao mesmo tempo uma função que se retorna, evitando os argumentos comuns sobre por que botdeveria ser desabitado).

Também pode ser usado como uma função geral nos tipos ( any -> bot) para lidar com o despacho que deu errado.

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

Telastyn
fonte
11
Não, um tipo inferior não é o tipo de unidade. Um tipo de fundo tem qualquer valor, de modo que uma função retornando um tipo de fundo não deve retornar (isto é, accionar uma excepção ou repetir indefinidamente)
Basile Starynkevitch
@BasileStarynkevitch - eu não estou falando sobre o tipo de unidade. O tipo de unidade é mapeado para voididiomas comuns (embora com semântica ligeiramente diferente para o mesmo uso), não null. Embora você também esteja certo, a maioria dos idiomas não modela nulo como o tipo inferior.
Telastyn 24/03/2015
3
@TheodoreNorvell - as primeiras versões do Tangent fizeram isso - embora eu seja o autor, talvez seja trapaça. Eu não tenho os links salvos para os outros, e já faz um tempo desde que eu fiz essa pesquisa.
Telastyn 24/03/2015
11
@ Martijn Mas você pode usar null, por exemplo, você pode comparar um ponteiro com nullum resultado booleano. Eu acho que as respostas estão mostrando que existem dois tipos distintos de tipos inferiores. (a) Idiomas (por exemplo, Scala), em que o tipo que é um subtipo de todo tipo representa cálculos que não fornecem nenhum resultado. Essencialmente, é um tipo vazio, embora tecnicamente frequentemente seja preenchido por um valor inferior inútil, que representa não terminação. (b) Idiomas como Tangent, em que o tipo inferior é um subconjunto de qualquer outro tipo, pois contém um valor útil que também é encontrado em todos os outros tipos - nulo.
Theodore Norvell
4
É interessante que alguns idiomas tenham um valor com um tipo que você não pode declarar (comum para o literal nulo), e outros tenham um tipo que você pode declarar, mas que não possui valores (um tipo inferior tradicional), e que eles preencham funções comparáveis .
287 Martijn
1

Sim, este é um tipo bastante útil; embora seu papel seja principalmente interno ao sistema de tipos, há algumas ocasiões em que o tipo inferior apareceria abertamente.

Considere uma linguagem de tipo estaticamente em que condicionais são expressões (para que a construção if-then-else dobre como o operador ternário de C e amigos, e pode haver uma declaração de caso de várias maneiras semelhante). A linguagem de programação funcional possui isso, mas isso também acontece em certas linguagens imperativas (desde o ALGOL 60). Então todas as expressões de ramificação devem finalmente produzir o tipo de toda a expressão condicional. Pode-se simplesmente exigir que seus tipos sejam iguais (e acho que esse é o caso do operador ternário em C), mas isso é excessivamente restritivo, especialmente quando o condicional também pode ser usado como declaração condicional (sem retornar nenhum valor útil). Em geral, deseja-se 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 abordarei esses 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, em que o tipo de resultado é o tipo de unidadevoid; esse é naturalmente um supertipo de todos os outros tipos e, ao permitir que qualquer tipo seja (trivialmente) convertido, é possível usar a expressão condicional como instrução condicional. O outro envolve casos em que a expressão retorna um valor útil, mas uma ou mais ramificações são incapazes de produzir uma. Eles geralmente geram uma exceção ou envolvem um salto, e exigir que eles (também) produzam um valor do tipo de toda a expressão (de um ponto inacessível) seria inútil. É esse tipo de situação que pode ser tratada com clareza, fornecendo cláusulas, saltos e chamadas para aumento de exceção que terão esse efeito, o tipo inferior, o tipo que pode ser (trivialmente) convertido em qualquer outro tipo.

Eu sugeriria escrever um tipo inferior que *sugerisse sua conversibilidade para um tipo arbitrário. 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 inferenciador de tipo pode 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 no tipo comum das não recursivas. Se não houver ramificações não recursivas, 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 resultado das funções de lançamento de exceção, pode-se usar*como tipo de componente de sequências de comprimento 0, por exemplo da lista vazia; novamente se um elemento for selecionado a partir de uma expressão do tipo [*](lista necessariamente vazia), o tipo resultante *indicará corretamente que isso nunca poderá retornar sem erro.

Marc van Leeuwen
fonte
Então, é a idéia que var foo = someCondition() ? functionReturningBar() : functionThatAlwaysThrows()poderia inferir o tipo de fooas Bar, já que a expressão nunca poderia produzir mais nada?
Supercat 24/03
11
Você acabou de descrever o tipo de unidade - pelo menos na primeira parte da sua resposta. Uma função que retorna o tipo de unidade é a mesma que é declarada como retornando voidem C. A segunda parte da sua resposta, em que você fala sobre um tipo para uma função que nunca retorna, ou uma lista sem elementos - isso é realmente o tipo de baixo! (É muitas vezes escrito como _|_em vez de *Não sei por que Talvez porque ele se parece com um (fundo humano) :)..
andrewf
2
Para evitar dúvidas: 'não retorna nada útil' é diferente de 'não retorna'; o primeiro é representado pelo tipo de unidade; o segundo pelo tipo inferior.
22715 Andrewf
@andrewf: Sim, eu entendo a distinção. Minha resposta é um pouco demorada, mas o argumento que eu queria enfatizar é que o tipo de unidade e o tipo inferior desempenham papéis (diferentes, mas) comparáveis ​​ao permitir que determinadas expressões sejam usadas de maneira mais flexível (mas ainda com segurança).
Marc van Leeuwen
@ supercat: Sim, essa é a ideia. Actualmente no C ++ que é ilegal, apesar de que seria válido se functionThatAlwaysThrows()foram substituídos por um explícito throw, devido à linguagem especial na norma. Ter um tipo que faça isso seria uma melhoria.
Marc van Leeuwen
0

Em alguns idiomas, você pode anotar uma função para informar ao compilador e aos desenvolvedores que uma chamada para essa função não retornará (e se a função for escrita de uma maneira que possa retornar, o compilador não permitirá ) É uma coisa útil a saber, mas no final você pode chamar uma função como essa como qualquer outra. O compilador pode usar as informações para otimização, para fornecer avisos sobre código morto e assim por diante. Portanto, não há uma razão muito convincente para ter esse tipo, mas também não há uma razão muito convincente para evitá-lo.

Em muitos idiomas, uma função pode retornar "nula". O que isso significa exatamente depende do idioma. Em C, significa que a função não retorna nada. No Swift, isso significa que a função retorna um objeto com apenas um valor possível e, como existe apenas um valor possível, esse valor recebe zero bits e não exige nenhum código. Em ambos os casos, isso não é o mesmo que "inferior".

"bottom" seria um tipo sem valores possíveis. Isso nunca pode existir. Se uma função retornar "bottom", na verdade não poderá retornar, porque não há valor do tipo "bottom" que possa retornar.

Se um designer de linguagem quiser, não há motivo para não ter esse tipo. A implementação não é difícil (você pode implementá-la exatamente como uma função retornando nula e marcada como "não retorna"). Você não pode misturar ponteiros para funções retornando inferior com ponteiros para funções retornando nulos, porque eles não são do mesmo tipo).

gnasher729
fonte