2021. Desenvolvimento Orientado a Tipos

1 Apresentação

Em sistemas de computação com aplicações sensíveis (área financeira, lançamento de um foguete, etc…) busca-se por códigos comprovadamente livres de falhas. O modelo tradicional para assegurar a qualidade do software se baseia na detecção de falhas durante a execução através da criação e execução de testes automatizados. Este método, por sua natureza, garante apenas que especificamente o que foi testado funciona conforme verificado pelos testes. Como o número de testes é finito, tais técnicas não raramente são combinadas com a avaliação da cobertura de código. Ainda assim, este método não é capaz de provar que não há falhas assim como não impede que códigos incorretos sejam escritos. Ademais, para qualquer software de tamanho razoável a complexidade ciclomática para que todos os caminhos de execução sejam verificados torna a escrita de testes de maneira manual proibitivamente complexa.

Um modelo complementar é o da utilização de tipos e funções com restrições de tal forma a maximizar a localização de erros em tempo de compilação, evitando que eles ocorram durante a execução. Esta abordagem evita a escrita de diversos testes automatizados que, por definição, perdem o seu sentido em uma linguagem com tipagem mais restritiva já que o compilador ou prova que tais situações são impossíveis ou emite um erro de compilação.

2 Objetivos

Neste curso sobre Programação Orientada a Tipos nós vamos explorar em detalhes as principais técnicas que são empregadas para evitar erros durante a execução. Para isto utilizaremos ferramentas que, em sua maioria, ainda não estão presentes nas principais linguagens utilizadas hoje no mercado.

Ao fim do curso, você deverá ser capaz de criar aplicações que, se não forem 100% type safe, pelo menos serão capazes de evitar vários erros em tempo de execução.

Se conseguimos salvar pelo menos um de vocês de terem que trabalhar na véspera de natal para atender um chamado por um pau que deu em produção, já vai ter valido a pena! :-D

3 Pré-requisitos

É exigido que os participantes tenham uma ótima familiaridade com programação. A linguagem de programação utilizada é Haskell, logo familiaridade com programação funcional e Haskell é um diferencial!

Se Haskell ou programação funcional não é o seu forte, aproveite para fazer uma maratona dos nossos vídeos sobre programação funcional em Haskell e seguir o material didático que acompanham esses vídeos disponível aqui.

4 Conteúdo

  • Breve revisão de Haskell, tipos, restrições (constraints)
  • Polimorfismo paramétrico e ad-hoc
  • Tipos de dados algébricos (algebraic data types - ADTs)
  • Tipos fantasmas (phantom types)
  • Tipos, Kinds, Sorts
  • Tipos existenciais (existential types)
  • Tipos de dados algébricos generalizados (Generalized Algebraic Data Types - GADTs)
  • Família de tipos (type family)

As aulas serão liberadas dia a dia no Youtube. A lista de vídeos com o curso completo pode ser acompanhada aqui: https://www.youtube.com/watch?v=KTmHPTxKIBY&list=PLYItvall0TqKaY6qObQMlZ45Bo94xq9Ym

Assine, clique o sininho coisa e tal para ser notificado!

Já o texto de apoio (e links pra os vídeos relevantes) você acha aqui: Desenvolvimento Orientado a Tipos.

Dúvidas, pelo Discord: https://discord.gg/DtQtBWvwzg

5 Programação e formato do curso

O curso ocorrerá entre os dias 29/Nov. e 12/Dez. Devido às restrições a nós impostas pela pandemia, ele será ministrado de maneira totalmente online e aberta a todos os interessados.

Todo o material (vídeos + texto de referência) ficará disponível abertamente na internet e assim ficará mesmo após o término do curso.

Durante este período os professores liberarão o material de estudos e novos vídeos diariamente (ou quase!). Interações com os professores serão feitas pelo servidor do Discord e em aulas online e síncronas cuja data e hora será definida por uma enquete com os inscritos.

6 Inscrições

As inscrições estarão abertas até dia 26/Nov. Para se inscrever é muito fácil!

Por motivos práticos o número de inscrições será limitado a 100 pessoas. Esse limite é necessário para que tenhamos tempo hábil para corrigir as tarefas dos inscritos e consigamos emitir o certificado de participação.

Você, contudo, não precisa de uma inscrição para acompanhar o curso ou para interagir com os professores pelo Discord ou nas aulas síncronas! Basta aparecer! Ou seja, se você acha que não vai ter tempo suficiente para fazer as tarefas mas ainda assim quer acompanhar o curso, fique a vontade! Compareça, participe e deixe a vaga livre para outros colegas!

7 Responsáveis, contatos, etc…

O curso foi desenvolvido pelos Profs. Fabrício Olivetti e Emilio Francesquini da Universidade Federal do ABC.

Contatos: