$ % 17-Mar-2024 \def\start{&&} \def\more{\\&&} \def\sse#1#2{{#1}\subseteq{#2}} \def\iso{\cong} \newenvironment{lcbr}{\left\{\begin{array}{l}}{\end{array}\right.} \def\ana#1{(\hskip -1ex[#1]\hskip -1ex )} \def\cata#1{(\hskip -1.1pt[\hskip 0.1pt #1 \hskip 0.1pt]\hskip -1.1pt)} \def\Seq#1{{#1}^{\star}} \def\fB{\fun B} \def\mcond#1#2#3{#1 \rightarrow #2\;,\;#3} \newenvironment{lcbr}{\left\{\begin{array}{l}}{\end{array}\right.} \def\bang{{!}} \def\Nat{\mathbb{N}} \def\N{\Nat} \def\atmost{\subseteq} \def\alt#1#2{[#1,#2]} \def\comp{\mathbin\cdot} \def\conj#1#2{\mathopen{\langle} #1, #2\mathclose{\rangle}} \def\conv#1{#1^\circ} \def\crflx#1{\Phi_{#1}} \def\dom#1{\delta {#1}} \def\from{\leftarrow} \def\fun#1{\mathsf{#1}} \def\i#1{\mathit{i}_{#1}} \def\inT{\mathsf{in}} \def\outT{\mathsf{out}} \def\implied{\Leftarrow} \def\implies{\Rightarrow} \def\just#1#2{\\& \mathopen{\{}~\mbox{#2}~\mathclose{\}}\\&&} \def\ker#1{\mathbf{ker}\ {#1}} \def\img#1{\mathbf{img}\ {#1}} \def\kons#1{\underline{#1}} \def\larrow#1#2#3{#3\ \xleftarrow{#2}\ #1} \def\ldiv{\mathbin{/}} \def\p#1{\pi_{#1}} \def\plus{\mathbin{\dagger}} \def\rarrow#1#2#3{#1\ \xrightarrow{#2}\ #3} \def\rcb#1#2#3#4{\mathopen{\langle}#1 #2 : #3 : #4\mathclose{\rangle}} \def\rdiv{\mathbin{\setminus}} \def\sep{\rule{15em}{0.3pt}} \def\shrunkby{\mathbin{\upharpoonright}} \def\syd#1#2{\frac{#1}{#2}} \def\to{\rightarrow} \def\trans#1{\overline{#1}} \def\scata#1{⦅\, #1 \,⦆} \def\sep{\rule{15em}{0.3pt}} $
Q1 - Vamos poder levar o formulário para o teste?
R: Como se disse nas aulas e está nos avisos, os alunos poderão levar para as provas de avaliação, se assim o entenderem, o formulário da disciplina em papel, desde que dele não conste qualquer anotação manuscrita ou outra.
Q2 - Na questão 2 deste exame, $h: A \times B \to B \times A$ e a sua propriedade natural é semelhante à do $swap$, correto?
R: O tipo de $h$ é o tipo de entrada de $f$. Se definir
f h = cond (p1.p2) swap he pedir ao GHCi o tipo de $f$ (:t f), não é isso que obtém. Ora veja melhor como inferiu esse tipo.
Q3 - Não consigo ver o que fazer para iniciar a questão 4 deste exame.
R: Experimente começar por usar fusão-exp no único sítio onde isso é possível e prosseguir sem usar as leis que se referem.
Q4 - Tenho bastante dificuldade em fazer inferência dos tipos mais gerais de expressões funcionais polimórficas como as que temos visto nas aulas. Há algum texto que sugiram para eu perceber melhor o método, e.g. um road-map de como o fazermos?
R: Sugiro que leia esta nota pedagógica. Nele o métodos de ir fazendo a inferência por partes unificando os tipos é dado com detalhe, incluindo exemplos.
Q5 - Na questão 1 do teste de 1 de Junho de 2022 não há uma troca entre $\mathsf{assocr}$ e $\mathsf{assocl}$? Ou seja, onde está $\mathsf{assocr}$ seria $\mathsf{assocl}$ e vice e versa? Cf. Cp.hs.
R: Sim, estão trocados os nomes! Obrigado por identificar a gralha, que entretanto já foi corrigida.
Q6 - Como é que, na questão 4 da ficha 2, obtenho $\mathsf{xr}$ a partir da propriedade $\mathsf{xr} \comp \conj{\conj{{f}}{{g}}}{{h}}\mathrel{=}\conj{\conj{{f}}{{g}}}{{h}}$ ?
R: Como se mostra no início deste vídeo, a melhor solução é resolver a equação auxiliar $\conj{\conj{{f}}{{g}}}{{h}} = id$, e substituir as soluções no lado direito $\conj{\conj{{f}}{{h}}}{{g}}$, pois $\mathsf{xr}$ fica sozinho no lado esquerdo. A igualdade $\conj{\conj{{f}}{{g}}}{{h}} = id$ é facilmente resolvida aplicando a propriedade universal-$\times$.
Q7 - Seria possível explicar a passagem do tipo de dados no passo 5 ? Este exercício é referente ao teste 13 Junho de 2020.
R: Nesse passo a parte relevante é o isomorfismo $Bool \iso 1 + 1$. Como $Bool = \{True,False\}$, tem-se que $\larrow{1+1}{\inT}{Bool}$ é $\inT = \alt{\kons{True}}{\kons{False}}$. A sua inversa $\outT$ pode ser obtida resolvendo $\outT \comp \inT = id$ como se fez nas aulas. Sendo assim, $\fbox 5 = id \times out$.