Agda始めました

Agdaを始めました。Windows 10でWindows版EmacsとWindows版のGHCupのCabalで入れたHaskellでやっています。最初にCygwin版のEmacsとWindows版のHaskellでやろうとしてできませんでした。前者の方法なら引っかかるところはなかったはずです。

Emacs以外にもVSCodeやNeovimでできるみたいです。でも、元々はEmacsで作られたみたいで、安定していそうなのでこれにしました。

「どこから手をつけるか？」ですがAgda公式ページのチュートリアルが一番丁寧そうです。でも、"Agda"でぐぐっても公式ページすら最初のほうに出てこないんですよね。本当に公式ページなのかもよくわかりませんし。"Agda tutorial"だと古いバージョンが引っかかる始末。なぜ、こんなことになっているのか？

公式ページの頭から読んでいくと"A Taste of Agda"がけっこう難しかったです。なので、ここは飛ばして次の"A List of Tutorials"の"Books on Agda"にある、"Programming Languages Foundations in Agda"をやるのが良い気がします。日本語のページだと違う気がしますが、英語のサイトだとBooksにあるやつはだいたいただでHTMLで読めますよね。どういうことなんでしょう？読めるならいいんですけど。

最初は自然数の定義からです。

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

で定義できます。

ℕは黒板太字というやつで、数学の世界では自然数を表わすことが多いようです。黒板太字を使えない環境ではNatと書くことが多いようです。他にはℤで整数、ℚで有理数、ℝで実数、ℂで複素数みたいです。EmacsのAgdaだと\bNで出せます。\bnだと小文字が出てきます。\->で→が出せます。でも、ここらへんはバージョン依存かも。他にもたくさんの記号があって、Agda Emacs Symbolsに書いてあります。ここは公式ページではなさそうなのですけど。詳しくは公式ページのHow can I write Unicode characters using Emacs?に書いてあります。

自然数の定義ですが、これらはHaskellに似た記法になっています。dataはデータ型を宣言する命令です。ℕを定義しています。Setはまだよくわかりませんが、zeroとsucの集合みたいなことでしょう。zeroはデータコンストラクタで型はℕです。sucはsuccessorの略でℕを引数にとってℕを返す関数になります。

自然数の定義の後に

