From: Matthijs Kooijman Date: Tue, 1 Dec 2009 10:12:27 +0000 (+0100) Subject: Add note about β-reduction for type variables. X-Git-Tag: final-thesis~131 X-Git-Url: https://git.stderr.nl/gitweb?a=commitdiff_plain;h=0cd3f69b1d8fb7e18a7e0b2bccd86a96d7fd009b;p=matthijs%2Fmaster-project%2Freport.git Add note about β-reduction for type variables. --- diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 55e0057..cdd57bb 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -812,6 +812,11 @@ sure that most lambda abstractions will eventually be reducable by β-reduction. + Note that β-reduction also works on type lambda abstractions and type + applications as well. This means the substitution below also works on + type variables, in the case that the binder is a type variable and teh + expression applied to is a type. + \starttrans (λx.E) M ----------------- @@ -829,6 +834,17 @@ \transexample{beta}{β-reduction}{from}{to} + \startbuffer[from] + (λt.λa::t. a) @Int + \stopbuffer + + \startbuffer[to] + (λa::Int. a) + \stopbuffer + + \transexample{beta-type}{β-reduction for type abstractions}{from}{to} + + \subsubsection{Empty let removal} This transformation is simple: It removes recursive lets that have no bindings (which usually occurs when unused let binding removal removes the last