From 34942572995dfda43937082cbb6d7addc323e8e6 Mon Sep 17 00:00:00 2001 From: chris Date: Mon, 9 Mar 2015 14:43:10 -0400 Subject: [PATCH] --- topics/week5_system_F.mdwn | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.11.0