Arantium Maestum

プログラミング、囲碁、読書の話題

let rec内での多相とlocally abstract typeとpolymorphic type constraints

OCaml

こういう記事を最近読んだ：

tatta.hatenadiary.org

（書かれたのは10年以上前だが）

こういうコードは型チェック通らないよ、という話：

let rec f x = x 
and g () = f 1
and h () = f true;;

Line 3, characters 13-17:
Error: This expression has type bool but an expression was expected of type int

let rec ... and ... and ...という構文の中ではlet多相が効かないということらしい。

let rec ... in ...ならもちろんlet多相で大丈夫：

let rec f x = x in
let g () = f 1 in
let h () = f true in
(g ()), (h ());;

- : int * bool = (1, true)

じゃあ明示的に型をつければ？とナイーブな付け方をしてみると：

let rec f : 'a -> 'a = fun x -> x
and g () = f 1
and h () = f true;;

Line 3, characters 13-17:
Error: This expression has type bool but an expression was expected of type int

これは失敗する。その理由については以前記事を書いた：

zehnpaard.hatenablog.com

のでこういう風には多相を強要できず、let rec ... and ... and ...が（この構文の中では）単相になってしまう。

locally abstract type

記事を読んで手元で試したときは「はえー」と思ったくらいだったのだが、ここ数日GADTについて調べているときにlocally abstract typeに遭遇した。

ふとこの問題にlocally abstract typeが使えるのでは？と思って試してみた：

let rec f : type a. a -> a = fun x -> x
and g () = f 1
and h () = f true;;

val f : 'a -> 'a = <fun>
val g : unit -> int = <fun>
val h : unit -> bool = <fun>

これは通るので成功。locally abstract type、小技として便利そう。

Polymorphic type constraints

ここまで記事を書いてちょっと寝かせておいたら、こんな記事に遭遇した：

www.craigfe.io

The punchline is that OCaml actually does have syntax for expressing polymorphic constraints – and it even involves an explicit quantifier – but sadly it's not often taught to beginners:

let id : 'a. 'a -> 'a = (fun x -> x + 1)

知らなかった・・・

let rec f : 'a. 'a -> 'a = fun x -> x
and g () = f 1
and h () = f true;;

val f : 'a -> 'a = <fun>
val g : unit -> int = <fun>
val h : unit -> bool = <fun>

これで問題なくうまくいくようだ・・・

この構文で

  • let rec ... and ...などで関数が単相にならないようにする
  • 関数の実装的に単相的なものを型検査で弾く

の両方ができるらしい。

しかしGADTで：

type 'a t =
  Int : int -> int t
| Char : char -> char t

let get : 'a. 'a t -> 'a = function
  Int x -> x
| Char x -> x

とは書けない。ここの違いに関してはまだ理解できていない・・・　（'a. 'a -> 'aがダメな理由はなんとなくわかるが、locally abstract typeはそれ以上の何をしているのだろう？）

追記１

こういうご指摘を@camloebaさんにいただいた：

なるほど・・・　この例だと実行時は最初のf xで無限ループになるが、こういうこともできるわけだ：

let rec f : 'a. ('a * int) -> unit =
  fun (x, y) ->
    if y = 0 then ()
    else (print_endline "hello"; f ((x,x), y-1));;

引数のタプルの第一要素の型は再帰するたびに変わる（倍々になっていく）がpolymorphic type constraintを入れているので大丈夫。let rec f = fun ...と型制約を入れない場合は多相だと型推論しないのでエラー。

追記２

こちらは@dico_lequeさんに教えていただいた：

たしかに・・・(type a) : a -> aのようなOCaml 3.12で追加されたlocally abstract type構文ではダメで：

let rec f (type a) : a -> a = fun x -> x
and g () = f 1
and h () = f true;;

Line 3, characters 13-17:
Error: This expression has type bool but an expression was expected of type int

4.00で追加されたlocally abstract typeのpolymorphic syntax let rec f : type a. a -> aを使う必要がある。（GADTで使うのもこちらの構文）

@camloebaさん、@dico_lequeさんご教示いただきありがとうございます！