Quais são os benefícios de segurança de um sistema de tipos?

Sistemas de tipos impedem erros

Os sistemas de tipos eliminam programas ilegais. Considere o seguinte código Python.

 a = 'foo'
 b = True
 c = a / b

No Python, este programa falha; lança uma exceção. Em uma linguagem como Java, C #, Haskell , o que quer que seja, isso nem é um programa legal. Você evita completamente esses erros porque eles simplesmente não são possíveis no conjunto de programas de entrada.

Da mesma forma, um sistema de tipos melhor exclui mais erros. Se saltarmos para sistemas de tipos super avançados, podemos dizer coisas como esta:

 Definition divide x (y : {x : integer | x /= 0}) = x / y

Agora, o sistema de tipos garante que não haja erros de divisão por zero.

Que tipo de erros

Veja uma breve lista de quais tipos de erros os sistemas podem impedir

1. Erros fora do intervalo
2. Injeção de SQL
3. Generalizando 2, muitos problemas de segurança (o que teste de retenção é para Perl )
4. Erros fora de sequência (esquecendo de chamar o init)
5. Forçando um subconjunto de valores a serem usados (por exemplo, somente inteiros maiores que 0)
6. Gatinhos nefastos (Sim, foi uma piada)
7. Erros de perda de precisão
8. Erros de memória transacional de software (STM) (isso precisa de pureza, o que também requer tipos)
9. Generalizando 8, controlando os efeitos colaterais
10. Invariantes sobre estruturas de dados (é uma árvore binária balanceada?)
11. Esquecendo uma exceção ou jogando a errada

E lembre-se, isso também ocorre no tempo de compilação . Não há necessidade de escrever testes com 100% de cobertura de código para simplesmente verificar erros de tipo, o compilador apenas faz isso por você:)

Estudo de caso: cálculo lambda digitado

Tudo bem, vamos examinar o mais simples de todos os sistemas de tipos, simplesmente cálculo lambda digitado .

Basicamente, existem dois tipos,

Type = Unit | Type -> Type

E todos os termos são variáveis, lambdas ou aplicativo. Com base nisso, podemos provar que qualquer programa bem digitado termina. Nunca há uma situação em que o programa fique preso ou faça um loop para sempre. Isso não é provavel no cálculo lambda normal porque, bem, não é verdade.

Pense nisso, podemos usar sistemas de tipos para garantir que o nosso programa não faça um loop para sempre, muito legal, certo?

Desvio para tipos dinâmicos

Sistemas de tipo dinâmico podem oferecer garantias idênticas como sistemas de tipo estático, mas em tempo de execução, em vez de tempo de compilação. Na verdade, como é tempo de execução, você pode oferecer mais informações. Você perde algumas garantias, no entanto, particularmente sobre propriedades estáticas como rescisão.

Assim, os tipos dinâmicos não excluem determinados programas, mas direcionam os programas malformados para ações bem definidas, como gerar exceções.

TLDR

Portanto, o longo e o curto, é que os sistemas de tipos excluem certos programas. Muitos dos programas são quebrados de alguma forma, portanto, com sistemas de tipos, evitamos esses programas quebrados.

A realidade em si é digitada. Você não pode adicionar comprimentos a pesos. E enquanto você pode adicionar feets a metros (ambos são unidades de comprimentos), você deve dimensionar pelo menos um dos dois. Não fazer isso pode travar sua missão a Marte, literalmente.

Em um sistema de tipos seguros, adicionar dois comprimentos expressos em unidades diferentes teria sido um erro ou teria causado uma transmissão automática.

Um sistema de tipos ajuda a evitar erros simples de codificação, ou melhor, permite que o compilador capture esses erros para você.

Por exemplo, em JavaScript e Python, o problema a seguir geralmente só é detectado no tempo de execução - e, dependendo da qualidade do teste / raridade da condição, pode realmente chegar à produção:

if (someRareCondition)
     a = 1
else
     a = {1, 2, 3}

// 10 lines below
k = a.length

Enquanto um idioma strongmente tipificado forçará você a declarar explicitamente que a é uma matriz e não permitirá que você atribua um inteiro. Dessa forma, não há nenhuma chance de a não ter length - mesmo nos casos mais raros.

Quanto mais cedo no ciclo de desenvolvimento de software você conseguir detectar um erro, menos caro será corrigi-lo. Considere um erro que faz com que seu maior cliente ou todos os seus clientes percam dados. Esse erro pode ser o fim da sua empresa se for detectado apenas depois que clientes reais perderem dados! É claramente menos caro encontrar e corrigir esse bug antes de movê-lo para produção.

