Let polymorfizmus a Systém F

Pokúste sa nájsť najvšeobecnejší typ termu: $$let\ id=\lambda x.x\ in\ id\ id$$

Pokúste sa nájsť najvšeobecnejší typ termu: $$let\ id=\lambda x.x\ in\ if\ id\ true\ then\ id\ 5\ else\ id\ 8$$

Pokúste sa nájsť najvšeobecnejší typ termu: $$let\ ff=\lambda f.\lambda x.f\ x\ in\ add\ ff\ ff $$ v typovom kontexte: $$\Gamma=\{add:Nat \to Nat \to Nat\}$$

Definujte polymorfnú identickú funkciu a jej typ: $$id=... : T$$

• Overte či je správne typovaná.
• Aplikujte ju na vhodné parametre.

Definujte typ $Bool$ ako polymorfný typ a následne definujte:

• hodnoty typu,
• operácie negácie a konjunkcie.

Majme term: $$neg\ true$$

• Overte či je správne typovaný.
• Vyhodnoťte ho.

Majme term: $$and\ true\ false$$

• Overte či je správne typovaný.
• Vyhodnoťte ho.

Definujte typ $Nat$ ako polymorfný typ a následne definujte:

• hodnoty typu,
• operácie nasledovníka a sčítania.

Majme term: $$succ\ 2$$

• Overte či je správne typovaný.
• Vyhodnoťte ho.

Majme term: $$plus\ 1\ 0$$

• Overte či je správne typovaný.
• Vyhodnoťte ho.