aboutsummaryrefslogtreecommitdiff
path: root/posts/typed-racket-and-excluded-middle.md
blob: 0e9853bff6d449f8433c525ee4fc8f8e53ba9562 (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
title: 排中律と二重否定除去をTyped Racketで実装する
id: typed-racket-and-excluded-middle
date: 2020-03-26 02:20
---
Qiita を退会したときに消えてしまった記事を復元したものです。

[排中律と二重否定除去をSMLで実装する](https://qiita.com/mod_poppo/items/eb59428206371ff4751a)という記事で、Typed
Racket という静的型のあるSchemeがあるらしいと噂されていたため、Typed
Racket を使って実装してみました。

上記の記事を読んでから先に進んでください。

## Typed Racket で直和型を表現する

最初に直面したのは[Union
Typesは直和型ではない](https://blog.miz-ar.info/2015/01/union-types/)という問題でした。(上の記事ではTypeScriptのUnion
Typesについて説明されていますが、Typed RacketのUnion
Typesについても同様のことが言えます)

Typed Racket
で直和型を表現するために`left`,`right`という構造体をそれぞれ用意して、`(U (Left A) (Right B))`へのエイリアスとして`Either`を定義することにしました。

    #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)))

## Typed Racketで爆発律と否定を実装する

Typed Racket
では`Nothing`という値を持たない型があり、元記事で`void`と定義されていた型と対応しています。`Nothing`型を利用すると`absurd`と`not`型は以下のように実装することができます。

    (: absurd (All (A) (-> Nothing A)))
    (define (absurd x)
      (absurd x))

    (define-type (Not A) (-> A Nothing))

## Typed Racketによる排中律の実装

では、Typed Racket で排中律を実装してみましょう。Typed Racket
では0個の引数をとる手続きが書けるので、`excluded-middle`の型は`(-> (Either A (Not A)))`とするのが自然だと思われます。また、Typed
Racket
ではある型Aの値を受けとる継続は`(-> A Nothing)`のような`Nothing`型を戻り値とする手続きであることに注意してください(これは呼ばれたら決して戻ってこないことを意味しています)。

    (: 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!")]))

元記事の例と同様に Hello world! と出力されるはずです。

## Typed Racketによる二重否定の除去の実装

元記事の演習問題の解答に相当するため、自分で解きたい人は飛ばしてください。
ただ、Union
Typesがないと使用例が動かない気がするので、これだとSMLでは動かないような……。

    (: 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!")))

Hello world! と出力されます。

## 宣伝

Typed
Racketは静的に型付けられたバージョンのRacketで、後付けで型を追加したプログラミング言語のなかでは本当に良くできていると思います。Typed
Racketに興味をもった人は[Racketをインストール](https://download.racket-lang.org/)して、[Typed
Racket](https://docs.racket-lang.org/ts-guide/)を始めましょう!