Mesmo para erros menos dispendiosos, mais tempo e energia são gastos se os testadores estiverem envolvidos do que se os programadores puderem encontrá-lo e consertá-lo. É mais barato se ele não for verificado no controle de origem, onde outros programadores podem criar software que depende dele. O tipo de segurança impede que certas classes de erros sejam compiladas, eliminando, assim, quase todo o custo potencial desses erros.

Mas essa não é toda a história. Como qualquer um que programa em uma linguagem dinâmica dirá a você, algumas vezes é bom se o seu programa apenas compilar para que você possa experimentar parte dele sem que cada pequeno detalhe funcione. Existe um trade-off entre segurança e conveniência. Testes de unidade podem atenuar alguns dos riscos de usar uma linguagem dinâmica, mas escrever e manter bons testes de unidade tem seu próprio custo, que pode ser maior do que o uso de uma linguagem de segurança de tipos.

Se você estiver experimentando, se seu código será usado apenas uma vez (como um relatório único), se você estiver em uma situação em que você não se importaria em escrever um teste de unidade de qualquer maneira, então uma linguagem dinâmica é provavelmente perfeito para você. Se você tiver um aplicativo grande e quiser alterar uma parte sem interromper o restante, a segurança do tipo é um salva-vidas. Os tipos de erros tipo capturas de segurança são exatamente o tipo de erros que os humanos tendem a ignorar ou errar ao refatorar.

Introdução

A segurança de tipo pode ser obtida com linguagens com tipagem estática (compilada, verificação de tipo estático) e / ou tempo de execução (avaliação, verificação de tipo dinâmico). De acordo com Wikipedia , um '... sistema de tipos strongs é descrito como um em que não há possibilidade de um erro de tipo de tempo não verificado (ed Luca Cardelli). Em outros textos, a ausência de erros de tempo de execução não verificados é chamada de segurança ou segurança de tipos ... '

Segurança - Verificação de tipo estático

Classicamente, type safety tem sido sinônimo de tipagem estática, em linguagens como C, C ++ e Haskell, que são projetadas para detectar erros de digitação de tipos quando são compilados. Isso tem o benefício de evitar condições potencialmente indefinidas ou propensas a erros quando o programa é executado. Isso pode ser inestimável quando existe o risco de os tipos de ponteiros serem incorretos, por exemplo, uma situação que poderia levar a conseqüências catastróficas, se não detectadas. Nesse sentido, a tipagem estática é considerada sinônimo de segurança de memória.

A tipagem estática não é completamente segura, mas aumenta a segurança, no entanto. Mesmo os sistemas com tipos estáticos podem ter conseqüências catastróficas. Muitos especialistas consideram que o tipo estático pode ser usado para escrever sistemas mais robustos e menos propensos a erros (de missão crítica).

Linguagens com tipos estáticos podem ajudar a reduzir o risco de perda de dados ou perda de precisão no trabalho numérico, que pode ocorrer devido a erros de correspondência ou truncamento duplo para flutuar ou correspondência incorreta e tipos flutuantes.

Existe uma vantagem em usar linguagens com tipagem estática para eficiência e velocidade de execução. O tempo de execução se beneficia de não precisar determinar os tipos durante a execução.

Segurança - Verificação do tipo de tempo de execução

Erlang, por exemplo, é um tipo declarado, tipo dinamicamente, que é verificado em uma máquina virtual. O código Erlang pode ser compilado por byte. Erlang é considerado talvez a mais importante linguagem de missão crítica, tolerante a falhas disponível, e é relatado que Erlang tem uma confiabilidade de nove 9's (99,9999999% ou não mais de 31,5 ms por ano).

Certos idiomas, como o Common Lisp, não são estaticamente tipados, mas os tipos podem ser declarados, se desejado, o que pode ajudar a melhorar a velocidade e a eficiência. Também deve ser notado que muitas das linguagens interpretadas mais amplamente utilizadas, como o Python, são, por baixo do loop de avaliação, escritas em linguagens com tipagem estática, como C ou C ++. O Commom Lisp e o Python são considerados seguros pelo tipo acima.

the safety benefits of a type system are lost.

So first of all, what actually is safety? protection against data corruption, or hackers, or system malfunctions, etc.?

What are the safety benefits of a type system? What makes a type system different that allows it to provide these safety benefits?

Eu sinto que os sistemas de tipos têm uma visão tão negativa. Um sistema de tipos é mais uma garantia do que provar a ausência de erros. Este último é uma consequência do sistema de tipos. Um sistema de tipos para uma linguagem de programação é uma maneira de produzir, em tempo de compilação, uma prova de que um programa atende a algum tipo de especificação.

