equi-recursive type in ocaml †

参考: Developing Applications With Objective Caml より、

たとえば、タプル型でリストを作ったりできる。以下の例では、OCamlのequi-recursive typeのサポート(オプション-rectypes)を使って、1の無限リストを直積型で実現する。

Haskellではこれはできない。そもそも型システムがStructuralでなくNominalだから?(cf.TAPL, しかし耳学問、ソース求む)

$ ocaml
        Objective Caml version 3.09.3

# let rec ones = (1, ones);;
This expression has type int * (int * 'a) but is here used with type int * 'a
# ^D

$ ocaml -rectypes
        Objective Caml version 3.09.3

# let rec ones = (1,ones);;
val ones : int * 'a as 'a =
  (1,
   (1,
    (1,
     (1,
      (1,
       (1,
        (1,
         (1,
          (1,
           (1,
            (1,
             (1,
              (1,
               (1,
                (1,
                 (1,
                  (1,
                   (1,
                    (1,
                     (1,
                      (1,
                       (1,
                        (1,
                         (1,
                          (1,
                           (1,
                            (1,
                             (1,
                              (1,
                               (1,
                                (1,
                                 (1,
                                  (1,
                                   (1,
                                    (1,
                                     (1,
                                      (1,
                                       (1,
                                        (1,
                                         (1,
                                          (1,
                                           (1,
                                            (1,
                                             (1,
                                              (1,
                                               (1,
                                                (1,
                                                 (1,
                                                  (1,
                                                   (1,
                                                    (1,
                                                     (1,
                                                      (1,
                                                       (1,
                                                        (1,
                                                         (1,
                                                          (1,
                                                           (1,
                                                            (1,
                                                             (1,
                                                              (1,
                                                               (1,
                                                                (1,
                                                                 (1,
                                                                  (1,
                                                                   (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    (1,
                                                                    
(...)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
# 

val x : int * 'a as 'a という型表現に注目して頂きたい。不動点演算子μで書くとμ'a.int*'a という感じ。

Haskellでムリヤリ近いことをやる †

Haskellでムリヤリ実現するには。

newtype Rec t = R (t (Rec t))

という「型レベルの不動点コンビネータ」みたいなものを作る。Haskellでは、不動点コンビネータYは y f = f (y f)となるのを思い出してほしい。

この型構築子は、

ones = R (1, ones)

などとして使う。このonesの型は

*Main> :t ones
ones :: Rec ((,) Integer)

である。 (型(a,b)は (,) a b と表記されることに注意。(,)は2引数の型構築子で、 (,) Integer は型の半適用。)

型の構造で再帰型が表現できているわけではないが(この表現であってる?)、データは再帰的である。

このデータを使うには、 データ構築子Rを介して再帰を展開する必要がある:

printRec (R (a,r)) = "(" ++ show a ++ "," ++ printRec r
*Main> printRec ones
(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,(1,....

(けいご)

トップ   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS