質問するログイン新規登録

回答編集履歴

4

単純な例の誤解しやすい点の改善

2015/08/15 00:15

投稿

YoshikuniJujo
YoshikuniJujo

スコア33

answer CHANGED
@@ -2,14 +2,14 @@
2
2
  再帰的な型を扱うためには明示的に型を作成してやる必要があります。
3
3
 
4
4
  より単純な例でまずは説明します。
5
- たとえばx x = x xのような場合xの型はどうなるでしょうか。
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
- このようにするとx x = unR x xのように表現することができます。
12
+ このようにするとf x = unR x xのように表現することができます。
13
13
 
14
14
  型Rの場合、再帰的になっているのは引数の部分('->'の左側)だけです。
15
15
  Church数の場合、返り値('->'の右側)の部分も再帰的にする必要があるので、以下のような型となります。

3

型変数の削除の変更漏れの修正

2015/08/15 00:15

投稿

YoshikuniJujo
YoshikuniJujo

スコア33

answer CHANGED
@@ -18,7 +18,7 @@
18
18
  実際にしていることはCとunCによって関数をデータ型Cに入れたり出したりしているということになります。
19
19
 
20
20
  静的な型付けで再帰的な型を定義するこのやりかたは僕には非常に美しいように感じます。
21
- またA (C a)やZはChurch数を数値に変換するために用意したもので、本質的な部分ではありません。
21
+ またA CやZはChurch数を数値に変換するために用意したもので、本質的な部分ではありません。
22
22
 
23
23
  ```Haskell
24
24
  data C = C { unC :: C -> C } | A C | Z

2

型変数は不要であることに気づく。

2015/08/14 18:41

投稿

YoshikuniJujo
YoshikuniJujo

スコア33

answer CHANGED
@@ -21,31 +21,31 @@
21
21
  またA (C a)やZはChurch数を数値に変換するために用意したもので、本質的な部分ではありません。
22
22
 
23
23
  ```Haskell
24
- data C a = C { unC :: C a -> C a } | A (C a) | Z
24
+ data C = C { unC :: C -> C } | A C | Z
25
25
 
26
- (.$.) :: C a -> C a -> C a
26
+ (.$.) :: C -> C -> C
27
27
  (.$.) = unC
28
28
 
29
- toInt :: C a -> Int
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 a
34
+ toChurch :: Int -> C
35
35
  toChurch 0 = zero
36
36
  toChurch n = s .$. toChurch (n - 1)
37
37
 
38
- false, true, _if :: C a
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 a
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 a
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 a
57
+ hoge :: C
58
58
  hoge = C (\n -> _if .$. (isZero .$. n) .$. one .$. n)
59
59
  ```
60
60
 

1

単純な例の誤りを修正した

2015/08/14 18:39

投稿

YoshikuniJujo
YoshikuniJujo

スコア33

answer CHANGED
@@ -2,14 +2,14 @@
2
2
  再帰的な型を扱うためには明示的に型を作成してやる必要があります。
3
3
 
4
4
  より単純な例でまずは説明します。
5
- たとえばy = x xのような場合xの型はどうなるでしょうか。
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
- このようにするとy = unR x xのように表現することができます。
12
+ このようにするとx x = unR x xのように表現することができます。
13
13
 
14
14
  型Rの場合、再帰的になっているのは引数の部分('->'の左側)だけです。
15
15
  Church数の場合、返り値('->'の右側)の部分も再帰的にする必要があるので、以下のような型となります。