F#でGADTsを実現する二つの方法

gistfile1.fs

module FPStyle =

  [<AbstractClass>]
  type Eq<'A, 'B> private () =
    abstract F : 'A -> 'B
    abstract G : 'B -> 'A
    static member Id<'A>() =
      { new Eq<'A, 'A>() with
        member this.F(x) = x
        member this.G(x) = x }

  [<AbstractClass>]
  type Term<'T> internal () = class end

  [<Sealed>]
  type Zero<'T> private (ev : Eq<int, 'T>) =
    inherit Term<'T>()
    member this.Ev = ev
    static member make() = Zero(Eq<int, 'T>.Id())

  [<Sealed>]
  type Succ<'T> private (prev : Term<'T>, ev : Eq<int, 'T>) =
    inherit Term<'T>()
    member this.Ev = ev
    member this.Prev = prev
    static member make(t) = Succ(t, Eq<int,'T>.Id())

  let (|Zero|Succ|) (term : Term<'T>) =
    match term with
    | :? Zero<_> as term -> Zero(term.Ev)
    | :? Succ<_> as term -> Succ(term.Prev, x.Ev)
    | _ -> failwith "invalid case"

  //F#でも多相再帰な関数は書ける。
  //ただし型推論は出来ない。多相再帰する場合には型を明記する必要がある。
  let rec eval term =
      match term with
      | Zero ev -> 0 |> ev.F
      | Succ (t, ev) -> ev.G (eval t) + 1 |> ev.F

module OOPStyle =

  [<AbstractClass>]
  type public Term<'T> internal () =
    abstract Eval : unit -> 'T

  [<Sealed>]
  type Zero() =
    inherit Term<int>()
    override this.Eval() = 0

  [<Sealed>]
  type Succ(prev : Term<int>) =
    inherit Term<int>()
    member this.Prev = prev
    override this.Eval() = prev.Eval() + 1

  //コードを一箇所に集めたいならVisitorパターンを使う
  //Visitorパターンを使うときにtype equalityを表す項を一緒に渡さないと駄目

F#にはhigher-kinded polymorphismが無いのでhttp://okmij.org/ftp/ML/first-class-modules/leibniz.ml のweak equalityしか定義できない。
なのでLeibniz's law: ('a, 'b) eq -> ('a tc, 'b tc) eqが利用できない。
ただしもしhigher-kinded polymorphismがF#にあったとしても、leibniz equalityではinverse of Leibniz's law: ('a tc, 'b tc) eq -> ('a, 'b) eqが作れないからinjectivity problemが解決できない。
これを解決するためにはHaskellのtype familyのような型をパターンマッチで分解する仕組みが必要。あるいはSystemFCのようにtype equalityとcoercionを言語に組み込むとか。
疑問点：型レベルCPSでパターンマッチを模倣してみたらどうか？→F#やHaskellだと型レベルのlambdaが無いから多分無理。そもそも出来ても使いにくくなる予感。

let rec foo<'T> () : 'T = fst (foo<'T * 'T> ())
↑のようにF#だと明示的な型適用を書けば普通に多相再帰できるっぽい。OCamlだと(moduleとか使わないと）無理かも。

System FC: http://www.cse.unsw.edu.au/~chak/papers/fc-tr.pdf
weak equalityの場合はいくつかのinjectivity problemが解決可能らしい（oleg氏のやつにも書いてある）。しかしSystem FCのように組み込みのtype equalityと比べると実行時に関数適用するからrun-time costがかかる。
あとbottomが使われちゃうとアレだからそういうのがsyntacticallyに防げて嬉しいとかなんとか。これは他のoleg氏の論文（多分promotion関連）で見た情報だったかも。

promotion関連の奴はolegさんは書いてなかったかも…。思い出せない…。

http://alaska-kamtchatka.blogspot.jp/2010/08/polymorphic-recursion-with-rank-2.html
新しいversionのOCamlだとpolymorphic recursionはmodule無くてもイケるとのこと。