Alan Bertani

Rapaz, eu fiz a mesma pergunta há 10 anos, e, na época, eu não entendi a resposta, até briguei com o carinha que tentou me ensinar kkkk. Hoje, eu entendo, mas admito que é meio difícil comunicar. Vou tentar responder da forma que EU penso, ok? A teoria dos tipos estuda a lógica por trás da estrutura todos os programas. Ela vai além de te ensinar a programar em uma linguagem específica; ela revela uma "linguagem universal" por trás de todas as outras. É como se alguém tivesse pego o Python, Java, C, etc., virado eles do avesso, e descoberto que, por trás de todos, existe o mesmo "idioma comum". Esse idioma é o Inter... err, digo, a Teoria dos Tipos. Tá, mas qual a vantagem disso? Acontece que, quando você domina esse "idioma comum", você acaba percebendo que ele é surpreendentemente conveniente para modelar e resolver um leque amplo de problemas. E, pra melhorar: quando você resolve um problema nesse idioma, é muito fácil transcrever sua solução para qualquer linguagem específica; afinal, todas são derivadas da Teoria dos Tipos! Com o tempo, esse processo se torna tão útil que, eventualmente, a TT se torna sua "linguagem interna" de raciocínio; como se fosse o "Português" dos códigos; e isso é mais útil que eu consigo colocar em palavras, de uma forma universal. Talvez isso soe meio abstrato, então, vou tentar dar um exemplo concreto. Há alguns dias atrás, eu publiquei um algoritmo em TypeScript (gist.github.com/VictorTaelin/d…), e aí um carinha comentou que meu código nem parece TS, pois era "simétrico e organizado como se fosse outro idioma, porém que, de alguma forma, se encaixou perfeitamente bem à sintaxe do TypeScript". E foi exatamente isso que ocorreu: na minha cabeça, eu implementei a solução na Teoria dos Tipos, e apenas "transcrevi" para a primeira linguagem que apareceu. Da mesma forma, hoje eu consigo usar confortavelmente qualquer linguagem, porque, internamente, eu estou usando apenas uma. Em resumo, a Teoria dos Tipos te oferece uma nova forma de pensar e modelar problemas, que acaba sendo extremamente conveniente, a ponto de se tornar sua forma principal de pensar sobre, e abordar, a programação. É a melhor oferta da sua vida: "aprenda um linguagem, domine todas". O video abaixo é uma explicação beeeem simplificada (TT nerds, não briguem comigo) para ilustrar esse ponto.

Um candidato me pediu um "desafio muito difícil" valendo vaga. Gosto disso. Segue o desafio: > Implemente um normalizador para o cálculo lambda não tipado afino, usando Agda. Crie um tipo indutivo para termos, assegurando a linearidade das variávies. Crie uma função normalize, que comprovadamente retorna a forma normal do termo original. Qualquer um capaz de terminar esse exercício, e explicar sua solução, tem uma vaga garantida na HOC, com ou sem posições abertas. É super difícil, mas totalmente "fazível" em um dia de trabalho. Não recomendo tentar, mas, se alguém fizer, já pode mandar a solução junto com a carteira pra gente assinar @sseraphini @ViUmaVaga @tuiteirodevagas #vagas #vagastech #bolhadev