Leertaak 9

Typeafleiding en typeverificatie

Achtergrond

In de eerste-orde getypeerde lambda-calculus is het beslisbaar of een gegeven term typeerbaar is. In het positieve geval kunnen we een type berekenen op een systematische manier, via het oplossen van typevergelijkingen.

In programmeertalen komen vaak polymorfe constructies voor: eenzelfde functie kan op verschillende manieren (d.w.z. met een verschillend type) gebruikt worden in hetzelfde programma. Polymorfe typering is in het algemeen onbeslisbaar, maar we kunnen een beslisbare variant onderscheiden die overeenkomt met de manier waarop polymorfie in programmeertalen voorkomt.

Leerdoel

Na het voltooien van deze taak kunt u

Instructie

  1. Lees p. 7 en p. 13-18 in het dictaat over typetheorie en bekijk deze extra pagina over "principal types". Kernbegrippen:
  2. Voer de opdrachten in de bijlage uit.

Product

Reflectie