Closed16
Agda やるぞ
ゆきくらげインストールしてみる
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を使いたい．
調べたところ拡張機能があるようなので利用させてもらう．
hello
最初のプログラム
Haskellと違って型は:で指定するようだ．
putStrLnなどはHaskellからFFIとして導入するみたい．
実行
agda --compile hello-world.agda
./hello-world
結果
Hello world!
いいですね
ゆきくらげdata Greeting : Set where
hello : Greeting
のSetはなんだろう カインドっぽいけどわからない
ゆきくらげ
依存型を使ったVectorの例
型チェックしたらData.Natがないって怒られた．標準ライブラリのインストールを忘れていた．
に従って手動でインストールした．パッケージマネージャ欲しい……欲しくない？
インストール後に型チェックを走らせたら通った いいね
コードに関しては，型定義はHaskellのGATsみたいな感じ．
open importはqualifiedがついていない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は依存型のパラメーターとして導入されている
ゆきくらげ例として
ゆきくらげ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
できた
このスクラップは2022/10/21にクローズされました