cp2425faqs

$ % 18-Abr-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{\\&#1& \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}} %-------- \def\Varid#1{\mathbin{#1}} \def\ensuremath#1{#1} \def\Conid#1{\mathbin{#1}} $

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 - Como é que se verifica analiticamente a igualdade $(f + h) \comp \alpha = \alpha \comp (f + g \times h)$? (Tendo em conta que a expressão é a propriedade grátis de $\alpha$.)

R: Deverá desenhar o diagrama dessa propriedade para obter o tipo (polimórfico) de $\alpha$. A partir desse tipo irá inferir a definição de $\alpha$. Com essa definição já pode verificar analiticamente a lei.

Q3 - Nas perguntas do teste que forem para mostrar os passos usando várias fórmulas, podemos utilizar várias fórmulas de uma vez (ou seja fazer mais do que um passo de cada vez) ou temos de mostrar passo a passo como é que as equações vão ficando?

R: Podem aplicar mais do que uma lei no mesmo passo, desde que as identifiquem na justificação.

Q4 - Encontro-me com dúvidas no exercício 5 da ficha 5. Podem disponibilizar uma resolução?

R: Sugere-se que, em $ap \comp (\trans f \times id) = f$, se substitua $f$ por $uncurry\ g$. Como $\trans f$ é abreviatura de $curry\ f$, obter-se-á \begin{eqnarray} ap \comp (curry\ (uncurry\ g) \times id) = uncurry\ g \end{eqnarray} isto é \begin{eqnarray} ap \comp (g \times id) = uncurry\ g \end{eqnarray} pois $curry (uncurry\ g) = g$. Agora é só introduzir variáveis acima e simplificar.

Q5 - Não consegui resolver o exercício 6 da ficha 6 e preciso de uma orientação. Por onde começar?

R: A primeira coisa que deve fazer é olhar para o diagrama geral do catamorfismo,

e instanciar $g := \cata{\alt{\kons{id}}{(f\comp)}}$. Ter-se-á

\begin{eqnarray} \start \kons{id} : 1 \to A \more (f\comp) : A \to A \end{eqnarray}

A questão surge agora é: qual é o tipo $A$ neste caso? Em geral, $id : B \to B$, isto é, $id : B^B$. Logo $A = B ^ B$. Sendo assim, de imediato se tem $(f\comp): B^B \to B ^ B$. A questão que fica então para pensarem é: e qual é o tipo de $f$? Com isso, ficará totalmente caracterizado o tipo de $rep$...

Q6 - No teste a primeira pergunta (tipo mais geral de $\alpha = \conj {\i1} {\p1}$, etc etc) correu-me muito mal e tenho dificuldade em fazer inferência de tipos polimórficos. Há alguma sugestão sobre estudar este assunto?

R: Sugere-se o estudo de 'A Quick Introduction to Polymorphic Type Checking' que está na Bibliografia.

CP/2425 - FAQs¶