日々の流転

λ. OCamlでランクn多相

レコードでもliftしたい - みずぴー日記 のコメントに関する補足。

関数を受け取って、レコードの型の異なる複数のフィールドに対して適用する高階関数を書きたいという話。

型の異なるフィールドに対して適用するには、受け取る関数は [Int]→[Int]→[Int] のような型の単相的な関数ではなく、∀a. [a]→[a]→[a] のような型の多相的な関数である必要がある。で、多相的な関数を受け取る高階関数の (∀a. [a]→[a]→[a])→Record→Record→Record のような型は、二階ラムダ計算の言葉でいうと、ランク2の型になっている。

ランクの正確な定義は Type reconstruction in finite-rank fragments of the polymorphic λ-calculus (c.f. The “Curry view” and the “Church view” of polymorphic λ-calculus - ヒビルテ (2006-04-25)) あたりを参照してもらうとして、ランク2の型はHindley-Milnerの型システムの表現力を超えるので、言語によって扱いが異なっていて面白い。

Haskellの場合

GHCはランク2多相(rank-2 polymorphism)をサポートしていて、型宣言を書きさえすれば自由に使うことが出来る*1。

{-# LANGUAGE Rank2Types #-}

data Record
    = R
    { x :: [Int]
    , y :: [Double]
    }

lift :: (forall a. [a] -> [a] -> [a]) ->
        Record -> Record -> Record
lift f R{ x=x1, y=y1 } R{ x=x2, y=y2 }
  = R{ x = f x1 x2, y = f y1 y2 }

append' :: Record -> Record -> Record
append' = lift (++)

ちなみに、Haskellでのランク2多相の使用例でもっとも有名なのは、STモナド(Control.Monad.STモジュール)の runST :: (forall s. ST s a) -> a で、これについては Lazy Functional State Threads で詳しく説明されている。

OCamlの場合

一方、OCamlの場合にはランクN多相に直接対応してはいない*2けど、レコードのフィールドが多相型を持つことが出来るので、多相関数をレコードに包んで受け渡すことでエンコードできる。

type some_record = {x:int list;y:float list}

type op = { app : 'a. 'a list -> 'a list -> 'a list }

let lift f {x=x1;y=y1} {x=x2;y=y2} =
  {x=f.app x1 x2;
   y=f.app y1 y2}

let append' = lift { app = (@) }

あと、同様の例として、昔のOCaml.jpにあったチャーチ数の例がある。

• Church 数 ― OCaml.JP
• <URL:http://web.archive.org/web/20060430024445/ocaml.jp/archive/sample/firstclass.ml>

Scalaの場合

Scalaでランクn多相をエミュレート - Onion開発停滞日記(2008-05-30) で水島さんがScalaへの翻訳を書いてくれました。ありがとうございます。 あとで自分でやろうと思ってたら先を越されてしまった(^^;

SML#の場合

現在のSML#にはこういった機能はないのかな。LLDN のときの上野さんの発表「Language Update: Standard MLer から見たML 概要」の「Next generation of ML」によると Rank-n polymorphism についても「理論的には完成。実装待ち」とのことなので、そのうち実装されるのだとは思うけど。

【2009-03-14追記】 ……と書いたけど、PPL2009で上野さんに聞いたら、どうもこういったファンシーな機能は当面実装されることはなさそうな感じだった。

F#の場合 (2009-02-19追記)

いげ太さんという方が、いげ太のブログ: F# で ランク N 多相っぽく でF#の場合について書かれていた。 F#ではOCaml流の多相的なフィールドを持つレコードではなく、ジェネリックなメソッドを持つインターフェースが推奨されているらしい。