Open16

Agda やるぞ

インストールしてみる

https://agda.readthedocs.io/en/latest/getting-started/hello-world.html

Agda

Haskellの環境はあるので,公式ガイド通りにやる.

sudo apt-get update
sudo apt-get install zlib1g-dev libncurses5-dev
cabal update
cabal install Agda

めちゃくちゃパッケージがインストールされる(60個ほど).僕の環境では38.2mとかなり遅かった.

agda-mode

ガイドではemacsだが,僕はVSCodeを使いたい.
調べたところ拡張機能があるようなので利用させてもらう.

https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode

hello

最初のプログラム

https://agda.readthedocs.io/en/latest/getting-started/hello-world.html#hello-agda
Haskellと違って型は:で指定するようだ.
putStrLnなどはHaskellからFFIとして導入するみたい.

実行

agda --compile hello-world.agda  
./hello-world  

結果

Hello world!

いいですね

data Greeting : Set where
  hello : Greeting

Setはなんだろう カインドっぽいけどわからない

https://agda.readthedocs.io/en/latest/getting-started/a-taste-of-agda.html

依存型を使ったVectorの例

型チェックしたらData.Natがないって怒られた.標準ライブラリのインストールを忘れていた.

https://github.com/agda/agda-stdlib/blob/master/notes/installation-guide.md
に従って手動でインストールした.パッケージマネージャ欲しい……欲しくない?

インストール後に型チェックを走らせたら通った いいね

コードに関しては,型定義はHaskellのGATsみたいな感じ.
open importqualifiedがついていないimportのような感じか
∀ {n}forall n.っぽい
複数の引数の間にを書かなくていい?
あと引数の名前も型についてる
演算子の周りにはスペースを入れないと動かないっぽい?

キーバインドに関して,=は直接打たないといけないんですかね?日本語キーボードに=ないので詰んでるんですが……

variable
  A : Set
  n : ℕ

variable構文で関数のデフォルトの型変数を指定できるみたい

無限ループはできないようになっているらしいので,確かめてみる.

loopTest : Nat  Nat
loopTest x = loopTest x

結果

Termination checking failed for the following functions:
  loopTest
Problematic calls:
  loopTest x

判別できている,今後仕組みを調べたい.

加算の結合法則の証明

型で証明したいことを書いて,実装で証明していく.それにしても+-assocってすごい名前だ

関数の型が難しい
いろんな書き方ができるけど,個人的には

_ : {x : X} {y : Y}  (a : A)  (b : B)  C

みたいなのが分かりやすい

この場合,x, yは型変数(?)として導入されていて,_A型の値とB型の値をとってC型の値を返す関数であり,a, bは依存型のパラメーターとして導入されている

例としてa \times (b + c) = a \times b + a \times cを証明してみたい.

module distributive where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

lemma : Set
lemma = (a b c :)  a * (b + c) ≡ a * b + a * c

proof : lemma
proof zero b c = refl
proof (suc a) b c =
  begin
    b + c + a * (b + c)
  ≡⟨ cong (_+_ (b + c)) (proof a b c)⟩
    b + c + (a * b + a * c)
  ≡⟨ assoc b c (a * b + a * c) ⟩
    b + (c + (a * b + a * c))
  ≡⟨ cong (_+_ b) (sym (assoc c (a * b) (a * c)))⟩
    b + (c + a * b + a * c)
  ≡⟨ cong (_+_ b) (cong (+right (a * c)) (comm c (a * b))) ⟩
    b + (a * b + c + a * c)
  ≡⟨ cong (_+_ b) (assoc (a * b) c (a * c)) ⟩
    b + (a * b + (c + a * c))
  ≡⟨ sym (assoc b (a * b) (c + a * c)) ⟩
    b + a * b + (c + a * c)where
  open ≡-Reasoning

  +right : ℕ
  +right a b = b + a

  assoc : (a b c :)  a + b + c ≡ a + (b + c)
  assoc zero b c = refl
  assoc (suc a) b c = cong suc (assoc a b c )

  comm : (a b :)  a + b ≡ b + a
  comm zero zero = refl
  comm zero (suc b) = cong suc (comm zero b)
  comm (suc a) zero = cong suc (comm a zero)
  comm (suc a) (suc b) = cong suc (
    begin
      a + suc b
    ≡⟨ shift a b ⟩
      suc (a + b)
    ≡⟨ comm (suc a) b ⟩
      b + suc a
    ∎
    )
    where
    shift : (a b :)  a + suc b ≡ suc a + b
    shift zero b = refl
    shift (suc a) b = cong suc (shift a b)

できた(?)

まだ短くできそう

基本的に?でHole作って,C-c C-,で型を見つつ,C-c C-aで自動補完,それができなかったら適当に変数書いてC-c C-cで場合分けとか,なんか関数書いてC-c C-rで外に出すとかして証明を行う

複雑になりそうだったら≡-Reasoningを使って変形していく

って感じかな?

加法の交換法則と結合法則,分配法則,乗法の交換法則と結合法則を証明してみました

