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
- onderstaande kernbegrippen (zie 'Instructie') verklaren;
- varianten van het begrip 'polymorfie' aanduiden en verklaren;
- uitleggen hoe het typeringsalgoritme in eerste-orde getypeerde lambda-calculus
werkt;
- gegeven types unificeren;
- van een gegeven term het principal type bepalen;
- het verband tussen typeafleiding en typeverificatie aangeven;
- duidelijk maken hoe typeafleiding in implementaties van (functionele) programmeertalen
in zijn werk gaat.
Instructie
- Lees p. 7 en p. 13-18 in het dictaat over typetheorie en bekijk deze extra pagina over "principal types". Kernbegrippen:
- polymorfie, tweede-orde lambda-calculus,
- unifier, most general
unifier, unificatie,
- principal type,
- typeschema, instantiatie,
- syntaxgestuurd
- typeafleiding (type inference), typeverificatie
(type checking).
- Voer de opdrachten in de bijlage uit.
Product
- Mgu's van de gegeven typeparen.
- Principal types van de gegeven termen.
- Term(en) als oplossing van de gegeven typespecificaties.
Reflectie
- Houdt u bij het unificeren rekening met de syntactische (haakjes)conventies?
- Gebruikt u de typevergelijkingen om aan te tonen dat een term niet typeerbaar
is, dan wel om het principal type te verantwoorden?