Skrivmiljö

I typteorin representerar en skrivmiljö (eller skrivkontext ) kopplingen mellan variabelnamn och datatyper .

Mer formellt är en miljö $\Gamma$ en uppsättning eller ordnad lista med par $\langle x,\tau \rangle$ , vanligtvis skriven som $x:\tau$ , där $x$ är en variabel och $\tau$ dess typ.

Domen _

$\Gamma \vdash e:\tau$

läses som " $e$ har typen $\tau$ i sammanhanget $\Gamma$ ".

I statiskt typade programmeringsspråk används och underhålls dessa miljöer genom att skriva regler för att typkontrollera ett givet program eller uttryck.

Se även

• Typ system