Skip to content

Latest commit

 

History

History
168 lines (120 loc) · 6.96 KB

1.introducao.md

File metadata and controls

168 lines (120 loc) · 6.96 KB
Raw

Índice

1. Introdução

Bem-vindo a esse curso! Esse projeto pretende ajudar você a aprender a programar na linguagem de programação Idris2 e entender sua filosofia e com isso fazer um futuro com software que quebre menos e seja mais fácil de se provar correto. Para compreender melhor esse livro, é importante saber o básico de programação.

1.1 O que é Idris

Idris é uma linguagem de programação puramente funcional que surgiu em 2007 visando usar técnicas de verificação de software state-of-art em uma linguagem de programação que teria potencial para ser mainstream. Idris é muito influenciado por outras 3 linguagens funcionais (Agda, Haskell e Epigram), mas com a característica de ter linear types e dependent types.

Não se preocupe se você não entendeu metade dessas coisas, nós iremos caminhar por cada uma das características dentro desse curso. Mas em resumo, Idris é uma linguagem muito resiliente a falhas e tenta delegar muitas das tarefas de verificação do software para o compilador.

1.2 Diferenças entre Idris 1 e Idris 2

Idris1 foi uma tentativa de fazer uma linguagem prática, mas como toda primeira tentativa, ela teve seus erros e Idris2 é uma versão atualmente mais robusta e resolve grande parte desses problemas como, por exemplo:

1.3 Instalação

Instalar Idris2 ainda é um processo árduo e com muita tentativa e erro (se você quiser instalar coisas para o Idris além do compilador). Porém, ainda sim, é possível instalar tanto no Windows (usando WSL) quanto no Linux.

1.3.1 Usuários de Ubuntu

A instalação no ubuntu é direta ao ponto. Porém, desse modo você não conseguirá instalar o Idris2 LSP já que não tem como instalar o Idris2 API.

sudo apt install idris2

1.3.2 Usuários de Linux

  1. Clonar o repositório do Idris2 https://github.com/idris-lang/Idris2

  2. Entrar no repositório e buildar fazendo bootstrap usando o Chez Scheme (Precisa ter o chez scheme instalado e isso depende de cada distribuição linux) sudo apt install chez
    cd Idris2 && make bootstrap scheme=SCHEME

  3. Após isso é necessário usar make install para colocar no lugar adequado. Caso você não consiga usar o comando idris2 tente colocar o caminho ~/.idris2/bin na variável de ambiente PATH e reinicie o terminal.

1.3.2.1 Instalar o Idris2 LSP no Linux

  1. Primeiro é necessário remover os arquivos de build do Idris2 já que a versão que você compilou provavelmente é mais antiga do que o compilador que você já tem.

    • cd Idris2 && rm -r build
    • idris2 --install idris2api.ipkg (Para instalar a API)

  2. Clonar o repositório do Idris2 LSP

    • https://github.com/idris-community/idris2-lsp
    • Buildar ele com make install

  3. Instalar a extensão correspondente no seu editor de texto. No caso do Visual studio code a extensão recomendada é idris2-lsp

1.3.3 Para usuários de Windows

  1. Instalar uma distribuição linux para WSL
  2. Fazer os passos para windows dentro do WSL

Um bom video para isso é o do Identity GS:

Install Idris2 on Windows using WSL - Tutorial

1.4 Hello World em Idris

Uma explicação superficial — e que você não precisa entender totalmente — desse Hello World é:

  • Primeira linha explicita que o nome do módulo é Main
  • Terceira linha declara a função main com tipo IO () que faz a função poder usar funções de entrada e saída de dados e retorna o tipo Unit (())
  • Quarta linha declara que a função main tem como valor a ação mostrar na tela o "Hello, World"

Arquivo: Main.idr

module Main

main : IO ()
main = putStrLn "Hello, World!"

1.5 REPL

Para melhorar o REPL do Idris, podemos utilizar uma dependência chamada rlwrap. Instalar essa dependência é bem simples, porém, depende de cada sistema.

$ rlwrap idris2

     ____    __     _         ___                                           
    /  _/___/ /____(_)____   |__ \                                          
    / // __  / ___/ / ___/   __/ /     Version 0.5.1-0a4fd3dc0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           
 /___/\__,_/_/  /_/____/   /____/      Type :? for help                     

Welcome to Idris 2.  Enjoy yourself!

Main> 23 * 32 +3-233
506

Há vários comandos úteis no REPL do Idris:

  • :help Que mostra uma lista de comandos
  • :t Que mostra o tipo da expressão 
    Main> :t 3
3 : Integer
  • :q Para sair
  • :module Para importar um módulo como por exemplo 
    Main> :module Data.List
Main> zip [1,2,3] [4,5,6]
[(1, 4), (2, 5), (3, 6)]
  • :doc Que mostra a documentação para uma certa palavra chave ou nome. 
    Main> :doc reverse

Prelude.reverse : String -> String
Reverses the elements within a string.

``idris example
reverse "ABC"
``
``idris example
reverse ""
``
Totality: total
  • :l Para carregar um arquivo
  • :r Para recarregar um arquivo
  • :exec Para executar comandos de IO tal como: 
    Main> :exec putStrLn "☆*:.｡.o(≧▽≦)o.｡.:*☆"
☆*:.｡.o(≧▽≦)o.｡.:*☆

1.6 Materiais para aprender sobre Idris

Todas palestras sobre Idris1 dão uma boa introdução tanto sobre Idris2 quanto Idris1

Link Description
https://idris2.readthedocs.io/ Tutorial oficial feito para pessoas que já tem noção de Ocaml ou Haskell
https://www.youtube.com/watch?v=X36ye-1x_HQ Sobre Idris1 e Desenvolvimento orientado a tipos
https://www.youtube.com/watch?v=zSsCLnLS1hg Um curso de 4 aulas sobre Idris1
https://www.youtube.com/watch?v=nbClauMCeds Novidades em Idris2
https://www.youtube.com/watch?v=mOtKD7ml0NU Desenvolvimento orientado a tipos em Idris2
https://www.youtube.com/watch?v=_prvbd0e_pI Entrevista com Edwin Brady sobre Idris2
PROXIMO