回答編集履歴
4
単純な例の誤解しやすい点の改善
answer
CHANGED
@@ -2,14 +2,14 @@
|
|
2
2
|
再帰的な型を扱うためには明示的に型を作成してやる必要があります。
|
3
3
|
|
4
4
|
より単純な例でまずは説明します。
|
5
|
-
たとえば
|
5
|
+
たとえばf x = x xのような場合xの型はどうなるでしょうか。
|
6
6
|
xの型がaだったとするとxは引数xを取り何かを返す関数でもあるのでxの型はa -> bとなります。
|
7
7
|
すると今度はxの型は(a -> b) -> cとなります。
|
8
8
|
さらにxの型は((a -> b) -> c) -> dとなり...のようにいつまでも型が決まりません。
|
9
9
|
このような場合、代数的データ型で明示的に再帰的な型を作ってやる必要があります。
|
10
10
|
newtype R a = R { unR :: R a -> a }のようにします。
|
11
11
|
すると、型R aは(R a -> a)を保持する再帰的な型となります。
|
12
|
-
このようにすると
|
12
|
+
このようにするとf x = unR x xのように表現することができます。
|
13
13
|
|
14
14
|
型Rの場合、再帰的になっているのは引数の部分('->'の左側)だけです。
|
15
15
|
Church数の場合、返り値('->'の右側)の部分も再帰的にする必要があるので、以下のような型となります。
|
3
型変数の削除の変更漏れの修正
answer
CHANGED
@@ -18,7 +18,7 @@
|
|
18
18
|
実際にしていることはCとunCによって関数をデータ型Cに入れたり出したりしているということになります。
|
19
19
|
|
20
20
|
静的な型付けで再帰的な型を定義するこのやりかたは僕には非常に美しいように感じます。
|
21
|
-
またA
|
21
|
+
またA CやZはChurch数を数値に変換するために用意したもので、本質的な部分ではありません。
|
22
22
|
|
23
23
|
```Haskell
|
24
24
|
data C = C { unC :: C -> C } | A C | Z
|
2
型変数は不要であることに気づく。
answer
CHANGED
@@ -21,31 +21,31 @@
|
|
21
21
|
またA (C a)やZはChurch数を数値に変換するために用意したもので、本質的な部分ではありません。
|
22
22
|
|
23
23
|
```Haskell
|
24
|
-
data C
|
24
|
+
data C = C { unC :: C -> C } | A C | Z
|
25
25
|
|
26
|
-
(.$.) :: C
|
26
|
+
(.$.) :: C -> C -> C
|
27
27
|
(.$.) = unC
|
28
28
|
|
29
|
-
toInt :: C
|
29
|
+
toInt :: C -> Int
|
30
30
|
toInt Z = 0
|
31
31
|
toInt (A c) = 1 + toInt c
|
32
32
|
toInt n = toInt $ n .$. C A .$. Z
|
33
33
|
|
34
|
-
toChurch :: Int -> C
|
34
|
+
toChurch :: Int -> C
|
35
35
|
toChurch 0 = zero
|
36
36
|
toChurch n = s .$. toChurch (n - 1)
|
37
37
|
|
38
|
-
false, true, _if :: C
|
38
|
+
false, true, _if :: C
|
39
39
|
false = C (\x -> C (\y -> y))
|
40
40
|
true = C (\x -> C (\y -> x))
|
41
41
|
_if = C (\b -> C (\x -> C (\y -> b .$. x .$. y)))
|
42
42
|
|
43
|
-
zero, one, s :: C
|
43
|
+
zero, one, s :: C
|
44
44
|
zero = C (\f -> C (\x -> x))
|
45
45
|
one = C (\f -> C (\x -> f .$. x))
|
46
46
|
s = C (\n -> C (\f -> C (\x -> f .$. (n .$. f .$. x))))
|
47
47
|
|
48
|
-
isZero :: C
|
48
|
+
isZero :: C
|
49
49
|
isZero = C (\n -> n .$. (C (\x -> false)) .$. true)
|
50
50
|
|
51
51
|
add, mult, pre :: C a
|
@@ -54,7 +54,7 @@
|
|
54
54
|
pre = C (\n -> C (\f -> C (\x ->
|
55
55
|
(n .$. (C (\g -> C (\h -> h .$. (g .$. f)))) .$. (C (\u -> x))) .$. (C (\u -> u)))))
|
56
56
|
|
57
|
-
hoge :: C
|
57
|
+
hoge :: C
|
58
58
|
hoge = C (\n -> _if .$. (isZero .$. n) .$. one .$. n)
|
59
59
|
```
|
60
60
|
|
1
単純な例の誤りを修正した
answer
CHANGED
@@ -2,14 +2,14 @@
|
|
2
2
|
再帰的な型を扱うためには明示的に型を作成してやる必要があります。
|
3
3
|
|
4
4
|
より単純な例でまずは説明します。
|
5
|
-
たとえば
|
5
|
+
たとえばx x = x xのような場合xの型はどうなるでしょうか。
|
6
6
|
xの型がaだったとするとxは引数xを取り何かを返す関数でもあるのでxの型はa -> bとなります。
|
7
7
|
すると今度はxの型は(a -> b) -> cとなります。
|
8
8
|
さらにxの型は((a -> b) -> c) -> dとなり...のようにいつまでも型が決まりません。
|
9
9
|
このような場合、代数的データ型で明示的に再帰的な型を作ってやる必要があります。
|
10
10
|
newtype R a = R { unR :: R a -> a }のようにします。
|
11
11
|
すると、型R aは(R a -> a)を保持する再帰的な型となります。
|
12
|
-
このようにすると
|
12
|
+
このようにするとx x = unR x xのように表現することができます。
|
13
13
|
|
14
14
|
型Rの場合、再帰的になっているのは引数の部分('->'の左側)だけです。
|
15
15
|
Church数の場合、返り値('->'の右側)の部分も再帰的にする必要があるので、以下のような型となります。
|