排中律と二重否定除去を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 では 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 では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! と出力されるはずです。

元記事の演習問題の解答に相当するため、自分で解きたい人は飛ばしてください。 ただ、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を始めましょう！