parametrisyyden

Parametrisyyden är ett begrepp inom programmeringsteori som beskriver hur polymorfa funktioner uppträder uniformt oavsett vilka typer de tillämpas på. En funktion av typen forall a. T a får inte använda information om typen a utan den måste bete sig på samma sätt för alla typer.

Historik och teori: Begreppet introducerades av John C. Reynolds i samband med System F och kallas ofta Reynolds abstraktionssats. Den beskriver en relationell tolkning av typer och termer, där varje polymorf term översätts till en familj av funktioner som bevarar relationer mellan relaterade typer. Denna modell möjliggör en princip om "uniformt beteende" för polymorfa konstruktioner.

Konsekvenser: Parametrisyyden leder till fria teorem, eller Theorems for Free, som kan härledas från typen själv. Exempelvis måste en funktion av typen forall a. a -> a i de flesta sammanhang uppträda som identiteten (upp till icke-termination eller konstruktioner som gör att det inte går att använda typen för mer information). Denna uniformitet gör det möjligt att resonera om generiska funktioner och deras beteende utan att känna till den specifika typen.

Användning och begränsningar: Parametrisyyden används som teoretisk modell i språk som System F och i analyser av funktionella språk som Haskell. I språk där sid effekter eller I/O förekommer är parametrisyyden mer begränsad och gäller ofta endast under särskilda antaganden eller i modeller som tar hänsyn till effekter.

Se även: Reynolds abstraktionssats; Wadlers Theorems for Free.