2024.2 Programação Funcional

Pontos de participação

Homework (HW)

Leia bem o FAQ sobre hw. Note também que:

• Homeworks são atribuidos também durante as aulas e no Zulip.
• Homeworks marcados assim são auxiliares; tente apenas se tu tem resolvido uma parte satisfatória dos outros.

2024-10-07 (hw01)

1. Defina (sem consulta) a adição, a multiplicação, e a exponenciação (nos Nats).
2. Calcule os:
   1. 2 + 3
   2. 3 + 2
   3. um dos: 4 · 1; 1 · 4
3. Defina uma função double que retorna o dobro da sua entrada.
4. Calcule os:
   1. double (double (S O))
   2. double ((S O) + (S (S O)))
5. Demonstre uma das: (·)-idL, (·)-idR
6. Demonstre uma das: (^)-idL, (^)-idR
7. Defina a função pred : Nat → Nat de “predecessor”, onde consideramos que o predecessor de zero é o próprio zero mesmo: AVISO: a maioria das vezes que um aluno de 2022.1 e de 2022.2 usou a pred em outras definições, estava errando
8. Defina as funções:
   1. fact : Nat → Nat
   2. fib  : Nat → Nat
   3. min  : Nat × Nat → Nat
   4. max  : Nat × Nat → Nat
   5. div  : Nat × Nat → Nat × Nat
   6. quot : Nat × Nat → Nat
   7. rem  : Nat × Nat → Nat
   8. gcd  : Nat × Nat → Nat
   9. lcm  : Nat × Nat → Nat
9. Instale Haskell, Agda, e Lean no teu sistema (veja o FAQ).
10. Implemente em Haskell todas as tuas definições dos exercícios acima.
11. Clone o meu repositório mencionado no FAQ do Git.
12. Crie o teu repositório mencionado no FAQ do Git.
13. fmcbook §«Um toque de lambda»
14. fmcbook Cap. 4: «Recursão, Indução»: §«Definindo funções recursivamente»
15. [Hutton] Cap. 3

2024-10-11 (hw02)

1. Cap «Recursão; Indução»: até a §«Demonstrando propriedades de naturais sem indução»
2. Cap «Recursão; Indução»: §«Abusando um tipo para implementar outro»; §«Os Bools»; §«O ListNat»

2024-10-18 (hw03)

1. Ache no hw/ do meu repo, copie para o teu, e resolva os:
   • ExNat
   • ExBool
   • ExList
   • ExCurry
   • ExHyper

2024-10-26 (hw04)

1. fmcbook: Cap. Funções: §«Composição»
2. fmcbook: Cap. Funções: §«Definições estilo point-free»
3. Desafio: implementar um data type para os inteiros

2024-11-01 (hw05)

1. Demonstre que: bnot é uma involução: bnot . bnot = id
2. Complete as igualdades e demonstre:

   take n xs ++ drop n xs  =
   take m . drop n  =
   take m . take n  =
   drop m . drop n  =
   map g . map f  =
   sum . map double  =
   sum . map sum  =
   sum . sort  =
   map f . reverse  =
   concat . map concat  =
   filter p . map f  =
   

