Undecided

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 に書いてあります。ここは公式ページではなさそうなのですけど。詳しくは公式ページ...

だいぶ前にCygwin版EmacsからWindows版Haskellで動いているAgdaを使おうとして File is missing: Searching for program, No such file or directory, /bin/bash というエラーが出て動かないので諦めていました。 もう一つ、Windows版Emacsをコマンドプロンプトから動かすと C:\Users\kurok\AppData\Roaming\.emacs を読んで起動するのに、CygwinからrunemacsでWindows版Emacsを起動するとエラーが出るのにも悩まされていました。前者の .emacs と同じ内容の init.el を読み込んでもです。 普段はVimを使っているので、「じゃあ、Windows版のEmacsをCygwinを経由させないで動かせばいいじゃない」で解決していました。でも、本格的にAgdaをやってみようと思ったら、フォントが足りなかったり、Agdaの標準ライブラリの設定が必要になったりで、 AppData の下に設定ファイルがあるのはめんどくさくなりました。設定ファイルはいつものCygwinのHOMEに集めたいです。ということで、エラーの原因を探ってみることにしました。 Cygwin経由だと $HOME/.emacs.d/init.el を読みにいくので、 AppData の下の .emacs をコピーしてきて余計なところを削ってみたのですが同じエラーになります。 (load-file (let ((coding-system-for-read 'utf-8)) (shell-command-to-string "agda-mode locate"))) /bin/bash が無いとのことなので、PATHの問題だと思いました。なので、Cygwin関係のパスを削ってみました。 PATH=`echo $PATH | sed 's/~\/bin//g;s/\/usr\/local\/bin//;s/\/usr\/bin//'` runemacs しかし、同じエラーが出る。 /bin/bash が問題なんだから shell-command-to-string ...

Windows版HaskellをCygwinから使っていて文字コードでトラブったので、その備忘録です。 きっかけは main = putStrLn "ℕ" が a.hs: <stdout>: commitBuffer: invalid argument (invalid character) というエラーを吐いたことです。"ℕ"じゃなくて"あ"なら出るんです。 ここで「なんだ、Haskellはユニコードをまともに扱えないのか」と思ってしまいました。ユニコード使いまくりの自作言語を作ってみたかったので「じゃあRubyでやるか」となったのですが、Raccでもℕが期待通りに動かなかったので、もう一度Haskellで試してみることにしました。 unicode-show をcabalから入れて、 uprint を試すも、特に変化なし。 {-# LANGUAGE UnicodeSyntax #-} を付けてみるも変化なし。 setLocaleEncoding utf8 を試すとエラーは出なくなるけど文字化けする。 ここで import GHC.IO.Encoding main = do getLocaleEncoding >>= print の結果が CP932 でした！！！ 「えっ？なんで？だってCygwinのターミナルはutf-8のはずでは？だったら"あ"とかも出ないはずでは？」と思いぐぐってみると 20190222: Cygwin - ターミナルエミュレータと文字化け というページがありました。 どうやら、conhostというのが勝手に変換しているようなのです！そして、パイプでつなぐと最後のコマンドの文字コードが変換の根拠になるもよう。ということで、 utf-8.hs import GHC.IO.Encoding main = do setLocaleEncoding utf8 getLocaleEncoding >>= print putStrLn "あいうえおℕ" を runghc utf-8.hs | cat で実行したら正常に出た！！！ どうやら、最初の例でエラーになったのはc...

てきとうにぐぐって、なんとなく分かりかけてきたので、簡単なまとめです。 いろいろな分野でモナドと呼ばれるものがありますが、Haskellではただの型クラスです。do記法があるという点以外は特別扱いされていません。do記法はただの糖衣構文なのでモナドの扱いを便利に書けるだけです。 定義は以下のようになっています。 Prelude> :i Monad type Monad :: (* -> *) -> Constraint class Applicative m => Monad m where (>>=) :: m a -> (a -> m b) -> m b (>>) :: m a -> m b -> m b return :: a -> m a {-# MINIMAL (>>=) #-} -- Defined in ‘GHC.Base’ instance Monad (Either e) -- Defined in ‘Data.Either’ instance Monad [] -- Defined in ‘GHC.Base’ instance Monad Maybe -- Defined in ‘GHC.Base’ instance Monad IO -- Defined in ‘GHC.Base’ instance Monad ((->) r) -- Defined in ‘GHC.Base’ instance (Monoid a, Monoid b, Monoid c) => Monad ((,,,) a b c) -- Defined in ‘GHC.Base’ instance (Monoid a, Monoid b) => Monad ((,,) a b) -- Defined in ‘GHC.Base’ instance Monoid a => Monad ((,) a) -- Defined in ‘GHC.Base’ Haskellでは型クラスの実装に型以外の制約は付けられませんから、モナド則に従わない実装も可能です。つまり、HaskellではMonadのInstanceではあるが...

黒板太字というのはℕみたいなやつです。ただ、それを入力したかっただけなんです。ついでに各種記号も。なのにとても大変だった。ということで、あとで絶対忘れるやつなので備忘録です。 最初はMS-IMEを使っていました。Windowsの標準のやつです。これで記号を入力するには「きごう」で変換するか、記号の名前を入れるかです。でも、どちらもだめっぽい。 ならば辞書登録です。なんという読みにしましょうか？長いのはめんどうです。Agdaだと \bN で入力できるんですよね。黒板太字はそのままBlackboard bold lettersなので。小文字もあるみたいなので、大文字を bN 、小文字を bn で登録しておけば便利そうです。 さっそく登録してみるけど、動きがよくわからない。もうちょっとまとめて登録して動きを観察したいけどめんどくさい。テキストファイルからまとめて登録できるみたいなのでチャレンジ。でもフォーマットがわからない。エクスポートしてみるも、文字化けしている。ぐぐってみると、どうやらutf-16leでタブ区切りのようです。Vimの設定が足りなくて文字コードを認識できない模様。 set fileencodings=ucs-bom,utf-16le,utf-8,iso-2022-jp,cp932,euc-jp,default,latin としてみたら開けた。わーい。でも、念のためutf-8のファイルを開いてみたら文字化け。 utf-16le を utf-8 の後ろに持っていったら両方開けました。そもそも、このエクスポートしたファイルはBOM付きみたいなので、 utf-16le の記述自体がいらないのではと思って削除してみたら両方とも開けた。これにて一件落着。 辞書ファイルが作れたのでさっそく登録してみるも、なんだか思ったように動かない。出てこないわけではないのだけれど、登録したはずのものが全部は出てこない。 bN と後ろにスペースを付けると ℕ とスペース付きで変換はできるみたい。でも、毎回そんな手間がかかるのは我慢なりません。 他の登録手段として、「えぬ」で変換とか、NICOLA配列で使っているのでbaと押したときに出てくる「へう」とかを考えたのですが、なんだか違う感じがします。他の手段も考えたのだけどなにも思いつかない。MS-IMEが半角英数間接入力が...

ToDoリストが増えすぎて管理できていません。前は目的別にToDoリスト管理アプリを使い分けていたのですが、アプリだと記録が残せないのでやめました。テキストで管理しておけばスクリプトでなんでもできますから。なので現在はLiquidLogicとVimです。 実態は優先度の低いToDoだけどアプリは別になっていることも多いStreak管理アプリも前は使っていました。Productiveというのを買って使ってみたんですが、デザインや機能が突然変わったりして使いづらかったです。やはりテキストが最高です。 テキストは自由でよいのですが、自由であるが故にファイルを作りすぎてしまいました。コンピュータに関するメモをcomp/memo.txtの様に書いてみたり、memo/comp.txtの様にしてみたり、雑多なメモをmemo/memo.txtに書いたり、メモについての考察をmemo/memo.mdに書いたりで、それはもうぐちゃぐちゃになりました。名前の付け方として「そのファイルについての場合」と「そのファイルの内容についての場合」があるんですね。そこら辺を意識せずに名前を付けたのは失敗でした。 こうなってしまったのは、とりあえず新規のファイルに書いて、どこに保存するかのポリシーがないのでてきとうに保存してきた結果です。「後で整理すればいいや」と思ったんですが、整理なんかしないんですよね。このブログを書きながら整理していますが、重い腰を上げるのが大変でした。 後で整理するからと、そのときいちばん簡単にメモできる関係の無いファイルに書いてそのままのケースも多かったです。でもLiquidLogicで書こうとタブの一覧表示、タブの選択、最後尾に移動とやっている間に書くことを忘れるのも確かに多いので、とりあえずすぐに書いて、その後にテキストの移動みたいな手順は合理的なんですけどね。 今あるリストと目的は Todoist 家賃の振り込みとかの定期的なものを書いています。でも、実際には「すぐにやって消えるはず」という理屈ですぐやるべきことも書いています。ですが、やらないんですよね。だからどんどん溜まっていって、家賃とかの重要なものが埋もれてしまって、上手に管理できていません。 日記 「やること todo」の形式でその日から数日で処理する予定のものを書いています。他の形式は「買...

Haskellではデータは全て型を持っています。この型のことを代数的データ型と言います。Int, Integer, Float, Doubleなどがあります。 変数は a :: Int a = 3 のように定義します。関数は add :: Int -> Int -> Int add x y = x + y のように定義します。これはaddという関数は引数xとyをとり、x + yの結果を返すことを意味します。型は一番左のIntが最初の引数xの型、2番目のIntが2番目の引数yの型、最後のIntが戻り値の型です。変数と関数が同じ名前空間に束縛されるので変数と関数に同じ名前は使えません。 新しい代数的データ型は既存の代数的データ型を組み合わせて data Figure = Triangle { base :: Double, height ::Double } のように定義します。Figureは型の名前で、これをタイプコンストラクタと言います。Triangleはデータの名前で、これをデータコンストラクタと言います。base :: Doubleはbaseというラベルを持つDouble型のフィールドです。名前が必要なければ data Figure = Triangle Double Double と書けます。代数的データ型は複数のデータコンストラクタを持つことができて data Figure = Triangle Double Double | Rectangle Double Double | Circle Double のように書けます。これはFigure型はTriangle、Rectangle、Circleのいずれかのデータを持つことを意味します。データはフィールドが無くても構いません。その場合は data Bool = True | False のようになります。この場合、フィールドを持たないデータコンストラクタTrueとFalseができることになります。 型変数を持つ代数的データ型は data Maybe a = Nothing | Just a のように書けます。使うときにaに具体...