こういうのは数打って慣れるしかない(と思ってる)

module multi where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning

+assoc-proof : (a b c :)  (a + b) + c ≡ a + (b + c)
+assoc-proof zero b c = refl
+assoc-proof (suc a) b c = cong suc (+assoc-proof a b c)

+comm-proof  : (a b :)  a + b ≡ b + a
+comm-proof  zero zero = refl
+comm-proof  zero (suc b) = cong suc (+comm-proof  zero b)
+comm-proof  (suc a) zero = cong suc (+comm-proof  a zero)
+comm-proof  (suc a) (suc b) = cong suc (
  begin
    a + suc b
  ≡⟨ shift a b ⟩
    suc (a + b)
  ≡⟨ +comm-proof  (suc a) b ⟩
    b + suc a
  ∎
  )
  where
  shift : (a b :)  a + suc b ≡ suc a + b
  shift zero b = refl
  shift (suc a) b = cong suc (shift a b)

distributive-lemma : Set
distributive-lemma = (a b c :)  a * (b + c) ≡ a * b + a * c

distributive-proof : distributive-lemma
distributive-proof zero b c = refl
distributive-proof (suc a) b c =
  begin
    b + c + a * (b + c)
  ≡⟨ cong (_+_ (b + c)) (distributive-proof a b c)⟩
    b + c + (a * b + a * c)
  ≡⟨ +assoc-proof b c (a * b + a * c) ⟩
    b + (c + (a * b + a * c))
  ≡⟨ cong (_+_ b) (sym (+assoc-proof c (a * b) (a * c)))⟩
    b + (c + a * b + a * c)
  ≡⟨ cong (_+_ b) (cong (λ { x  x + (a * c) }) (+comm-proof c (a * b))) ⟩
    b + (a * b + c + a * c)
  ≡⟨ cong (_+_ b) (+assoc-proof (a * b) c (a * c)) ⟩
    b + (a * b + (c + a * c))
  ≡⟨ sym (+assoc-proof b (a * b) (c + a * c)) ⟩
    b + a * b + (c + a * c)*assoc-lemma : Set
*assoc-lemma = (a b c :)  (a * b) * c ≡ a * (b * c)

*comm-lemma : Set
*comm-lemma = (a b :)  a * b ≡ b * a

*comm-proof : *comm-lemma
*comm-proof zero zero = refl
*comm-proof zero (suc b) = *comm-proof zero b
*comm-proof (suc a) zero = *comm-proof a zero
*comm-proof (suc a) (suc b) = cong suc (sub₁ a b)
  where
  sub₁ : (a b :)  b + a * suc b ≡ a + b * suc a
  sub₁ a b =
    begin
      b + a * suc b
    ≡⟨ cong (_+_ b) (*comm-proof a (suc b)) ⟩
      b + suc b * a
    ≡⟨ refl ⟩
      b + (a + b * a)
    ≡⟨ sym (+assoc-proof b a (b * a)) ⟩
      b + a + b * a
    ≡⟨ cong (λ { x  x + (b * a) }) (+comm-proof b a) ⟩
      a + b + b * a
    ≡⟨ +assoc-proof a b (b * a) ⟩
      a + (b + b * a)
    ≡⟨ cong (_+_ a) (cong (_+_ b) (*comm-proof b a)) ⟩
      a + (b + a * b)
    ≡⟨ refl ⟩
      a + suc a * b
    ≡⟨ cong (_+_ a) (*comm-proof (suc a) b) ⟩
      a + b * suc a
    ∎

*assoc-proof : *assoc-lemma
*assoc-proof zero b c = refl
*assoc-proof (suc a) b c =
  begin
    (suc a) * b * c
  ≡⟨ refl ⟩
    (b + a * b) * c
  ≡⟨ *comm-proof (b + a * b) c ⟩
    c * (b + a * b)
  ≡⟨ distributive-proof c b (a * b) ⟩
    c * b + c * (a * b)
  ≡⟨ cong (λ { x  x + (c * (a * b)) }) (*comm-proof c b) ⟩
    b * c + c * (a * b)
  ≡⟨ cong (_+_ (b * c)) (sym (*assoc-proof c a b)) ⟩
    b * c + (c * a) * b
  ≡⟨ cong (_+_ (b * c)) (cong (λ { x  x * b }) (*comm-proof c a)) ⟩
    b * c + (a * c) * b
  ≡⟨ cong (_+_ (b * c)) (*assoc-proof a c b) ⟩
    b * c + a * (c * b)
  ≡⟨ cong (_+_ (b * c)) (cong (_*_ a) (*comm-proof c b)) ⟩
    b * c + a * (b * c)
  ≡⟨ refl ⟩
    (suc a) * (b * c)

JSにもコンパイルできる.どんな感じになるのか見てみる.

module js-test where

test : {a : Set}  a  a
test x = x

open import Data.Nat

test₂ : ℕ
test₂ x = x + 1

agda --js  js-test.agda

使っているライブラリの分の.jsファイルがめちゃくちゃ生成される.js-testモジュールのコードはこんな感じ