3. Quais das seguintes são válidas e quais não?

   map f . take n  =?=  take n . map f
   map f . reverse  =?=  reverse .map f
   map f . sort  =?=  sort . map f
   filter (p . g)  =?=  map ginvl . filter p . map g
   reverse . concat  =?=  concat . reverse . map reverse
   filter p . concat  =?=  concat . map (filter p)
   

   (suponha aqui que a ginvl é um inverso esquerdo da g, ou seja: glinv . g = id
4. Complete as igualdades e investigue:

   length . reverse  = 
   reverse . reverse  = 
   (xs ++ ys) ++ zs  = 
   map id  =  
   map (f . g)  =  
   length (xs ++ ys)  = 
   sum (xs ++ ys)  = 
   product (xs ++ ys)  = 
   concat (xss ++ yss)  = 
   filter p (xs ++ ys)  = 
   map f (xs ++ ys)  = 
   

2024-11-22 (hw06)

1. Aproveite Records nos teus programas até agora e brinque com a sintaxe
2. Dadas funções f : α → γ e g : β → δ mostra como definir ? : α × β → γ × δ (i) manualmente; (ii) aproveitando algo sobre um (×) que aparece aí (qual dos dois, e qual é o tal algo?)
3. Dadas funções f : α → γ e g : β → δ mostra como definir ? : α + β ← γ + δ (i) manualmente; (ii) aproveitando algo sobre um (+) que aparece aí (qual dos dois, e qual é o tal algo?)
4. Desenhe, adivinhe, e demonstre:
   1. ⟨outl, outr⟩ = ?
   2. ⟨f,g⟩ = ⟨k,h⟩ ⇒ ?
   3. ⟨f∘h,g∘h⟩ = ?
   4. (f×h)∘⟨g,k⟩ = ?
   5. $1_A \times 1_B = {?}$
   6. (f×h)∘(g×k) = ?

Histórico

Quadro das aulas

• Quadro: lec11 – lec22
  Last update: 2024-12-18

2024-09-25: (1) Meta & Intro

• Linguagens de programação

2024-09-27: (2) Tipos

• (→) e (×)

2024-10-02: (3) Tipos

• de buracos para (↦) para λ
• currificação
• duas definições de double : Int → Int
• números vs numerais
• 4 maneiras diferentes de definir o tipo Nat

2024-10-04: (4) Nat

• o que «aridade» pode significar: currificamente ou descurrificamente
• o modelo computacional de programação funcional
• uma definição de soma: _+_ : ℕ → ℕ → ℕ
• 2 + 3 = 5
• 2 + 3 ≢ 3 + 2
• estratégias de evaluação: lazy vs strict
• infinity : Nat e five infinity

2024-10-09: (5) fun with GHCi

• (apanhando num computador-não-meu, usando um teclado-não-meu)
• como definir a (·)
• Brincando com ghci
• Ints, Bools, Listas, Strings built-in da Haskell (no Prelude)
• modules: importar, definir
• list comprehension
• trabalhando com «valores infinitos»
• let-in expressions
• if-then-else expressions
• sombreamento de variáveis
• inconsistência de Haskell
• bottom : α
• error : String → α
• mensagens de erro no GHCi e como interpretá-los

2024-10-11: (6) more types

• raise awareness: stop abusing types
• abusing Nats
• novo tipo: Bool
• novo tipo: Weekday
• novo tipo: ListNat
• tipos (propriamente) recursivos
• duas interpretações de um construtor Nat → ListNat: colchetor, looper
• length

2024-10-16: (7) polimorfismo, type classes, desconstrutores

• desconstrutores de construtores
• head, tail, pred
• polimorfismo: a (família de funçoẽs) id : α → α
• especificação vs implementação
• typeclasses
• a typeclass Num
• a typeclass Show
• a typeclass Eq
• implementação padrão em typeclass

2024-10-18: (8) blah-expressions, list toolkit

• match-with / case-of expressions
• let-in expressions
• patterns nos let-in
• uso de desconstrutores como sinal de algum possível problema
• if-then-else expressions
• guards
• o tipo Char e umas maneiras de defini-lo
• o 'a' * 2 faz sentido em C
• abstraindo a parte comum de definições
• a map
• duas maneiras de interpretar o tipo da map
• a filter
• duas maneiras de interretar o tipo da filter
• de umas definições de 2 linhas para algo melhor: 1 linha só
• de definiçoes de 1 linha só para algo melhor: 1 linha curta
• algo ainda melhor: 0 linhas!

2024-10-23: (9) map, filter, fold

• como implementar notações de list comprehension
• sum, prod, and, or
• ($)
• notação de section: (^ 2), (2 ^), etc.
• fold associando à esquerda e à direita

2024-10-25: (10) composição

• composição de funções
• quebrando o problema de definir ? : α → ω para iluminar a situação
• point-free / pointless / tacit programming
• a Δ : α → α
• o que significa «a óbvia função de tal tipo»

2024-10-30: Prova 1

2024-11-01: (11) Indução

• at-patterns
• ArEx
• tentativa de demonstração de (+)-ass sem indução
• o princípio da indução
• construtores respeitando propriedades

2024-11-06: (12) Caçando teoremas

• descubrindo teoremas
• demonstrações por indução
• comandos e o estado duma demonstração: Dados/Alvo
• Basta _.
• recursão e indução
• Θ. (+)-ass
• igualdade entre funções
• Θ. length ∘ map f = length
• Θ. length = sum ∘ map (const 1)

2024-11-08: (13) Unit, Empty, Maybe

• Unit (𝟘)
• Empty (𝟙)
• Entendendo tipos através de maneiras de chegar neles e de sair deles
• Maybe α

2024-11-13: (14) Either, Functors

• Either α β
• Functors
• As leis de functor

2024-11-22: (15) Records, (Co)products, Diagrams

• Record types
• Diagramas comutativos
• Product types
• Coproducts (sums)

2024-11-27: (16) Indução, diagramas comutativos

• Θ. sum (xs ⧺ ys) = sum xs + sum ys
• mais produtos
• mais funções de graça: cross, plus
• mais diagramas comutativos

2024-11-29: (17) IO

• IO a
• pure, do-notation
• putChar, getChar
• putStr

2024-12-04: (18) FAM: Applicative

• Applicative typeclass
• Applicative instances for IO, Maybe, List

2024-12-06: (19) SMG, valores ambiguos e temporais

• Semigrupo
• cópias isómorfas de tipos: newtype
• interpretações computacionais
• valores ambígulos
• valores temporais
• produto cartesiano de listas

2024-12-11: (20) thunks, pointfree proofs, laws

• do laws
• applicative laws
• thunks, :sprint, seq
• demonstrações sem pontos

2024-12-13: (21) efficiency by induction, sorting

• eficiência “por indução”
• uma reverse de complexidade O(n)
• merge sort
• quick sort
• insertion sort

2024-12-18: (22) fold, applicatives and functors, isomorphic copies

• folds para Listas: foldr, foldl
• folds para Nats
• Temporal α vs Ambiguous α como applicatives e seus fmaps
• cópias isomórficas de tipos: type vs data vs newtype

2024-12-20: (Cancelada)

Futuro (fluido)