この記事は Haskell Advent Calendar 2020 20日目の記事です．

TL; DR#

タイトル

Dhall の Prelude を眺めていて見付けた，ランク2多相を使ったテクニックを紹介する．

前編はこちら

一昨年のゴールデンウィークに池袋のジュンク堂を訪れた際，『形式意味論入門』という表題の本に目が止まり，数学や論理学を用いて自然言語表現の意味を形式的に考察する学問分野があることを知った^*1．また，その道具立てとして単純型付きラムダ計算が用いられていることが，なおのこと私の興味を惹いた．ラムダ計算といえば，読者の多くが計算機科学分野での応用を思い浮かべると思うが，Richard Montague^*2 が自然言語分野に応用して以来，そちらの方面でも道具立てとして用いられているようである．

この本は，Irene Heim と Angelika Kratzer による Semantics in Generative Grammar (以下 Heim and Kratzer) をベースに書かれているのだが，Heim and Kratzer で用いられる意味計算規則のうち，実質的に用いられるものはたった4つであるとし，前半で4つの意味計算規則の導入を行い，後半ではその他の自然言語現象に対して形式的な意味を与えていく，という構成になっている．また，統語論を学んだ人文学系の学生を対象読者として書かれているため．序盤では集合論やラムダ計算に関する非形式的な説明に文量が割かれている．

この記事は，私が『形式意味論入門』の内容の習得を試みる際に，自分の理解が正しいかを確かめるため，Haskell のコードとして書き下した内容を下地に書かれている．言語表現及びそれらの外延をプログラム，とりわけ Haskell のプログラムにエンコードするメリットとしては，

• 意味計算を自力で行う必要がない
• 型の整合性が GHC の型検査機によって自動的に保証される

などが挙げられるだろう．

この記事は前後編に分かれている．前編では，事前知識の導入の後，4つの意味計算規則のうち最初の2つを導入する．後編では，更なる準備の後，残る2つの意味計算規則を導入する．

みなさん，Haskell やってますか？普通に Haskell IDE Engine を入れようとするとビルドにメッチャ時間がかかって「地獄か？」という感じがするので，Nix でシュッと入れていきましょう．

「関数プログラミングとはなんですか？」と問われたときには「デ，データファースト……(震え声)」と答えることが多いのだが，実際 Haskell や OCaml などの言語を特徴付けるものとして，代数的データ型 (Algebraic Data Type; ADT) の存在は無視できないだろう．その有用性ゆえに，近年では新たな言語の策定の際にその概念が輸出され，Rust や Swift などの言語にも採用されている．

「代数的データ型とはなんですか？」と問われたときには——問われたことがないのでわからないのだが——おもむろに ghci か utop を立ち上げて，解説を始めるのではないかと思う．ひとしきり解説をした後，「つまり直積の直和なんですよ〜🙌✨」と言って話を締めくくるだろう．

int 型や float 型など，「メモリ上の表現」という計算機の気持ちに極めて寄り添ったプリミティヴなデータ型や，オブジェクトがヒープに展開された先のアドレスを保持する参照型にしか馴染みがないプログラマにとっては，データ型の定義に「代数」などという仰々しい概念が登場するのは不思議に思われるかもしれない．しかし，代数的データ型自体の有用性は，少しプログラムを書けばわかる^*1はずであるし，そもそも「代数」などという難しい言い方をしなければ，自然数どうしの足し算や掛け算，指数の計算などは，小中学校での教育を通じて万人が既に知っており，日頃から親しんでいるはずである．この記事では，人々がよく知る計算の上に成り立つ法則と，代数的データ型との類似性を示すことで，代数的データ型に親しみを持ってもらうことを目的としている．この記事を読み終えた頃には，「Option[T] とか T? とかいう型は $T+1$ とでも書かれるべきものなのか〜」という理解がなされることが期待される．

基礎的な Haskell の読み書きと，概ね中学校から高校1年生くらいで習う程度の数学の知識があれば読み進められるはずである．また，この記事では再帰的に定義されたデータ型は扱わない^*2．

operational (あるいは freer) と呼ばれているものの説明として，

• a) Coyoneda を使うと，kind が * -> * であるような任意の型から functor を作り出せる
  • 任意の型 f :: * -> * について Coyoneda f は Functor のインスタンスになる
• b) Free を使うと，任意の functor から monad を作り出せる
  • Functor のインスタンスである任意の型 f について Free f は Monad のインスタンスになる
• a と b を組み合わせると，適当な型 f :: * -> * から monad を作り出せて便利〜🙌

というストーリーが往々にして語られる^*1．

Template Haskell を使って，時間の長さをいい感じに (人間が読みやすい形で) 記述できるライブラリを作った．

たまには初学者向けにライトな話題を．

対象読者#

• すごいH本を12章か13章ぐらいまでは読んだ
• do 構文を使って IO などの処理が書ける
• Haskell のプログラムはなんとなく書けるが，あまり綺麗に書けている気がしない

FunctionalDependencies という GHC 言語拡張がある．Haskell Wiki によると，

Functional dependencies are used to constrain the parameters of type classes.

と書かれているが，これはどういうことか．

Haskell Language Report で定められた範囲では，型クラスに与えられるパラメータは1つに限られるが，MultiParamTypeClasses を用いると，複数のパラメータを与えることができる．この際に，パラメータとして与えられた (複数の) 型の間の関係性に制限を加えることができるのが，FunctionalDependencies なのであった．恐らく多くの人が初めて目にするのは，mtl package の MonadReader の定義なのではないだろうか．| m -> r というのがそれである．

class Monad m => MonadReader r m | m -> r where
   ...

さて，GHC 8 から TypeFamilyDependencies という GHC 言語拡張が追加された．これについては既に lotz 先生が『型族が単射だと嬉しい理由』という記事を書いていらっしゃるのだが，(氏には失礼ながら) 少しばかりわざとらしい例だと感じたので，もう少し実務的な例を引き合いに出して，有用性を示したいと思う．

前回よりはもう少し実用的な例を．

Template Haskell を使って，Haskell のコード中に JSON をそのまま埋め込むことができるようにする．また，あらかじめ用意しておいた JSON ファイルをコンパイル時に読み込み，指定したデータ型の値にする．

ToC#

1. コード中に JSON を埋め込む
2. コンパイル時に JSON をファイルから型安全に読み込む

数ヶ月前に Twitter で，コンパイル時に FizzBuzz を計算して，実行時には計算された文字列を出力をするだけ，というコンパイル時 FizzBuzz を何かの言語でやっているのを見かけた．元ネタは江添さんがC++で書いたものらしい．インスピレーションを受けて，Haskell で書いてはみたが，簡単すぎて全然おもしろくなくなってしまった．

Rust には std::str::FromStr という trait があり，データ型がこれを実装すると，from_str という名前の associated function^*1 を通じて，str からそのデータ型に変換できるようになる．