排中律と二重否定除去をTyped Racketで実装する

目次

投稿日: 2020-03-26 木

Qiita を退会したときに消えてしまった記事を復元したものです。

排中律と二重否定除去をSMLで実装するという記事で、Typed Racket という静的型のあるSchemeがあるらしいと噂されていたため、Typed Racket を使って実装してみました。

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

1. Typed Racket で直和型を表現する

最初に直面したのは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)))

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

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

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

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

3. 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! と出力されるはずです。

4. 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! と出力されます。

5. 宣伝

Typed Racketは静的に型付けられたバージョンのRacketで、後付けで型を追加したプログラミング言語のなかでは本当に良くできていると思います。Typed Racketに興味をもった人はRacketをインストールして、Typed Racketを始めましょう!

著者: Masaya Tojo

Twitter: @tojoqk

Mastodon: @tojoqk, English: @tojo

RSS を購読する

トップページに戻る