From: chris Date: Mon, 9 Mar 2015 18:43:10 +0000 (-0400) Subject: (no commit message) X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=34942572995dfda43937082cbb6d7addc323e8e6 --- diff --git a/topics/week5_system_F.mdwn b/topics/week5_system_F.mdwn index 36c071cd..c20b61c5 100644 --- a/topics/week5_system_F.mdwn +++ b/topics/week5_system_F.mdwn @@ -122,7 +122,7 @@ Exercise: convince yourself that `zero` has type `N`. The key to the extra expressive power provided by System F is evident in the typing imposed by the definition of `pred`. The variable `n` -is typed as a Church number, i.e., as `N ≡ ∀α.(α->α)->α->α`. +is typed as a Church number, i.e., as N ≡ ∀α.(α->α)->α->α. The type application `n [Pair]` instantiates `n` in a way that allows it to manipulate ordered pairs: `n [Pair]: (Pair->Pair)->Pair->Pair`. In other words, the instantiation turns a Church number into a certain