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

Dhallのビルトイン型の一部（e.g. Natural, Option, List）にはそれぞれbuildという関数が定義されている．これはコメントで"inverse of fold"と説明されているから，最も普遍的に値を構築する手段として提供されているようである．

例えば，Natural/build関数の型は以下のようになっている．

⊢ :t Natural/build

( ∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural
) →
  Natural

引数として受け取った関数を元にNatural型の値を構築する関数であることがわかる．引数として受け取る関数の型は ∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → naturalである．このような型を持つ関数mkThreeを定義してみよう．

⊢ :let mkThree = λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → succ (succ (succ zero))

  mkThree
: ∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural

Natural/buildをmkThree関数に適用すると，無事に3という値を構築することができる．

⊢ Natural/build mkThree

3

さて，Dhallには自然数のリテラルが存在するので，succ (succ (succ zero))などと回りくどい記述をする代わりに，直接3と書けないのだろうか．実際に確かめてみると，残念ながらこの試みは失敗に終わる．

⊢ Natural/build (λ(natural : Type) → λ(_ : natural → natural) → λ(_ : natural) → 3)

Error: Wrong type of function argument

  …
→ …
→ …
→ - _@2
  + Natural

1│ Natural/build (λ(natural : Type) → λ(_ : natural → natural) → λ(_ : natural) → 3)

(input):1:1

型_@2とNaturalが一致していないというエラーが得られた．_@2の2はde Bruijn indexで，最も外側のラムダ抽象で導入された（型)）変数naturalを指している．値3は大文字のNatural型を持つが，これが全称量化された型変数naturalと一致しないのである．このラムダ抽象の本体はnatural型の値を返さねばならず，そのような値は（naturalが全称量化されているがゆえに）succ : natural → naturalとzero : naturalを通じてのみしか構築することができないのだ．

同様の関数をHaskellで定義してみよう．

{-# LANGUAGE Rank2Types #-}

import GHC.Natural (Natural)

build :: (forall natural. (natural -> natural) -> natural -> natural) -> Natural
build f = f (+ 1) 0

生産者は，第1引数に(+ 1) :: Natural -> Naturalを，第2引数に0 :: Naturalを供給する．しかし，消費者の立場から見れば，量化されたnatural型にしかアクセスできないので，内部実装にNaturalが使われていることなど知る由もない．その結果，引数で受け取ったsuccとzeroのみを使って値を構築することしかできないのである．

mkThree :: forall natural. (natural -> natural) -> natural -> natural
mkThree succ zero = succ (succ (succ zero))

three :: Natural
three = build mkThree -- 3

このテクニックの応用例を考えてみたが，残念ながら特に何も思い付かなかった．ライブラリを設計する際，syntacticなconstruction methodだけをユーザに提供したいというモチベーションがあるならば，パターンとして頭の片隅に置いておいて損はないかもしれない．