プログラミング関連 konn-san.com

記事一覧

VSCode で YaTeX のイメージ補完やユニコード数式記号を入力する為の拡張をつくった - 2018/11/17 03:54:00 JST

VSCode で YaTeX のイメージ補完相当の機能を実現したり、Agda や Lean などの定理証明系で必要となるユニコード数式記号の入力を補助するための機能拡張を作った話しです。

Emacs から Visual Studio Code に乗り換える作業のメモ - 2018/10/16 00:05:00 JST

Emacs にそろそろ辟易してきたので、VSCode に乗り換えようとしています。その作業記録。

Haskellerの私的Rustチートシート - 2018/08/29 18:47:20 JST

Rustに入門したので、適宜HaskellのこれはRustのこれ、ということをここに蓄積していって、個人的なチートシートにする。

欲望の赴くままRustで型レベルPeano自然数とサイズ付きベクトルを書いた - 2018/08/29 18:45:17 JST

あるていど強い型システムを持った言語を見ると、型レベルペアノ自然数とサイズ付きベクトルを書きたくなる、というのは人類普遍の欲求だと思います。 という訳で欲求に忠実であることとし、型レベルPeano自然数とサイズ付きベクトルRustで実装しました。実用性？皆無です。

zsh hooks を使って ssh / mosh の接続先によって Terminal.app のテーマを変える - 2015/08/04 00:00:00 JST

この記事はQiitaからの移行記事です。情報は古いので、記録以上の価値はありません。

latexmk で楽々 TeX タイプセットの薦め（＆ biblatex+biberで先進的な参考文献処理） - 2015/01/06 23:48:54 JST

TeX ファイルの変更を監視して、必要な回数だけ自動タイプセットしてくれる latexmk の紹介です。OMake はもう古い。あとbibtexの代替である biber と biblatex についても紹介。

Haskell ではじめるふわとろ Cocoa アプリ開発 - 2014/12/29 23:27:30 JST

Haskell による Cocoa アプリ開発の実際についての記事。Haskell Advent Calendar 2014 参加記事です。

定理証明系 Haskell - 2013/12/20 00:00:00 JST

Haskell Advent Calendar 2013 および Theorem Prover Advent Calendar 2013 参加記事。Haskell における依存型プログラミングおよび定理証明について解説した数少ない日本語文献です。C85 の TCUG に寄稿させて頂いた Haskell で定理証明を行う記事の販促記事でもあります。

Extensible Effects はモナド変換子に対する救世主になり得るか？ - 2013/07/21 21:26:00 JST

Oleg らによる、モナド変換子に対する大体手法、Extensible Effects の論文を読んだ感想紹介記事です。

絶対に理解出来ないモナドチュートリアル - 2013/06/28 02:04:09 JST

絶対に理解出来ないモナドチュートリアルです。

Haskell で Gentzen の LK - 2012/05/24 00:00:00 JST

この記事はQiitaからの移転記事です。 大昔に書いた、シーケント計算をHaskellの型システムを使って上手くエンコードした実装の記事ですが、正直何も整理されていないので、記録以上の意味はありません。

プロジェクト関連

computational-algebra

Haskellの先進的な機能をフルに使って実装された計算代数ライブラリ。

MathChrome

mimetex や Google Chart で書かれた数式を MathJax を用いて描画するようにする Google Chrome 拡張機能。.crx をダウンロードしたら、拡張機能ウインドウを開いてドラッグ・アンド・ドロップすれば使えます。

外部リンク

大抵のものは外部にある感じです。

GitHub

プロジェクトは主にここでホストしている。gist にも割と面白いコードが転がっている筈。ここで管理している主要なソフトウェアは以下の通り。

• Yablog - Yesod で書かれた blog エンジン。これは圏です はこれで動いている。
• gitolist - Yesod で書かれた Git Web Front-end。余りまだ機能がない。
• algebra - Gröbner 基底などの代数計算用のライブラリ。
• yesod-auth-oauth - ウェブフレームワーク Yesod の OAuth 認証プラグイン
• authenticate-oauth - http-conduit を使って OAuth API を叩くためのライブラリ。
• lk-proof-assistant - LK での証明をアシストして、結果の証明図を LaTeX で出力してくれる子。色々実験的な機能を使っているけどやや buggy。解説記事。

Qiita

Qiita に登録しているけど、最近はあまり使ってない。

これは圏です

ブログ。技術記事はここに集めてある。

デモ系

有限オートマトン・シミュレータ

Haskell で書かれたオートマトン・シミュレータ。Haskell から JavaScript へとコンパイルしてくれる Fay というものがあり、そのデモ。詳しい解説記事。

過去の遺産

中高時代に開発していた過去の遺物。あの頃は Ruby を使っていたので Ruby 1.8 製。今も動くかは知らん。

• WereWolf - Ruby 製の汎用人狼系ゲームエンジン、らしい。
• rupircd - リレーしない IRC サーバ。上のと組み合わせて、人狼が組み込まれている IRC サーバを作ろうとしていたがその目的は忘れ去られた。今は GitHub を見た方がまだいい。
• 偽音 - IRC 人狼bot。今あるのかはしらないがむかし人狼 BBS と云うものが流行って、IRC 上でも人狼をしたいと云う人達がいた。IRC人狼には真音（マロン）という bot があって、それは CHOCOA とかじゃないと動かなかったのでクローンを作った。上の WereWolf を使って書かれている。UO人狼のルールとかも実装してたんじゃなかったかなぁ。

いずれも古い Ruby 環境で作られたものなので今も動くかは知らない。多分動かない。