Lógica em Kind

Nos capítulos anteriores, vimos muitos exemplos de proposições e formas de apresentar evidências de sua veracidade (provas). Em particular, trabalhamos extensivamente com proposições de igualdade da forma e1 = e2, com implicações (p -> q), e com proposições quantificadas (x -> P(x)). Neste capítulo, veremos como Kind pode ser usado para realizar outras formas familiares de raciocínio lógico.

Antes de mergulhar nos detalhes, vamos falar um pouco sobre o status das declarações matemáticas em Kind. Lembre-se de que Kind é uma linguagem tipada, o que significa que toda expressão sensível em seu mundo tem um tipo associado. As afirmações lógicas não são exceção: qualquer afirmação que possamos tentar provar em Kind tem um tipo, ou seja, Type, o tipo de proposições. Podemos ver isso com o tipo Booleano:

Bool: Type
Bool.true  : Bool
Bool.false : Bool

No tipo Bool nós temos o Bool.true e o Bool.false. Para criar o tipo Bool nós declaramos que ele é um tipo (Type) e depois que o Bool.true e o Bool.false são do tipo Bool. Vendo como é, fica bem mais simples. Muitas vezes nos assombramos ao ver o nome "funcional", mas Kind é uma linguagem muito amigável, veremos bem sobre isso mais para a frente.

Outro exemplo possível é o Nat, dos números naturais. Números naturais são todos os números inteiros maiores ou igual a zero. Ou seja, eles começam com o número zero e vão até o infinito, mas não possuem valores decimais. Ou seja, o 3 é um número natural, mas o 3,14 não é, da mesma forma que o -3 também não é. Então sabemos que o número natural é feito de zero e dos sucessores dele. Vamos ver como isso é no kind:

Nat: Type
Nat.zero             : Nat
Nat.succ (pred: Nat) : Nat

Percebemos que a construção é similar aos Booleanos, mas há um elemento extra no Nat.succ, que é o "(pred: Nat)", e isso se deve ao fato de que, enquanto no outro nós tínhamos apenas duas opções de retorno (True ou False), agora temos uma infinidade de números que o código precisa compreender, além de que deve haver uma forma do código parar de rodar (veremos mais sobre isso ao decorrer desse estudo), uma vez que um código que nunca para de rodar é um código que nunca nos dará o resultado.

Porém, de qualquer forma, percebemos que a estrutura do Nat é basicamente a mesma do Bool, isso nos mostra que podemos criar qualquer tipo, desde que sigamos a mesma estrutura. Vamos criar o tipo suco:

Suco : Type
Suco.laranja : Suco
Suco.caju    : Suco

O suco de laranja possui dois construtores, o Suco.laranja e o Suco.caju. Esse tipo é fictício, ele não existia até então, mas agora podemos usar ele como um tipo e isso nos mostra que, graças ao design do Kind, podemos criar uma infinidade de tipos, pois todo tipo é uma função.

Entender a construção dos tipos impedirá que alguns erros de sintaxe ocorram.

Apenas revisando, nosso elemento Suco é do tipo Type e o Suco.laranja é do tipo Suco. Desta forma, em termos leigos, temos que o elemento fica a direita dos dois pontos e o tipo a esquerda

elemento : Tipo

Como dito antes, até mesmo os tipos são funções, logo podemos ter uma função como tipo. Por exemplo:

Problema : (Equal Bool Bool.true Bool.true

Podemos perceber que temos um elemento chamado "Problema" e ele é do tipo "(Equal Bool Bool.true Bool.true)". Nós já vimos essa estrutura diversas vezes nos últimos capítulos e agora é fácil entender que essa função é um tipo e, da mesma forma que não escrevemos

Suco: Type
Suco.laranja : Type

Não podemos simplesmente copiar a função para os construtores desse tipo. O Suco é tipo Type, mas o Suco.laranja não é do tipo Type, ele é do tipo Suco.

Mas atenção, observe que todas as proposições sintaticamente bem formadas têm o tipo Type em Kind, independentemente de serem verdadeiras ou não. Simplesmente ser uma proposição é uma coisa; ser demonstrável é outra coisa!

De fato, as proposições não têm apenas tipos: elas são objetos de primeira classe que podem ser manipulados da mesma forma que as outras entidades no mundo de Kind. Até agora, vimos um local primário onde as proposições podem aparecer: nas assinaturas de tipo das funções.

Plus_2_2_is_4 : Equal (Plus 2n 2n) 4n
Plus_2_2_is_4 = Equal.refl

Mas as proposições podem ser usadas de muitas outras maneiras. Por exemplo, podemos dar um nome a uma proposição como um valor próprio, assim como demos nomes a expressões de outros tipos.

Plus_fact : Type
Plus_fact = Equal (Plus 2n 2n) 4n

Posteriormente, podemos usar esse nome em qualquer situação em que uma proposição seja esperada – por exemplo, em uma declaração de função.

Plus_fact_is_true : Plus_fact
Plus_fact_is_true = Equal.refl

Também podemos escrever proposições parametrizadas – isto é, funções que recebem argumentos de algum tipo e retornam uma proposição. Por exemplo, a seguinte função pega um número e retorna uma proposição afirmando que esse número é igual a três:

Is_three (n: Nat) : Type
Is_three n = Equal Nat n 3n

Em Kind, diz-se que funções que retornam proposições definem propriedades de seus argumentos. Por exemplo, aqui está uma propriedade (polimórfica) que define a noção familiar de uma função injetiva

Injective <a> <b> (f: a -> b) : Type
Injective a b f = (x: a) -> (y: a) -> (e: Equal b (f x) (f y)) -> (Equal a x y)

Nós podemos instanciar uma regra de injetividade com

Nat.succ_injective : Injective ((x: Nat) => Nat.succ x)
Nat.succ_injective =
  (a: Nat) =>
  (b: Nat) =>
  (e: Equal Nat (Nat.succ a) (Nat.succ b)) =>
  Equal.apply (x => Nat.pred x) e