{-# BUILTIN NATURAL ℕ #-}

を書いておくと2などの数字がsuc (suc zero)の代わりに使えるようになります。

チュートリアルでは次のコードでインポートすることになっています。

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

しかし、標準ライブラリがインストールされていないとエラーになります。

D:\home\sakura\docs\comp\lang\agda\test.agda:1,8-51
Failed to find source of module
Relation.Binary.PropositionalEquality in any of the following
locations:
  D:\home\sakura\docs\comp\lang\agda\Relation\Binary\PropositionalEquality.agda
  D:\home\sakura\docs\comp\lang\agda\Relation\Binary\PropositionalEquality.lagda
  C:\cabal\store\ghc-8.10.7\Agda-2.6.2.2-44283e0a92e767b3a6754f539efccb0afbc41964\share\lib\prim\Relation\Binary\PropositionalEquality.agda
  C:\cabal\store\ghc-8.10.7\Agda-2.6.2.2-44283e0a92e767b3a6754f539efccb0afbc41964\share\lib\prim\Relation\Binary\PropositionalEquality.lagda
when scope checking the declaration
  import Relation.Binary.PropositionalEquality as Eq

Agdaの公式ページには標準ライブラリへのリンクしかありませんが、書いてあるとおりでインストールできます。

まず、ダウンロードして展開します。そして展開したディレクトリでcabal installです。

kurok@DESKTOP-55E88RD /cygdrive/d/app/agda-stdlib-1.7.1
$ cabal install
Wrote tarball sdist to
D:\app\agda-stdlib-1.7.1\dist-newstyle\sdist\agda-stdlib-utils-1.7.1.tar.
gz
Resolving dependencies...
Build profile: -w ghc-8.10.7 -O1
In order, the following will be built (use -v for more details):
 - unix-compat-0.7 (lib) (requires download & build)
  - filemanip-0.3.6.3 (lib:filemanip) (requires download & build)
   - agda-stdlib-utils-1.7.1 (exe:GenerateEverything) (requires build)
    - agda-stdlib-utils-1.7.1 (exe:AllNonAsciiChars) (requires build)
    Downloading  unix-compat-0.7
    Downloaded   unix-compat-0.7
    Downloading  filemanip-0.3.6.3
    Starting     unix-compat-0.7 (lib)
    Downloaded   filemanip-0.3.6.3
    Building     unix-compat-0.7 (lib)
    Installing   unix-compat-0.7 (lib)
    Completed    unix-compat-0.7 (lib)
    Starting     filemanip-0.3.6.3 (all, legacy fallback)
    Building     filemanip-0.3.6.3 (all, legacy fallback)
    Installing   filemanip-0.3.6.3 (all, legacy fallback)
    Completed    filemanip-0.3.6.3 (all, legacy fallback)
    Starting     agda-stdlib-utils-1.7.1 (exe:AllNonAsciiChars)
    Starting     agda-stdlib-utils-1.7.1 (exe:GenerateEverything)
    Building     agda-stdlib-utils-1.7.1 (exe:GenerateEverything)
    Building     agda-stdlib-utils-1.7.1 (exe:AllNonAsciiChars)
    Installing   agda-stdlib-utils-1.7.1 (exe:GenerateEverything)
    Completed    agda-stdlib-utils-1.7.1 (exe:GenerateEverything)
    Installing   agda-stdlib-utils-1.7.1 (exe:AllNonAsciiChars)
    Completed    agda-stdlib-utils-1.7.1 (exe:AllNonAsciiChars)
    Copying 'AllNonAsciiChars.exe' to 'C:\cabal\bin\AllNonAsciiChars.exe'
    Copying 'GenerateEverything.exe' to 'C:\cabal\bin\GenerateEverything.exe'

AGDA_DIRはWindows版ではC:\Users\kurok\AppData\Roaming\agdaになります。agdaの前にドットは必要ありません。AGDA_DIRにlibrariesというファイル名で先程展開したstandard-library.agda-libへのパスを書きます。もう一つ、defaultsというファイル名でstandard-libraryと書きます。これで標準ライブラリが動くはずです。

もしかしたら正常に表示されないフォントがあるかもしれません。その場合は"DejaVu Sans Mono"か"Noto Sans Math"を指定すれば表示されるはずです。"Noto Sans Math"はインストールが必要です。

ここまで環境を作って、基礎が理解できれば、あとはチュートリアルを読んでいくだけのはずです。さあ、どんどん行きましょう。

コメント

コメントを投稿

このブログの人気の投稿

五十音配列付き新下駄配列

イメージ
keyboard layout editorデビューしました。ファイルが複数になると管理がめんどうなので、このブログの内容はSVGファイルに直接書いてますが、これでいいんだっけ？まあ、消えなければ後からなんとでもなるからいいか。 と思ったら、SVGは日本語に対応していないみたいです。しくしく。 レイアウトは新下駄配列に覚えやすい五十音配列を加えたものです。アルファベット自体をいじってますが、qtypをちょっと動かしただけです。bntyを親指で押すシステムなんですが、けっこう快適です。ErgoDox EZだと斜めになっているキーが親指に当たるので取ってしまっています。アルファベットの長押しに制御キーやレイヤーキーを割り当ててしまえば30%で十分なんですね。ほとんど手首を動かさずに入力できます。 日本語配列は新下駄配列の拗音以外はそのままなので、覚え直すことなく使えます。五十音部分は左手で行を指定して、右手で段か拗音を指定する方式です。新下駄配列で使用しているsdklはそのまま残してあるのでさ行、た行がありませんが、それは新下駄の方を使ってください。拗音は新下駄のものをそのまま使うこともできたのですが、左手で行を指定する方式なのを活かして、右手で拗音を指定する方式にしました。各行に拗音とくっつくのはひとつしかないんですね。不思議な感じです。 欠点はロールオーバーミスが起こりまくることです。「うんち」と入力しようとして「にち」になるようなことがよく起こります。新下駄配列でもsdklioがからむと起こるのですが、それ以外にもシフトキーを増やしたので大幅に起こりやすくなっています。そういう配列なのでそこはあきらめてください。スピードを犠牲にして脳の負荷を抑えた配列です。ただ、ローマ字テーブルからfj同時押しで「に」の項目を消してしまえばそうはならないので、いろいろカスタマイズできるかもしれません。この配列でスピードを目指すならステノワードのような方向になるでしょう。脳の負荷が増えてしまいますが。 良い点は、左手で行を指定する方式なので数字行にはみ出していたみゃ行等を30%の範囲に取り込めたことでしょうか。もう一つ、頻度の低い文字は五十音の方を使うことにすれば、空いた所にいろいろ突っ込めるところでしょうか。かなり気に入ってます。 ∨ Source mar...
続きを読む

WSLでの親指シフトはどうやらMozcで実現可能と気がつくまで

WindowsではAutoHotKeyを使って疑似親指シフトで日本語を入力しています。もともとかな打ちだったんですが、キーボードをErgoDox EZに変えたら「ろ」とかのキーが足りなくなって、どうしようか悩んで親指シフトを見つけてきました。疑似なのは同時押しではなくて、親指でファンクションキーを押しながらアルファベットキーを押すことで出しているからです。AutoHotKeyを使って同時押しを実現しているものがあるのは知っていますが、とりあえずNICOLA配列を試しつつ今まで引っ張ってきた感じです。 Windowsではそれで満足していたのですが、WSLを使うようになって困りました。AutoHotKey(以下AHK)ではIMEの状態を取ってきてオンの場合には出力を変えているのですが、WSLだとAutoHotKeyからMozcの情報を取ってこられる気がしません。WSL側で検知してWindows側から読める位置にファイルを置くような、トリッキーな方法を使えばできなくはないような気もしますが、そこまでしてAHKに頼るのも変な感じです。 ということで、WSL側で親指シフトを使えるようにしようとぐぐって出てきたのは oyainput というやつでした。しかし、これがWSLでは動かない。エラーコードから察するに、 /proc/bus/input/devices が空なのでキーボードの情報が取れないのでだめみたいです。まあ、WSLですし。 しかたがないので、今度はWSLのEmacsでWindows側のIMEが使えるという「 emacs-mozc を動かすための設定（WSL 設定編） 」のmozc_emacs_helperというのを試してみました。で、苦労して動かしてみたものの、Windows側の辞書を使って変換はしているようですが、AHKがIMEの状態を把握できないので親指シフトモードに切り替わらないのは同じでした。残念。 いったんは諦めてMinGW版のEmacsを使うことにしたのですが、ぐぐってみたら「 [Question] Possible to (properly) implement simultaneous (custom) Kana-input layout? #512 」というMozcに新下駄配列を実装する話が出てきました。 新下駄配列は知らなかったのでぐぐ...
続きを読む

親指シフト新下駄配列の可能性

Google日本語入力の「シフトキーでの入力切り替え」をオフにして、ローマ字テーブルに大文字で登録すると、登録されたとおりに出力されます。当たり前ですが。これで「L」に「l」とは別に「じ」や「しかし、」や「𝕏」を割り当てることができます。 NICOLAなどの親指シフトとは違って、たんに大文字かどうかを見ているだけなのでシフトキーの左右を区別はできませんが、いろいろな使い方が考えられそうです。例えば、「X」に「𝕏」を割り当てるとか、「A」に「∀」とか。「L」に「しかし、」とかの接続詞を割り当てて入力時間の短縮もできるかもしれません。「L」に「じ」を割り当てて、「じ」に割り当てられている場所に別の文字なども考えられそうです。左右を混ぜて、シフトキーを押している間だけ全く別のマップでアルペジオとかも考えられます。覚えるのが大変ですけど。数字キーに割り当てられている文字をアルファベットに割り当てれば40%キーボードでも3点押しなしに入力することもできます。 このように、いろいろな可能性がありますが、実はまだ使っていません。まだ新下駄配列に慣れていないので、それどころじゃないんですよね。まずは新下駄配列に慣れて、その中で困ったことが起きたら解決に使う感じかな？
続きを読む