Básico
Introdução
O estilo de programação funcional traz programação mais perto da simples e cotidiana matemática: Se um procedimento ou método não tem efeitos colaterais, então (ignorando eficiência) só o que precisamos entender sobre ele é como mapear entradas para saídas - ou seja, podemos pensar nele como um método concreto que computa uma função matemática. Esse é um dos sentidos do "funcional" em "programação funcional". A conexão direta entre programas e objetos matemáticos simples suporta tanto a formalidade de provas de corretude quanto a racionalização informal sobre o comportamento do programa.
O outro sentido na qual programação funcional é "funcional" é que ela enfatiza o uso de funções "ou métodos" como valores de primeira classe - ou seja, valores que podem ser passados como argumentos para outras funções, retornados como resultados, incluídos em estruturas de dados, etc. O reconhecimento de que funções podem ser tratadas desse jeito como dados habilita uma gama de comandos úteis.
Outras funcionalidades comuns de linguagens funcionais incluem algebraic data types e pattern matching, o que torna fácil construir e manipular estruturas de dados, e sistemas de tipo polimórficos sofisticados, suportando abstração e reuso de código. Kind contém todas essas funcionalidades.
A primeira metade desse capítulo introduz os elementos mais básicos da linguagem de programação funcional Kind. A segunda metade introduz algumas técnicas básicas que podem ser usadas para provar propriedades em programas em Kind.