Leertaak 7
Getypeerde lambda-calculus
Achtergrond
Met typering in programmeertalen kunnen we voorkomen dat een programmeur bewerkingen toepast op argumenten waarvoor de betreffende operatie niet bedoeld is. Uit de typespecificatie van de optelling kan bijvoorbeeld afgeleid worden dat er geen string bij een integer kan worden opgeteld. Naast deze controle op 'locale consistentie' hebben typeringssystemen soms nog andere toepassingen, bijvoorbeeld het detecteren van optimalisatiemogelijkheden.
We kunnen op verschillende manieren typering toevoegen aan de lambda-calculus: door types toe te wijzen aan ongetypeerde termen, of door type-informatie op te nemen in de syntax van termen.
De uitspraak "term M heeft type A" kunnen we in computationele zin opvatten als "M is een programma en A is zijn type", maar ook in logische zin, namelijk als "M is een bewijs van propositie A".
Leerdoel
Na het voltooien van deze taak kunt u
Instructie
Product
Reflectie