#contents

* equi-recursive type in ocaml [#a4970a31]
参考:
[[Developing Applications With Objective Caml:http://caml.inria.fr/pub/docs/oreilly-book/]] より、
- [[Cyclic types:http://caml.inria.fr/pub/docs/oreilly-book/html/book-ora208.html]]
- [[Option -rectypes:http://caml.inria.fr/pub/docs/oreilly-book/html/book-ora209.html]]

たとえば、タプル型でリストを作ったりできる。以下の例では、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でムリヤリ近いことをやる [#g9493987]
Haskellでムリヤリ実現するには。

 newtype Rec t = R (t (Rec t))
という「型レベルの不動点コンビネータ」みたいなものを作る (''FIXME:''出典求む)。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