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ではあるが