summaryrefslogtreecommitdiff
path: root/posts/typed-racket-and-excluded-middle.sxml
blob: 3c54e5fb6f14192f240f6849c06ac0d595985668 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
(use-modules (haunt utils))

`((title . "排中律と二重否定除去をTyped Racketで実装する")
  (id . "typed-racket-and-excluded-middle")
  (date . ,(string->date* "2020-03-26 02:20"))
  (content
   (p "Qiita を退会したときに消えてしまった記事を復元したものです。")
   
   (p (a (@ (href "https://qiita.com/mod_poppo/items/eb59428206371ff4751a"))
         "排中律と二重否定除去をSMLで実装する")
      "という記事で、Typed Racket という静的型のあるSchemeがあるらしいと噂されていたため、Typed Racket を使って実装してみました。")
   (p "上記の記事を読んでから先に進んでください。")
   (h2 "Typed Racket で直和型を表現する")
   (p "最初に直面したのは"
      (a (@ (href "https://blog.miz-ar.info/2015/01/union-types/"))
         "Union Typesは直和型ではない")
      "という問題でした。(上の記事ではTypeScriptのUnion Typesについて説明されていますが、Typed RacketのUnion Typesについても同様のことが言えます)")
   (p "Typed Racket で直和型を表現するために"
      (code "left") "," (code "right")
      "という構造体をそれぞれ用意して、"
      (code "(U (Left A) (Right B))")
      "へのエイリアスとして"
      (code "Either")
      "を定義することにしました。")
   (pre (code
         ,(string-join
           (list
            "#lang typed/racket"
            ""
            "(struct (A) right ([value : A])"
            "  #:type-name Right)"
            ""
            "(struct (A) left ([value : A])"
            "  #:type-name Left)"
            ""
            "(define-type (Either A B) (U (Left A) (Right B)))")
           "\n")))
   (h2 "Typed Racketで爆発律と否定を実装する")
   (p "Typed Racket では" (code "Nothing") "という値を持たない型があり、元記事で" (code "void") "と定義されていた型と対応しています。"
      (code  "Nothing") "型を利用すると" (code "absurd") "と" (code "not")
      "型は以下のように実装することができます。")
   (pre (code
         ,(string-join
           (list
            "(: absurd (All (A) (-> Nothing A)))"
            "(define (absurd x)"
            "  (absurd x))"
            ""
            "(define-type (Not A) (-> A Nothing))")
           "\n")))
   (h2 "Typed Racketによる排中律の実装")
   (p "では、Typed Racket で排中律を実装してみましょう。Typed Racket では0個の引数をとる手続きが書けるので、" (code "excluded-middle") "の型は" (code "(-> (Either A (Not A)))") "とするのが自然だと思われます。また、Typed Racket ではある型Aの値を受けとる継続は" (code "(-> A Nothing)") "のような" (code "Nothing") "型を戻り値とする手続きであることに注意してください(これは呼ばれたら決して戻ってこないことを意味しています)。")
   (pre (code
         ,(string-join
           (list
            "(: excluded-middle (All (A) (-> (Either A (Not A)))))"
            "(define (excluded-middle)"
            "  (call/cc"
            "   (lambda ([k : (-> (Either A (Not A)) Nothing)])"
            "     (right (lambda ([x : A])"
            "              (k (left x)))))))"
            ""
            "(let ([x : (Either String (Not String)) (excluded-middle)])"
            "  (cond"
            "    [(left? x)"
            "     (displayln (left-value x))]"
            "    [else"
            "     (display \"Hello \")"
            "     ((right-value x) \"world!\")]))"
            )
           "\n")))
   (p "元記事の例と同様に Hello world! と出力されるはずです。")

   (h2 "Typed Racketによる二重否定の除去の実装")
   (p "元記事の演習問題の解答に相当するため、自分で解きたい人は飛ばしてください。
ただ、Union Typesがないと使用例が動かない気がするので、これだとSMLでは動かないような……。")
   (pre (code
         ,(string-join
           (list
            "(: double-negative-elimination (All (A) (-> (Not (Not A)) A)))"
            "(define (double-negative-elimination not-not-a)"
            "  (let ([f : (Either A (Not A)) (excluded-middle)])"
            "    (cond"
            "      [(left? f)"
            "       (left-value f)]"
            "      [else"
            "       (not-not-a (right-value f))])))"
            ""
            "(let ([x (call/cc"
            "          (lambda ([k : (Not (Not String))])"
            "            (double-negative-elimination k)))])"
            "  (if (string? x)"
            "      (displayln x)"
            "      (x \"Hello world!\")))")
           "\n")))
   (p "Hello world! と出力されます。")
   (h2 "宣伝")
   (p "Typed Racketは静的に型付けられたバージョンのRacketで、後付けで型を追加したプログラミング言語のなかでは本当に良くできていると思います。"
      "Typed Racketに興味をもった人は" (a (@ (href "https://download.racket-lang.org/")) "Racketをインストール") "して、"
      (a (@ (href "https://docs.racket-lang.org/ts-guide/"))
         "Typed Racket")
      "を始めましょう!")))