Church encoding は知ってるけど、 Scott encoding なんてのもあるのね。 Church encoding は μF ≅ ∀X. (FX→X)→X などと型レベルで理解してたけど、 Scott encoding は型付け出来ないそうで、 どういう風になっているのかピンとこないなぁ。