O tipo de especificação que um pode codificar como um tipo depende da linguagem, ou mais diretamente, da força do sistema de tipos da linguagem.

O tipo mais básico de especificação é uma garantia sobre o comportamento de entrada / saída de funções e da validade do interior de um corpo de função. Considere um cabeçalho de função

f : (Int,Int) -> String

Um bom sistema de tipos garantirá que f seja aplicado apenas a objetos que produzirão um par de Int quando avaliados, e garante que f sempre produzirá uma string.

Algumas declarações em uma linguagem, como blocos if-then, não possuem um comportamento de entrada / saída; aqui o sistema de tipos garante que cada declaração ou declaração no bloco seja válida; isso é aplica operações a objetos do tipo correto. Essas garantias são composíveis.

Além disso, isso dá uma espécie de condição de segurança da memória. A citação com a qual você está lidando é sobre elenco. Em alguns casos, a conversão é boa, como converter um Int de 32 bits em um Int de 64 bits. No entanto, geralmente, falha o sistema de tipos.

Considere

Foo x = new Foo(3,4,5,6);
f((Int)x,(Int)x);

Por causa do casting, x é transformado em um Int, então, tecnicamente, o tipo acima verifica; no entanto, ele realmente derrota o propósito do typechecking.

Uma coisa que poderia fazer um sistema de tipos diferente e melhor é dissallow casts (A) x onde x antes do caso ser do tipo B, a menos que B seja um subtipo (ou sub-objeto) de A. As idéias da teoria de subtipagem foram usado em segurança para remover a possibilidade de ataques de estouro / estouro de números inteiros.

Resumo

Um sistema de tipos é uma forma de provar que um programa atende a algum tipo de especificação. Os benefícios que um sistema de tipos pode fornecer dependem da força do sistema de tipos usado.

Uma vantagem ainda não mencionada para um sistema de tipos centra-se no facto de muitos programas serem lidos mais do que estão escritos e, em muitos casos, um sistema de tipos pode permitir que muita informação seja especificada de uma forma concisa e pode ser facilmente digerida por alguém que esteja lendo o código. Embora os tipos de parâmetro não ocupem o lugar de comentários descritivos, a maioria das pessoas achará mais rápido ler: "int Distância"; ou Distance As Int32 do que ler "A distância deve ser um número inteiro +/- 2147483647"; passar frações pode produzir resultados inconsistentes. "Além disso, os tipos de parâmetro podem ajudar a reduzir a lacuna entre o que uma implementação específica de uma API faz, versus o que os chamadores podem confiar. Por exemplo, se uma implementação JavaScript específica de uma API usa seus parâmetros de uma maneira que forçaria qualquer string à forma numérica, pode não ser claro se os chamadores podem confiar em tal comportamento, ou se outras implementações da API podem funcionar incorretamente se forem dadas strings.Ter um método cujo parâmetro é especificado como Double deixaria claro que qualquer valor de string deve ser coagido pelo chamador antes de ser passado, ter um método com uma sobrecarga que aceite Double e outro que aceite String tornaria um pouco mais claro que chamadores com strings seriam permitidos para passá-los como tal.

So first of all, what actually is safety? Protection against data corruption, or hackers, or system malfunctions, etc.?

Todas as outras respostas e mais. Em geral, "segurança de tipo" significa simplesmente que nenhum dos programas compilados com sucesso pelo compilador conterá erros de tipo.

Agora, o que é um erro de tipo? Em princípio, você pode especificar qualquer propriedade indesejável como um erro de tipo, e alguns sistemas de tipos poderão assegurar estaticamente que nenhum programa tenha tal erro.

Por "propriedade" acima, quero dizer algum tipo de proposição lógica que se aplica ao seu programa, por exemplo, "todos os índices estão dentro dos limites da matriz". Outros tipos de propriedades incluem: "todos os ponteiros deferenciados são válidos", "este programa não executa nenhuma E / S" ou "este programa executa somente E / S para / dev / null", etc. Apenas sobre qualquer tipo de propriedade pode ser especificada e digitada dessa maneira, dependendo da expressividade do seu sistema de tipos.

Sistemas de tipos dependentes estão entre os sistemas de tipos mais gerais, através dos quais você pode impor praticamente qualquer propriedade que desejar. Não é necessariamente fácil fazê-lo, já que propriedades sofisticadas estão sujeitas a incompletude cortesia de Gödel .