Oi, gente! O meu nome é Eduardo Ochs, e eu tou
pretendendo dar uma oficina de Lean4
daqui um tempo... e esse vídeo é para
explicar algumas coisas que seriam
difíceis de explicar só por uma página
na internet.
Os dados da oficina vão estar todos
aqui nessa URL, e essa daqui é minha
página sobre Lean4.
Primeiro: o que que é o Lean4?
O Lean4 é parecido com Haskell, mas
ele é bem mais fácil de instalar, e tem
uma interface muito bacana que eu vou
mostrar daqui a pouco. Ele pode ser usado
como proof assistant - muita gente pensa
nele como proof assistant, só que eu ainda
não sei usar ele como proof assistant...
eu comecei a aprender ele porque eu queria
usar ele como proof assistant pra umas
coisas super complicadas, e...
ainda não sei o suficiente para isso...
mas tou adorando ele como uma linguagem
parecida com Haskell, e mais legal, com uma
interface bacana, e tal...
e o mais importante é que ele é muito
extensível - no sentido de que é fácil
você definir sintaxes novas nele... definir
mini-linguagens, DSLs, todas essas coisas
assim... se vocês quiserem explicações pra
isso tem nesse manual daqui, já vou
explicar qual é...
então, um dos manuais principais do Lean4
é o "Metaprogramming in Lean4",
e aí um dos capítulos
explica essa história de definir as
sintaxes novas - nessa seção daqui.
Voltando...
Primeiro: quem é o público alvo dessa
oficina?
Vai ser uma oficina muito básica, e
a ideia é que ela vai ser direcionada
pra pessoas que tentaram aprender Haskell
mas que empacaram mais ou menos nos mesmos
lugares que eu.
A partir de um determinado ponto os
livros começam a mostrar umas coisas
super complicadas e meio que exigir que
a gente entenda todos os detalhes delas
de cabeça... eles não dão nenhuma
informação sobre como a gente poderia
fazer as "contas" no papel pra conseguir
entender os detalhes daquilo.
Então - aqui tem um exemplo. Um
amigo meu que tá trabalhando na Holanda...
uma das tarefas dele como pós-doc é
orientar os alunos que estão fazendo
curso de Haskell lá... e eles usam o livro
do Hutton, então eu tentei aprender a usar
livro do Hutton também... a capa dele é essa,
aqui tá o índice do livro...
e o capítulo 12 do livro é o capítulo
onde ele começa a explicar mônadas.
E aí ele...
define umas coisas que eu só fui entender agora...
eu já tentei decifrar esse capítulo várias
vezes nos últimos três ou quatro anos e só
comecei a entender agora...
então, ele tem essas figurinhas aqui para
explicar o que que é uma "state monad".
E aí ele define
essa coisa daqui, ó...
ele diz que a gente vai definir um tipo
novo desse jeito daqui...
e depois uma função "app", que usa esse tipo...
depois uma função "fmap", que é uma instância
do funtor ST, whatever that means...
e aí ele põe essa figurinha daqui.
Até hoje de tarde eu não fazia a menor
ideia de se essa figura era uma coisa
precisa ou não.
Se fosse certamente estavam faltando
muitos detalhes aqui, e
eu ainda não tinha certeza de como
completar esses detalhes.
Então... deixa eu mostrar uma
figura aqui.
Essa primeira definição... essas duas
definições daqui, essa e essa, estão nesse
primeiro diagrama.
Então, no livro do Hutton
elas aparecem como essas três linhas
daqui - essa definição de um newtype,
depois o tipo da da função "app", depois a
definição da "app" em si...
e aí esse tipo de figura daqui
me ajudou muito a decifrar essas coisas.
Eu pego essa expressão daqui de baixo,
e embaixo de cada subexpressão dela
eu escrevo qual é o tipo dela.
O ideal seria fazer uma animação
dizendo quais são os tipos que eu
descubro primeiro e como é que a
inferência de tipos funciona, e como é
que a gente vai descobrindo tudo aos
poucos... mas nesse caso aqui eu ainda não
fiz a animação.
Então, a grande dificuldade para mim
foi entender o que é essa operação S daqui
e esse underbrace daqui...
e o legal é que quando
eu faço esse tipo de diagrama eu consigo
apontar pra um underbrace e
dizer: é esse o underbrace que eu
ainda não tenho certeza... e depois de
horas eu descobri que se eu
escrevesse esse underbrace desse jeito
daqui... desculpa, esse underbrace daqui...
usando essa definição de newtype aqui, que diz
que "ST a" é sempre equivalente a
S (State→(a,State)),
aí tudo ficava claro... aí as
regras não ficavam mais tão
misteriosas.
Então, voltando.
Até pouquíssimo tempo atrás eu não sabia
decifrar
trechos difíceis do Hutton - eu não
sabia que ferramentas usar para
completar os detalhes deles... e esse tipo
de diagrama tem me ajudado muito.
Agora vem o diagrama... opa, peraí...
ah deixa eu mostrar o diagrama da página
seguinte... aqui.
Lembra que agora há pouco eu mostrei
essa figurinha no livro do Hutton
e disse que até pouco tempo atrás eu não
fazia ideia de se essa figura era só uma...
se ela era informal ou não...
então, nessa página o o Hutton introduz
algumas linhas a mais, aqui...
ele diz que a gente vai definir o fmap desse
jeito daqui, e aí ele mostra essa figura como
se fosse óbvia... e para mim ela não é!
Eu preciso fazer todas essas type
inferences daqui para descobrir qual é o
tipo
da g da st, da s, da x, da s', etc, e
das outras expressões que são compostas
a partir delas... e aí quando eu descubro
todos esses tipos daqui eu consigo
transformar esse diagrama daqui num
diagrama que tem não só esses símbolos
que são nomes de termos, como esses tipos
daqui...
então esse s daqui é de tipo State
essa coisa daqui é de tipo ST a, etc...
e aí tudo fez sentido para mim.
Então, voltando... agora eu preciso contar uma
historinha, tá... eu vou contar ela de um
jeito bem resumido e eu vou botar o link
do lugar onde vocês podem ler o texto dela.
Há um tempo atrás eu fiz dois
vídeos sobre didática... um deles ficou
muito bom e outro tem só alguns trechos bons.
Esse vídeo é o que tem alguns trechos bons.
E ele tem essa historinha que eu
acho bem importante. É o seguinte... eu
não vou ler ela toda agora, mas é
uma história sobre alguém... um
professor que ensina uma coisa super
difícil, um aluno não entende e ele diz:
"mas isso é óbvio!" Aí o aluno diz:
"não é óbvio não!"... mas o aluno vai
pra casa pensar, ele pensa, pensa, pensa muito,
depois no dia seguinte ele volta e ele
virou uma pessoa para quem aquilo é
óbvio. Ele não sabe explicar pra as
outras pessoas quais são os detalhes
daquilo, ele só sabe dizer pras pessoas
"ah, isso é óbvio!"... mas ele virou a
pessoa para quem isso é óbvio.
Eu não gosto dessa ideia de aprender coisas
complicadas e virar uma pessoa que só
sabe dizer "ah, isso é óbvio!", e e eu tou há
vários anos trabalhando em alternativas
pra isso. Essa alternativas são descobrir
os diagramas que faltam e encontrar um
jeito mais ou menos mecânico e formal de
produzir esses diagramas que faltam.
Então, essa oficina de Lean
vai ser principalmente sobre um modo de
produzir esses diagramas que faltam e de
apresentar as coisas que os livros sobre Lean
apresentam de um jeito muito difícil
com esses diagramas.
Então vou mostrar os pontos em que eu
empacava... e que ficaram
muito mais simples depois que eu aprendi
a fazer diagramas. Então: não tenho
certeza se esses diagramas vão funcionar
pra outras pessoas - é isso que eu quero
testar - mas são os diagramas que
funcionaram para mim.
E aí eu quero
descobrir quais são as dificuldades dos
outros, se isso faz sentido, se elas têm
os tipos delas de diagramas e coisas
do gênero...
Então, tem um monte de técnicas
didáticas por trás disso daqui...
e eu também vou mostrar como eu
transformei os exemplos dos livro de Lean
em exemplos que são mais fáceis de testar
passo a passo.
E aí aqui tem tem um
caso muito mais simples de
de situação em que eu fiz algo parecido
com essa técnica...
eu peguei coisas que eram explicadas de
um jeito complicado, com exemplos grandes...
e desmontei os exemplos em exemplos
muito simples. Então, por exemplo se a
gente quiser aprender o que que é essa
expressão aqui em Lisp eu posso
desmontar ela em várias expressões
pequenininhas, e aí eu posso executar
cada uma dessas expressões - quando eu
executo ela o resultado aparece aqui
embaixo... e aí com isso eu tenho todas as
expressões visíveis de uma vez, e eu
consigo comparar duas expressões, ver
onde é que tão as dificuldades ver onde
aparece algum conceito novo, e coisas assim...
e eu vou mostrar como fazer isso com os
exemplos dos manuais de Lean
de um modo que todos os pedaços
deles ficam visíveis ao mesmo tempo e é
muito fácil checar detalhes.
O meu plano é fazer a oficina em
três aulas só. A primeira aula vai ser
uma aula sobre instalação do Lean
e de outras coisas - a gente vai
usar o Emacs e o eev, mas eu tenho um
método para instalar eles no no Windows...
Então, nessa primeira oficina... ela
demora um pouco, porque alguns passos são
demorados, mas vocês podem fazer outras
coisas ao mesmo tempo... vai ter alguns
momentos em que
a gente vai ver que o computador vai
passar 20 ou 30 minutos instalando
alguma coisa, aí vocês vão fazer outra
coisa, e quando voltarem tá tudo
instalado.
Depois que tiver tudo instalado a gente
vai poder usar esse tipo de hiperlink
daqui pra ir pros manuais principais.
Então: o Lean tem cinco manuais principais.
Por exemplo esse aqui vai pro Functional
Programing in Lean, pra uma seção dele que é a
introdução dele... e ele abre esse manual
no browser. Então, repara: isso aqui é o
título do manual, "Functional Programing...",
aqui tem o índice, e a gente abriu a
introdução...
e aqui tem um outro manual que é
o "Lean Manual",
aqui tem o "Metaprograming in Lean4",
aqui tem o "Type Checking in Lean 4",
que é super técnico mas acho que os
matemáticos vão ter algumas dúvidas que
vão ser respondidas aqui, e aqui tem
o "Theorem Proving in Lean4", que é um dos
mais básicos.
E... a coisa que eu mais gosto no Emacs
é que dá para criar hiperlinks para tudo
e os hiperlinks são esses programinhas
de uma linha em Emacs Lisp. E eu
já dei um montão de oficinas sobre isso,
já melhorei meu material sobre isso
bastante, hoje em dia as pessoas acham
super fácil de aprender.
Então aqui tem um exemplo mais exótico.
É um hiperlink que vai abrir um vídeo numa
determinada posição. Esse vídeo é
espetacular - é um vídeo que foi feito há
poucas semanas atrás...
sobre... bom deixa eu ver o título dele...
eu esqueci o título. Vou fazer isso
aqui... é alguma coisa como
"Visualizing Proofs in Lean using Blender".
Então é um cara que usa Lean para
gerar código que usa o Blender
para fazer animações... é muito
impressionante. E nesse trecho daqui, a
partir do 6:50, ele
mostra como é que ele estendeu a
linguagem do Lean pra ela reconhecer
essas posições do jogo de xadrez aqui em
caracteres Unicode...
E aí o programa
dele faz coisas tipo demonstrar que uma
determinada posição é um mate em cinco
jogadas, e
ele pega a prova que é gerada pelo Lean e
anima ela usando Blender.
Então dá para fazer esse tipo de
coisa. É difícil, né, mas já faz a gente
ter bastante vontade de aprender o Lean...
é o que eu tô tentando fazer agora.
Aqui tem um programa relativamente
básico, que eu fiz... opa, peraí,
caramba... ah tá, faltou isso.
Então, esse programa daqui chama uma
biblioteca que eu fiz... e deixa eu
primeiro mostrar uma coisa...
Ah, peraí, deixa eu só fazer uma
coisinha aqui...
Pronto. Uma coisa muito legal da
interface do Lean é que a gente tem duas
teclas, que eu vou chamar de "go to" e
"go back". Por exemplo, se eu tou com
cursor aqui, em cima desse "LuaTree" aqui,
e aperto a tecla de "go to" ele vai
pro arquivo LuaTree.lean; se eu aperto a tecla
de "go back" ele volta para cá.
Além disso o Lean tem esse tipo de
comando daqui, que gera uma
mensagem aqui na "echo area"...
deixa eu diminuir a fonte... em alguns
casos a mensagem é bem grande e eu
também posso pedir para ele mostrar
todas as mensagens de uma vez.
Então você bato f10 l l - opa, peraí,
não era isso...
se eu bato uma sequência misteriosa
de teclas ele mostra todas as mensagens
de uma vez...
e se eu passeio por várias linhas ele dá
um highlight na mensagem correspondente
à linha em que eu tou.
E essa última...
bom, aqui nesse programa eu defini
uma linguagenzinha que entende só as
operações "-" e "^" e números,
e a linguagem entende elas com a
precedência certa.
Então por exemplo, essa linha daqui
entende essa expressão daqui e
parentesisa ela de uma determinada
forma... essa aqui faz algo parecido mas
ela produz uma coisa num formato que
agora não quero explicar, e essa última
pega essa coisa no formato complicado
transforma ela numa árvore em 2D.
Tá, então eu tou mais ou menos nesse nível...
eu tou aprendendo fazer linguagens muito
simples, e eu tou tentando entender como é
que comandos do link são
definidos usando esse método...
o Lean começa com uma linguagem muito
básica e depois ele define um montão
de extensões escritas em Lean mesmo.
Então, vamos voltar...
eu tava aqui...
isso foi só uma demonstração.
Na primeira aula a gente vai aprender a
interface do Lean, que eu já mostrei
algumas coisas dela, e a gente vai
aprender uma outra coisa bacana que a
gente pode fazer no Emacs: a gente pode
acessar o meu conjunto de anotações
sobre Lean.
Por exemplo, esse link aqui
vai pro bloco sobre "coerção", que tá aqui...
toda essa parte aqui tem links
para documentação, sendo que alguns links
são um pouco mais estranhos... esse link
daqui é um link pro resultado de um grep:
ele vai procurar todas as
ocorrências disso aqui no código fonte
das bibliotecas básicas do Lean
e vai mostrar elas na tela... tá, então
quando eu tava aprendendo sobre coerção
eu usei esse tipo de coisa, e esses links
pro grep vão ser super úteis, e eu vou
mostrar porquê.
Então essas são as minhas
notas sobre coerção, e isso aqui é um
bloquinho, um snippet [de código Lean]...
se eu rodo esse comando
daqui ele abre o meu arquivo temporário
aqui à direita... deixa eu apagar o
conteúdo dele...
e ele bota isso aqui no clipboard do Emacs.
Aí eu posso ir para cá, bater a tecla de
"copy"m e ele copia essas coisas aqui pro
meu arquivo de teste,
e aí eu posso examinar o resultado
de cada coisa dessas.
Esse "#check" aqui ele pega esse termo daqui
e faz algumas expansões nele...
então: o "+" em
princípio não sabe somar um número
natural, que é esse 2, com um inteiro...
mas na verdade esse "+" daqui é
transformado num "'+' heterogêneo",
que pode receber objetos de dois tipos
diferentes, e se for necessário ele
aplica uma coerção em algum deles.
Então quando a gente pede pro #check mostrar
que termo é esse daqui ele mostra o termo
ligeiramente transformado, e mostra que o 2
recebeu um operador de coerção, aqui...
a gente também pode examinar
versões mais detalhadas disso e
descobrir exatamente qual coerção é
usada nesse ponto.
Aí aqui tem um exemplo muito pequeno,
muito menor do que os do manual...
de eu definindo dois tipos diferentes
e definindo uma coerção entre eles...
e aqui tem vários testes, tá, que eu não vou
detalhar agora.
Então, isso é só um exemplo de como as minhas
anotações têm hiperlinks e têm snippets.
Deixa eu voltar...
É isso que a gente vai aprender na primeira aula.
Então, na primeira aula a gente vai aprender
a acessar os manuais principais,
vai aprender o básico da interface,
vai aprender a apontar
pra posições de vídeos,
e a testar código que já existe...
por exemplo, os meus snippets.
Aí... eu acho que isso é o que cabe
na cabeça das pessoas na primeira aula.
Depois vai estar todo mundo cansado, e uma
semana depois a gente faz a aula 2, em
que a gente vai aprender as coisas
básicas da linguagem - que estão
explicadas num dos manuais do Lean, o
"Functional Programming in Lean".
Então a gente vai começar nessa
seção daqui,
"1.1 Evaluating Expressions", e vai
possivelmente até a seção 1.5, e eu vou
traduzir... mostrar para vocês
as minhas traduções de várias dessas
demonstrações [?] daqui, por exemplo isso...
o manual mostra vários trechinhos de
código - deixa encontrar um interessante...
e aí por exemplo eu juntei todos os
trechinho sobre structures num bloco só,
mostrei várias comparações entre várias
sintaxes possíveis, fiz um exemplo muito
mais simples que esse, e tal... então a
gente vai ver como testar isso...
e a gente vai considerar que os manuais
do Lean são a fonte definitiva,
escrita por pessoas que têm muita prática
em didática, só que
elas estão em países em que o ensino é
muito melhor, em que eles têm
turmas enormes em que pessoas estão
aprendendo essas coisas, e tal...
é o contrário da situação em que eu tou,
eu tou totalmente isolado, trabalhando num
campus muito lixo da UFF no interior do
Estado do Rio de Janeiro...
Então, outra coisa que a gente vai ver é
uma coisa que os livros apresentam num
formato bem difícil - eles dão exercícios
bem difíceis...
Eu imagino que todo mundo queira
aprender um pouquinho sobre
como usar Lean como
proof assistant...
Então a gente vai começar com exemplo muito
simples... eu prefiro explicar Curry-Howard
a partir desse exemplo simples daqui, que
só usa implicação e...
Peraí, vamos começar por aqui,
que é a versão em Dedução Natural dele.
então, isso aqui é o "e". Se eu sei que
P∧R é verdade eu sei que P é verdade,
se eu sei que P é verdade e P→Q é
verdade eu sei que Q é verdade...
Então, aqui tem a tradução dessa
demonstração simples em dedução
natural para uma demonstração em
conjuntos... então isso para mim é o
primeiro exemplo interessante de
Curry-Howard...
E aqui à esquerda a gente diz qual é o
elemento do conjunto se eu conheço um
elemento desse conjunto A'×B daqui -
o elemento p - então a primeira projeção,
πp, vai ser um elemento desse conjunto
daqui, A'.
Eu acho que essa notação daqui é
a notação mais familiar para
matemáticos, e a gente vai ver
que o Lean costuma usar uma convenção que
para mim é estranha - é uma convenção
usada pelo pessoal de linguagens
funcionais...
deixa eu pegar uma figura aqui...
aqui é um outro trecho daquele
vídeo que eu falei que é maravilhoso...
Em geral a gente quer aprender o Lean
como provador de teoremas
começando por "táticas".
Muita gente começa rodando o Lean
no browser, no tal do
"Natural Numbers Game" e aí aquilo é um
tutorial que já começa direto por táticas.
O meu primeiro contato com Lean
foi no meio da pandemia quando um cara
chamado Francesco Noseda, que é um professor
da UFRJ... ele deu um curso de Lean online
e eu participei, e no curso dele ele supunha
que as pessoas sabiam um bocado
sobre técnicas de demonstração em
Cálculo de Sequentes e Fitch, e apesar
que eu trabalho com Lógica a minha
formação é muito estranha - eu nunca tive
um curso formal disso...
então, eu sou meio ruim nessas coisas...
eu sou bom em Dedução Natural,
mas eu tenho pouca prática com
técnicas de demonstração, Cálculo de
Sequentes, coisas assim
formalizadas do jeito tradicional para
quem fez um curso de Lógica.
Então, eu ralei muito pra
entender aquilo, e eu fiquei com a sensação
de que faltavam diagramas. Nesse vídeo eu
consigo mostrar para vocês que tipo de
diagrama faltava.
No curso do Francesco e a gente não
conseguia... a gente via esse tipo de coisa
daqui - aqui tem um exemplo de que
hipóteses a gente tem num certo momento
e o que que a gente quer provar...
e nessa figura daqui ele mostra
que quando a gente roda essa tática daqui
o nosso conjunto de hipóteses e
a coisa que a gente quer provar mudam
desse bloquinho de cima para esse
bloquinho de baixo.
Então para mim quando a gente consegue
ver o "antes" e o "depois" na mesma
tela fica muito mais fácil de entender,
e na época do curso de Francesco ele não
mostrou isso, ele não tinha técnicas pra
mostrar isso... e eu passei dias tentando
fazer as figurinhas para conseguir
entender quais eram as táticas principais.
Agora, outro motivo pra gente
não aprender táticas nesse meu curso de
três aulas é que mesmo o Theorem Proving
Lean... deixa eu aumentar a letra de novo...
ele só ensina táticas no capítulo 5 dele.
Então, antes ele ensina a Teoria de
Tipos básica até quantificadores, outros
modos de demonstrar proposições simples...
as táticas só aparecem no capítulo 5.
Então, a gente vai aprender essas
coisas na aula 2, e na aula 2 eu
só vou supor que as pessoas sabem um
pouquinho de Matemática e têm uma noção de
tipos mesmo que seja de linguagens como C,
e já tentaram aprender Haskell e
quebraram a cara...
que elas têm uma noção de coisas
mais básicas, mas empacaram -
possivelmente nos mesmos lugares que eu.
Então, isso é aula 2, e eu
suponho que a aula 2 vai
interessar pra um bocado de gente...
e a aula 2 é desculpa para as
pessoas aprenderem a aula 1, e na aula 1
eu vou apresentar o Emacs e a
biblioteca que eu fiz pro Emacs, que é
essa biblioteca de hiperlinks e outras
coisas, que é o eev.
A aula 3 eu ainda não preparei o
material dela direito, e ela é bem mais
avançada... eu não sei quanta gente
vai se interessar por ela,
porque tem bem pouca gente no Brasil que
se interessa por linguagens funcionais, e
até onde eu sei a maioria das pessoas
que se interessam por linguagens funcionais
está super sem tempo, então eu não sei
quantas pessoas vão fazer
esse meu minicurso...
e na verdade para mim o mínimo é 1 -
se tiver uma pessoa interessada e for uma
pessoa animada, que tem coragem de dizer
"eu não entendi isso aqui" quando eu mostrar
um determinado exemplo, para mim já tá bom...
porque eu consigo testar esse material e
transformar ele num blog post grande, em
alguma coisa publicável, sei lá...
então, digamos que a aula 3 interesse
para bem menos gente, e pode ser que
algumas pessoas assistam a aula 3 mais por
curiosidade mas achem tudo muito avançado...
Basicamente na aula 3 a gente vai ver
as figuras que me salvaram
para entender várias coisas do Lean.
Aqui tem um exemplo dessas figuras...
ih, não, tou na página errada, deixa eu ir
pra outra página... tá aqui.
Por exemplo, isso aqui é um exemplo de
mônadas sem usar a notação "do", que vou
supor que vocês já ouviram falar. Então,
isso aqui é um exemplinho de mônadas com
a notação "do" traduzida pra uma notação
mais básica e com as anotações de tipos.
E pra mim tinha umas coisas que eram
super misteriosas, que é... por exemplo,
como é que a gente descobre que uma
operação dessas, que usa a mônada
de listas retorna uma lista?
E aí a gente tem que fazer
essas type inferences todas pra entender
como é que esse "bind" vai funcionar,
porque tem que ser o bind "da mônada
associada a isso aqui" e aí esse bind
determina qual vai ser o "pure", e o pure
vai fazer com que o resultado seja uma
lista de pares do tipo A×B...
então eu
ficava lendo os capítulos sobre
mônadas dos tutoriais, eles davam um
montão de exemplos de uso, um montão de
analogias... e nada fazia muito sentido pra
mim, e a partir do momento em que eu
consegui ver todos esses detalhes
tudo ficou muito mais claro. Então eu vou
apresentar isso e a gente vai discutir e
eu vou tentar descobrir se esse tipo de
coisa ajuda outras pessoas também, ou não...
Aqui tem um outro exemplo de coisa...
de figura que me ajudou muito.
Deixa eu pegar esse pedacinho dela.
Vamos olhar só pra parte de cima dela.
Isso aqui é uma função que recebe
esses argumentos implícitos aqui, então o
usuário não precisa dar esses argumentos,
o Lean vai inferir esses argumentos
a partir do resto...
Aí tem essa coisa muito misteriosa aqui,
que eu levei meses para entender, e aí
tem essa coisa um pouco mais clara aqui...
aqui a gente tem o produto dos dois
tipos, que a gente pode considerar que é um
produto cartesiano de dois conjuntos, e
um ponto desse produto cartesiano.
Aqui tem uma coisa invisível...
e aí essa função que recebe esses
argumentos vai retornar o resultado
dessa coisa daqui aqui.
Tem uma expressão que vai pegar esse ab,
que é um par, vai separar ele
em lado esquerdo e lado direito,
vai colocar o lado esquerdo
dentro da variável a e vai ignorar o lado
direito... e aí aqui à direita a gente vai
retornar o resultado disso.
E aí como é que a gente faz pra
entender uma coisa dessas?
Eu descobri que o melhor modo de entender
essas coisas é a gente olhar pro parser
do Lean.
Então a gente vai dar uma olhada em como
cada estrutura sintática é definida lá...
algumas têm comentários bem interessantes,
outras têm só referências e outras coisas
[?] que mais ou menos legível
E aí eu fui
descobrindo eh que essa coisa aqui era
uma "typeAscription", essa coisa
misteriosa daqui era um "instance binder",
e a partir do nome [?] que eu descobri isso
eu consegui descobrir quais seções do
manual explicavam essas coisas... e aí aos
pouquinhos tudo foi ficando claro.
Essa figura daqui pode ser dividida
em figuras que detalham...
bom, eu não consegui fazer um
parsing diagram que coubesse numa linha só,
ficava muito grande, então eu dividi
isso em vários...
por exemplo, esse {α β} entre chaves aqui
ele pode ser transformado
nessa árvore daqui, bem maior...
isso aqui é parseado pelo "implicitBinder"...
essa outra estrutura daqui
é parseada pelo instBinder...
e essa última daqui é parseada
desse jeito daqui...
e o "let" é parseado por essas duas
árvores daqui de baixo.
Tá, então a gente vai entender isso aqui,
que é um outro tipo de diagrama
que me salvou...
E... ai caramba... aqui.
E basicamente é isso.
Talvez tenha um outro tipo de
diagrama, que é pra gente entender o que
que é um "Pratt parser" e como é que o
Lean entende precedência, macros e outras
coisas... mas eu ainda não tenho exemplos
muito bons dele... então é basicamente isso.
Tem mais uma seção aqui... peraí.
Ah, não, era só isso. Eu já expliquei qual
era minha motivação, meu público alvo, a
história da didática e tudo mais, e só
falta falar uma coisa.
É o seguinte eu já
disse que eu tou trabalhando num campus
da UFF que é muito pequeno. Eu já tinha
uma noção de que esse campus era um lixo,
até um tempo atrás... mas
nos últimos do anos eu consegui
descobrir que ele é um lixo, assim, 10
vezes maior do que eu pensava...
não dá para interagir com os meus colegas de lá
nem mesmo para para discutir os cursos
que eu tou dando e técnicas de didática...
e eu oferecia umas oficinas de Software
Livre pros... basicamente pros alunos,
e eles não iam nunca, e eu não entendia
porquê...
e aí durante a greve eu ofereci
essas oficinas divulgando elas pro
pessoal de todos os cursos e eu vi que
as pessoas de Produção Cultural e
Psicologia iam nas oficinas, ficavam
super animadas, faziam milhões
de perguntas... mas os alunos da
Computação e da Engenharia - eles não iam
de jeito nenhum.
Aí eu fui entendendo aos poucos - até
porque eu conversei com umas pessoas que
estudaram em Niterói - que eles têm uma
mentalidade na qual é inconcebível você
estudar junto com os colegas, você tirar
dúvida dos colegas, você ir na oficina
dos colegas... então eles não tem uma
mentalidade de "estamos na universidade
pública, vamos fazer tudo que aparecer,
vamos aprender tudo que der, e vamos
compartilhar o conhecimento"...
É uma coisa muito estranha. Eles
talvez tenham pego um pouco da mentalidade
do pessoal da Engenharia de Produção, não
sei direito... mas de qualquer forma é
péssimo.
E aí eu tô querendo dar essa oficina
pra fazer contato com pessoas
de outras universidades, descobrir que
que elas estão fazendo, descobrir como é que
eu posso participar dos projetos delas,
grudar nelas de alguma forma fazendo
coisas interessantes junto com elas online...
Deixa eu só mostrar uma coisinha que faltou.
Eu mostrei como é que esses
links daqui vão para seções dos manuais...
por exemplo, esse aqui abre
a versão em HTML do
"Functional Programing in Lean"...
e todos esses manuais tem exceto um têm
fonte um formato super fácil de acessar,
e a gente consegue extrair os
bloquinhos de código dessa fonte.
Então, por exemplo, nesse manual
daqui, do "Metaprograming", tem uma seção...
repara que esse link daqui veio pra uma subseção
dessa página, a subseção se chama "Building
a DSL and a syntax for it"...
é um exemplo mais ou menos básico
de como criar uma linguagenzinha nova...
e eu também posso ir pro código fonte
disso aqui, que gerou esse HTML...
Então, se eu rodo esse hiperlink daqui
ele abre o código fonte disso...
repara, esse título aparece
desse jeito aqui, e esse bloquinho de
código aparece desse jeito... isso aqui é
um arquivo em Lean, o arquivo parseou
essas coisas daqui
interpretou esse bloquinho daqui como
Lean, coloriu tudo do jeito certo, e,
por exemplo... talvez se eu usar a tecla
de "go to" aqui talvez ele vá
pra definição do "inductive"... bom,
talvez, mas eu não tenho certeza...
Tudo funciona exatamente como
naquele outro demo que eu mostrei - cada
"#check" desses mostra um output aqui
embaixo, e se eu bater f10 l l...
opa, não, seu eu bater essa
sequência misteriosa de teclas daqui
ele mostra todas as mensagens de uma vez.
Então: a gente vai ver como acessar esse...
o código fonte, e extrair o código fonte
e criar arquivos menores com isso, em que
a gente possa fazer nossos experimentos...
modificar coisas, simplificar coisas
acrescentar coisas, etc...
Então isso é uma coisa que a gente
vai ver superficialmente na primeira
aula e depois a gente vai usar
bastante.
E... é isso. O vídeo era isso aí.
Qualquer coisa acessem essas
páginas pra mais informações e entrem
em contato comigo... e se vocês tiverem
algum interesse no curso por
favor peguem os meus contatos e mandem
ou e-mail ou mensagem por WhatsApp ou
por Telegram. É isso por enquanto!