the-sofi-uwu/Idris2Noobs

Idris2 para falantes de portugues.

Idris2Noobs

Uma introdução a linguagem de programação Idris2 em português.

Todo

• Escrever tudo
• Melhorar site e botar questões como Quiz
• Refazer os desenhos pra deixar mais explicativos

Sumário

1. Introdução

• 1.0 Introdução
• 1.1 O que é Idris
• 1.2 Diferenças entre Idris 1 e Idris 2
• 1.3 Instalação
  • 1.3.1 Usuários de Ubuntu
  • 1.3.2 Usuários de Linux
  • 1.3.2.1 Instalar o Idris2 LSP no Linux
  • 1.3.3 Para usuários de Windows
• 1.4 Hello World em Idris
• 1.4 Materiais para aprender sobre Idris

2. Adivinhe o número

• 2. Descubra o numero!
• 2.1 Criando um projeto
• 2.2 O arquivo principal
• 2.3 Como rodar

3. Tipos primitivos e funções

• 3.1 Tipos primitivos e funções
• 3.2 Definições
• 3.3 Funções
• 3.4 Currying
• 3.5 Composição
• 3.6 Recursão
• 3.7 Funções do Preludio
• 3.8 Totalidade e Holes
• 3.9 Funções de ordem alta

4. Estruturas úteis

• 4 Expressões Úteis
• 4.1 Let e Where
  • 4.1.1 Let bindings
  • 4.1.2 Where
• 4.2 Cast e The
• 4.3 Expressão If
• 4.4 Case

5. Brincando com IO

• 4. Brincando com IO
• 4.1 PrintLn e PutStrLn
• 5.2 Notação do
• 5.3 getLine

6. Tipos algebricos e compostos.

• 6.1 Listas
  • 6.1.1 Funções úteis e o módulo Data.List
• 6.2 Type variables
• 6.2 Type Constructors e Data Constructors
• 6.3 Records
• 6.4 Exemplos de ADT
  • 6.4.1 Listas
  • 6.4.2 Maybe
  • 6.4.3 Either
  • 6.4.4 Tuplas
• 6.5 Pattern matching
• Exercicios

8. Interfaces

• Interfaces
• Extendendo Interfaces
• Constraints
• Categorias
  • Functor
  • Semigroup
  • Monoid
  • Applicative
  • Monad
• Exercicios

9. Dependent Types

• Tipos de primeira classe
• Tipos dependendo de termos
• Dependent Records
• Pares dependentes
• Exemplos de Dependent Types
  • Vetores Indexados
  • Sets finitos
  • Função Arity
• Argumentos implicitos
• Exemplos de código
  • Printf
  • Server Path Dependente
• Exercicios

10. Multiplices

• Linear Types
• Exemplos:
  • A porta