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

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

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

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

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

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をインストールして、Typed Racketを始めましょう！