var agdaRTS = require("agda-rts");

var z_jAgda_Agda_Primitive = require("jAgda.Agda.Primitive");
var z_jAgda_Data_Nat = require("jAgda.Data.Nat");

exports["test"] = a => a;
exports["test₂"] = a => agdaRTS.uprimIntegerPlus(agdaRTS.primIntegerFromString("1"),a);

わかりやすいですね.パターンマッチをしてみます.

test₃ : ℕ
test₃ zero = 0
test₃ (suc x) = suc (test₃ x)

ただの恒等関数です.結果

exports["test₃"] = a => (
  agdaRTS.uprimIntegerEqual(agdaRTS.primIntegerFromString("0"),a)? agdaRTS.primIntegerFromString("0"): agdaRTS.uprimIntegerPlus(
    agdaRTS.primIntegerFromString("1"),
    exports["test₃"](
      agdaRTS.uprimIntegerMinus(a,agdaRTS.primIntegerFromString("1"))
  ) )
);

3項演算子で分けていくようです.

バンドルしてブラウザで読み込んでみたい.
コマンド

npm init --yes
npm install -D esbuild

esbuild.js

require('esbuild').build({
  entryPoints: ['out/jAgda.src.Main.js'],
  bundle: true,
  outfile: 'public/index.js',
  minify: true,
  sourcemap: false,
  target: ['chrome70'],
}).catch(() => process.exit(1))

src/Main.agda

module src.Main where

open import Agda.Builtin.IO
open import Data.Unit
open import Data.String

postulate
  log : String  IO ⊤

{-# COMPILE JS log = (str) => () => console.log(str) #-}

main : IO ⊤
main = log "JS TEST"

コマンド

agda --js ./src/Main.agda --compile-dir=./out

Agdaが生成する.jsファイルでは,require(./XXX.js)じゃなくてrequire(XXX.js)と書かれているのでesbuildでは解決できない.
VSCodeの一斉置換機能とかで,require("require("./に置換する(嫌な操作!)

コマンド

 node esbuild.js

public/index.html

<!DOCTYPE html>
<html>
    <head>
        <title>JS Test</title>
        <script async="" type="text/javascript" src="index.js"></script>
    </head>
</html>

index.htmlをChromeで開いてみる.

結果

JS TEST

キタ

scriptの整理

  "scripts": {
    "test": "echo \"Error: no test specified\" && exit 1",

    "build:replace-require": "cd out && sed -i 's/require(\\\"jAgda/require(\\\".\\/jAgda/gI' *.js && sed -i 's/require(\\\"agda-rts\"/require(\\\".\\/agda-rts\\\"/gI' *.js && cd -",
    "build:agda": "agda --js --js-optimize --js-minify ./src/Main.agda --compile-dir=./out",
    "build":"npm run build:agda && npm run build:replace-require",

    "bundle:esbuild": "node esbuild.js",
    "bundle": "npm run build && npm run bundle:esbuild"
  },

やっぱり置換コマンドが頭悪い.WebPackなら回避できそうか

仮想DOMにアクセスしちゃおう!変更したところは以下


package.json

...

  "scripts": {
    "test": "echo \"Error: no test specified\" && exit 1",
    "build:replace-require": "cd out && sed -i 's/require(\\\"jAgda/require(\\\".\\/jAgda/gI' *.js && sed -i 's/require(\\\"agda-rts\"/require(\\\".\\/agda-rts\\\"/gI' *.js && cd -",
    "build:agda": "cd src && agda --js --js-optimize --js-minify ./Main.agda --compile-dir=./../out && cd -",
    "build": "npm run build:agda && npm run build:replace-require",
    "bundle:esbuild": "node esbuild.js",
    "bundle": "npm run build && npm run bundle:esbuild"
  },

...

esbuild.js

require('esbuild').build({
  entryPoints: ['out/jAgda.Main.js'],
  bundle: true,
  outfile: 'public/index.js',
  minify: true,
  sourcemap: false,
  target: ['chrome70'],
}).catch(() => process.exit(1))


src/Main.agda

module Main where

open import Agda.Builtin.IO
open import Data.Unit
open import Data.String
open import Web.Maquette

postulate
  log : String  IO ⊤
  _>>_ : {A B : Set}  IO A  IO B  IO B

{-# COMPILE JS log = (str) => () => console.log(str) #-}
{-# COMPILE JS _>>_ = () => () => (io1) => (io2) => () => {
  io1();
  io2();
} #-}

main : IO ⊤
main = (log "JS TEST") >> render


src/Web/Maquette.agda

module Web.Maquette where

open import Agda.Builtin.IO
open import Data.Unit

postulate
  render : IO ⊤

{-# COMPILE JS render = () => {
  const maquette = require('maquette');

  const h = maquette.h;

  function renderMain(){
    return h("body", ["Hello, World"]);
  }

  const projector = maquette.createProjector();

  projector.merge(document.body, renderMain);
}
#-}


コマンド

npm install maquette -D
npm run bundle

できた

ログインするとコメントできます