天泣記

ふと思い立って、Coq で依存型を使って arity が変化する関数を書いてみた。

Fixpoint dt n :=
  match n with
  | O => nat
  | S n' => nat -> dt n'
  end.

Fixpoint f' acc n : dt n :=
  match n with
  | O => acc
  | S n' => fun v => f' (acc+v) n'
  end.

Definition f n : dt n := f' 0 n.

Goal f 0 = 0. Proof. reflexivity. Qed.
Goal f 1 10 = 10. Proof. reflexivity. Qed.
Goal f 2 10 20 = 30. Proof. reflexivity. Qed.
Goal f 3 10 20 30 = 60. Proof. reflexivity. Qed.
Goal f 9 10 20 30 40 50 60 70 80 90 = 450. Proof. reflexivity. Qed.

f は最初の引数でそれに続く引数の数を指定し、その数だけ nat を与えるとそれらの和を返す。最初の引数の値に依存して、0 なら nat を返し、そうでなければ関数を返す、という型なので、依存型というわけである。

Goal で確認してみるとちゃんと動いているようである。

ところで、Goal って unit test みたいですね。

さて、extraction もできないわけではない。

Require Import ExtrOcamlBasic.
Require Import ExtrOcamlNatInt.
Extraction f'.
Extraction f.

で、OCaml で動かすとなんか警告がでるが、動くようである。(int に cast しないと <poly> と表示されて中身がわからないが)

# let add = (+);;
val add : int -> int -> int = <fun>
# let rec f' acc n =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ ->
    Obj.magic acc)
    (fun n' ->
    Obj.magic (fun v -> f' (add acc v) n'))
    n            ;;
            val f' : int -> int -> 'a = <fun>
# let f n =
  f' 0 n  ;;
  val f : int -> 'a = <fun>
# f 0;;
- : 'a = <poly>
# (f 0 : int);;
- : int = 0
# (f 1 10 : int);;
Warning 20: this argument will not be used by the function.
- : int = 10
# (f 2 10 20 : int);;
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
- : int = 30
# (f 9 10 20 30 40 50 60 70 80 90 : int);;
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
- : int = 450

まぁ、Obj.magic を使っていることからも分かるように、安全ではない。以下のように余計に引数を与えると SEGV する。

# f 0 100;;
Warning 20: this argument will not be used by the function.
zsh: segmentation fault  ocaml

Coq の Extraction は OCaml, Haskell, Scheme (と JSON) をサポートしている。Scheme なら型で問題になることはないだろうから、もうひとつ Haskell で試してみよう。

Require Import ExtrHaskellBasic.
Require Import ExtrHaskellNatInt.
Extraction Language Haskell.
Extraction dt.
Extraction f'.
Extraction f.

出てくるのは以下のコードである。

type Dt = Any

f' :: Prelude.Int -> Prelude.Int -> Dt
f' acc n =
  (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
    (\_ ->
    unsafeCoerce acc)
    (\n' ->
    unsafeCoerce (\v -> f' ((Prelude.+) acc v) n'))
    n

f :: Prelude.Int -> Dt
f n =
  f' 0 n

んー、実行する方法がわからないな。ロードまでは以下の指定を先頭につければいいことがわかった。

import Unsafe.Coerce
import qualified GHC.Prim
type Any = GHC.Prim.Any

そういう内容を a.hs に入れて、以下のようにしてもエラーになってしまう。

% ghci a.hs
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( a.hs, interpreted )
Ok, modules loaded: Main.
*Main> f

<interactive>:2:1:
    No instance for (Show (Int -> Dt)) arising from a use of `print'
    Possible fix: add an instance declaration for (Show (Int -> Dt))
    In a stmt of an interactive GHCi command: print it
*Main> f 0

<interactive>:3:1:
    No instance for (Show Dt) arising from a use of `print'
    Possible fix: add an instance declaration for (Show Dt)
    In a stmt of an interactive GHCi command: print it
*Main> f 1

<interactive>:4:1:
    No instance for (Show Dt) arising from a use of `print'
    Possible fix: add an instance declaration for (Show Dt)
    In a stmt of an interactive GHCi command: print it
*Main> f 1 10

<interactive>:5:1:
    Couldn't match expected type `a0 -> t0'
                with actual type `GHC.Prim.Any *'
    The function `f' is applied to two arguments,
    but its type `Int -> Dt' has only one
    In the expression: f 1 10
    In an equation for `it': it = f 1 10

#1 Coq Bug 5507 - Spelling miss: 'Brujin' should be 'Bruijn'.

Coq Bug 5507 - Bug 5507 - Spelling miss: 'Brujin' should be 'Bruijn'.

天泣記

2017-06-04 (Sun)

2017-05-30 (Tue)

2017-05-28 (Sun)

2017-05-27 (Sat)

2017-05-17 (Wed)

2017-05-08 (Mon)

2017-05-01 (Mon)