読者です 読者をやめる 読者になる 読者になる

Just $ A sandbox

プログラミングと計算機科学とかわいさ

美少女と学ぶ圏論(2)

本来ならば図式を交えて説明するべきところを図式を用意していないので非常に分かりにくいです(特に証明の部分など). 自分で可換図式を書きながら議論を追って読まれることをおすすめします. 1.2 SpecialなObjectたち レポートをやるというのは話を切り上げ…

美少女と学ぶ圏論

ここまで書いて飽きました. 1章 圏とその構造 1.1 圏の定義と千景の講義 「4月からのゼミはもう決めた?」「うん. とりあえず,クラスの子とホモロジー代数ゼミをやろうと思ってるよ. 春休みのうちに予習を進めないと」「ふぅん,ホモロジー代数ね」 千景は読…

objective覚書

objective-0.6.1 O' = data Object e m = forall x. e x -> m (x, Object e m) = hom(e, m . (-,O')) (as Nat) functor Kを用いてe = hom(a,K-) = forall x. a -> K xと書けるとき(Data.Functor.Kan.Ranを見よ) O' = hom(hom(a,K-), m . (-,O')) = hom(K^-1(…

Codensity Monad

Codensity という型がある. 定義は以下. newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b } instance Functor (Codensity k) where fmap f (Codensity m) = Codensity (\k -> m (k . f)) instance Monad (Codensity f) wh…

Agdaで集合論をやろうとして上手く行かなかった

この前の記事の方針でゴリゴリ公理を追加していたら, 問題が発生した. 写像の定義を _⟶_ A B = ∀ x → x ∈ A → ∃ \y → y ∈ B としたら, (これはとても自然な定義に見えるけれど)例えば A ≡ B から f(A) ≡ f(B) が導けなくなる. x ∈ A を像の方に押し込めて _⟶…

矛盾の証明

矛盾を示すときに使える方法としては主に以下の2つだと思う 命題 ¬P に P をぶつける 矛盾 ⊥ の特徴付けを使う 矛盾の特徴付けというのは, 例えばAgdaだと⊥は空集合の公理を満たすことが示せるから, 空集合の公理がそのまま矛盾の特徴付けになる. ∃ \(A : Se…

Classical set theory in Agda

Agda歴2週間くらいのザコです。 Agdaで圏論のライブラリを作って、流れで位相空間の定義をしようと思ったらそもそも集合を普通に扱えるライブラリがどこにもない。 標準ライブラリにRelation.Unaryとかいうのもあるけど、これは表面的には上手く行っているよ…

Printf実装を通して学ぶGADTs, DataKinds, ConstraintKinds, TypeFamilies

問題 問. Haskellで以下のようなCライクなprintf函数を実装してください。 > printf ["Hello, ", _s, "\n", "an integer:", _d, "\n", "a float:", _f] ["World!", (10 :: Int), (3.1415 :: Float)] -- 出力結果: > Hello, World! > an integer:10 > a float…

Haskellでもできる!実践・オブジェクト指向

Lensにほとんど触れたことのない人にはこちらの記事がオススメです:Lensで行こう! - Just $ A sandbox Haskellでもオブジェクト指向をしましょう! Haskellは直接オブジェクト指向的な機能を提供してはいませんが、我らがLensの力を借りることでオブジェク…

2ヶ月くらいでノベルゲームを作った話

発端 ノベルゲームやりたいし誰か作ろう— いるたん (@t_iru) 2013, 9月 8 【告知】フリーノベルゲーム「チェイン・コンプレックス」を公開しました。 http://t.co/JcLhaqfAKs http://t.co/3fJcNInJlj— いるたん (@t_iru) 2013, 11月 13 で2ヶ月くらいでノベ…

Ubuntuがdisk driveエラーで起動しない

Xubuntu 13.10で以下のようなエラーが出て起動できませんでした。 The disk drive for /home is not ready yes or not present. 私のHDDのパーティションは以下のような感じになっています。 /dev/sda2 /dev/sda7 /dev/sda5 Windows7 /home / /homeに当たる/…

LinuxでWindowsアプリケーションを動かしたい人のためのWineの設定

この記事はwineに関して私が蓄積したベストプラクティスとバッドノウハウをまとめたものです。 Wineとは Wineとは、Linuxで*1Windowsアプリケーションが動くエミュレータではない何か*2です。 はじめに、Wineで全てのWindowsアプリが動くわけではないことを…

Pythonでsuper(self.__class__, self)は使うな

[追記:2013/11/02] この記事ではPython2.xを前提としていますが、Python3以降はsuperの引数を省略することができるようになっています。 [/追記] 次のPythonコードを見てください。 class A(object): def method(self): pass class B(A): def method(self): …

Python製のベストなオープンソースプロジェクト

Best written projects on Python GitHub? redditで面白いポストをみつけたので日本語で軽くまとめておきます。 http://www.reddit.com/r/Python/comments/1ls7vq/best_written_projects_on_python_github/ エレガントで上手に書かれていて読みやすく練習に…

lxmlチュートリアル翻訳してみた

PythonでXML(HTML)を扱う高速で便利なライブラリがlxmlです。 非常に強力なメソッドが多数用意されているのですが、日本語の情報があまりないのが弱点です。なので今回、lxml.etree公式チュートリアルの一部を勝手に翻訳しました。 量が多いので全ては訳しき…

ubuntuで音が出なくなった

ubuntuを使っていたら突然音が出なくなりました。 結論から言うとpulseaudioとflashplugin-nonfree-extrasoundをインストールしなおしただけです。 環境 OS: ubuntu 12.04 LTS 問題のあったGoogle Chrome: version 28 経緯 最近Google Chromeで``Shockwave F…

HaskellのMonadは何をしているか

はじめに:モナドが何かわからないけど分かりたい人へ この記事はあなたの為に書かれたものです! 「モナドって難しいそうだしよく分からない、けどきっと賢い人たちが『モナドとは何か』について素敵な説明を与えてくれるはず!」 …そういう期待を持ってい…

世界一わかりやすいモナドの記事

は環 はアーベル群 , として、 はAbel圏でモナドを定め、T-代数は左加群になる*1。 *1:これよりわかりやすい例があれば教えて下さい

Yoneda lemmaとOperational Monad

最近Haskellerの間で人気になりつつある(?)Operational Monadというものについての記事です。 サンプルプログラム Operational Monadは http://hackage.haskell.org/package/free-operational で定義されています。後でも説明しますがこれはFree Monadの構…

PSh圏とcolimit

PSh圏とcolimit 位相空間Xに対して、X上の前層Fとは、Xの開集合から集合への写像 (で、かつ制限写像というものが定められているものの)のことです(詳しくは層 (数学) - Wikipedia等を参照)。 ここで、に包含関係で順序を入れてこれを順序集合の圏(と表記)と…

テキストフォーマットが欲しいという話

Haskellで時々Formatがしたくなる時があります。 しかしこれと言って便利そうなものが見当たらず、自作しました。 myuon/FuncFormat · GitHub import Text.FuncFormatとすれば使えるようになります*1。 ほんの少しだけTemplateHaskellの闇魔術を利用している…

Yes, Yesod!

abstract: this article shows how to install and run Yesod, a famous Haskell web framework for its simplicity to use and its difficulty to install. I wrote how I did it for whoever wants to install Yesod, and for myself. Yesodのインストール…

ブログのスタイルを少し変更

はてなブログにはいくつかテーマが選択できて、個人的には2カラムのテーマが好きなので一番シンプルなEpicというテーマを使っています。 しかしこのテーマ、横幅が短すぎるのです。プログラム関係の記事が多いためコードをよく掲載するのですが、ちょっと長…

Ubuntu12.04で自己満足用LaTeX環境構築

LaTeX環境構築の話です。 Linuxだと最初から入ってるもの・入ってないからいれなきゃいけないもの(apt-getできるもの・install-elispできるもの・ソースから落としてビルドするもの)が混在しているためか環境構築はかなり面倒です(面倒でした)。 同じ思いを…

GAEで(Twitter APIを利用した)簡単webアプリ

webアプリとか書いてみたくなったのでGAEでちょっと何か作って見ることにしました。 と言ってもあまり難しいものを作る技術も時間的余裕も無いので、今回は"Twitterにログインし、与えられた文字列をツイートする"ことだけを行います。 もちろん、OAuth認証…

Free Monadを使ってみよう!(2)

前回の記事について 前回の記事では、Free MonadをFunctorの延長として捉え、Monad的な使い方ではなくFunctor的な使い方を中心にFree Monadについて見て見ました。 さて、上の記事は実際のところ、まだFree Monadの便利さの片面しか見えていないと言わざるを…

Lensで行こう!(2):Isoへの拡張

このエントリーはLensで行こう! - みょんさんの。の続編にあたります。 前回の復習 前回、Lens型について詳しく見ました。 Lens型は以下のような型のデータです。 type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t これはFuctorを上手く…

はてブの投稿てすてす

登録してみた はてブを最近やたら見るようになったので移行もワンチャンある気がしてきました。 というか、Markdownの誘惑に負けました、はい。 いやこれ便利ですよほんとに 細かい書式とかにあんまりこだわりたくない場合はこっちのほうが遥かに速いし、何…

Lensで行こう!

続編:Lensで行こう!(2):Isoへの拡張 - みょんさんの。 Lensとは Lens(http://hackage.haskell.org/package/lens-3.7.1.2)というパッケージがあります。 非常に大きなパッケージで、中には非常に便利な函数群がたくさん揃っています。私が調べた限りでは、 …

commitとpushしかできない人のためのgithubの使い方まとめ

github(というよりgit)使っている方は結構な数いらっしゃると思います。 私もそのうちの一人ですが、正直「addしてcommitしてpushするだけ」です、はい。 branchとかmergeとかfetchとかあの辺がいまいちわからない情弱です。あんまりこの辺をまとめて書いた…

Free Monadを使ってみよう!

続編:Free Monadを使ってみよう!(2) - みょんさんの。Haskell楽しいです。 Haskellは純粋なのでとても大好きです。 ただ、Haskellでは副作用のあるように見える(手続きっぽい)書き方をしたくなる時がどうしてもありますので、そういうところでは手続きっぽ…

最も素敵な言語とは?(函数型言語とは何なのか)

函数型言語とは何なのか 函数型言語、という名前くらいは皆さんご存知だと思いますが、しかし使ったことがない人は多いと思います。 入門書は山のように有りますが、「なぜ函数で記述するの?」ということが分からなければそれらを読み進めることも難しいと…

3.pythonで対話型AI制作[モジュール化]

前回以降の部分で最初に目標として設定していた、最低限の機能を備えた自律学習型AIの中核はほぼ完成しました。しかしまだコードが読みにくいので*1、モジュール化してみます。 という訳でモジュール化されたコードがコチラ!→https://github.com/myuon/AI/b…

可愛いは、測れる?

SNSのプロフィールなどを見ていてふと気がついたのですが、「可愛いプロフィール」というものが存在するとすれば、それは一体どういうものでしょうか? それは定量化できるものなのでしょうか?安易に考えればひらがなのような柔らかい文字列+記号の多用が可…

2.pythonで対話型AI制作[形態素解析]

形態素解析とは 形態素解析とはなんでしょうか?ちょっと調べてみましょう。 形態素解析(けいたいそかいせき、Morphological Analysis)とは、コンピュータ等の計算機を用いた自然言語処理の基礎技術のひとつ。かな漢字変換等にも応用されている。対象言語…

1.pythonで対話型AI制作[マルコフ連鎖]

マルコフ連鎖とは 今回から実際にAIを作っていきますが、最初はまずマルコフ連鎖というアルゴリズムでプログラムを書きます。 マルコフ連鎖は数学的なモデルも確立しているとても有名な過程なので詳しくは調べていただければ良いかと思います。ざっくばらん…

0.pythonで対話型AI制作

昔作っていたpythonによる対話型AI*1が出てきたこともあり、せっかくなのでここにまとめることにしました。 全ソースコードは私のgithubからダウンロード可能です(https://github.com/myuon/AI)。 ほしい方は右の真ん中より少し上にあるDownloadボタンからお…

1.Haskellで遺伝的プログラミング[ファイル入出力]

Haskellで遺伝的プログラムとか大仰なことを言いましたが私自身まだHaskellを使い始めたばかりで、初歩的な型エラーに何時間も悩むレベルです。 なので、まぁゆっくり少しずつ、悩みながら作っていきたいと思います(つまり遅いということです)。 ファイル入…

2.ショートコーディングC[コラッツ予想]

今回はコラッツ予想のショートコーディングをしてみましょう。コラッツ予想を知らない方はコチラ→コラッツの問題 - Wikipedia まずは愚直に 何も考えずに組んだプログラムが以下になります。 2から順に全ての数の、コラッツ予想の手順に沿って数を出力するプ…

0.Haskellで遺伝的プログラミング

Haskellで遺伝的プログラミングを組んでみることにしました。 そもそも「論理式は解の個数と判定時間が性質を与えているに違いない!*1」「プログラム的な手法(つまりはアルゴリズム)は多くの場合は限定論理式で書けるのではないか」「ではプログラムは自己…

みょんさんのTwitterの使い方について

ぼくのTwitterポリシー - くだらぬみちくさにっき ---- To waste one’s time on the road might be good, I think.でお見かけしたのでまぁ真似(パクリ)しようってだけです。 そういえば私はいろんな所にプロフィールあるけど結構雑に書いているのとそれのま…

1.ショートコーディングC[素数列]

今回は「素数列」のショートコードを書いてみましょう。 まずはそこそこ速いコードを 以下に、使い古された普通のCコードを書きます。 #include <stdio.h> #define N 100 int main(void){ int primes[N]; int i=1,n=3; int isPrime; int j; primes[0]=2; while(i</stdio.h>

0.ショートコーディングC

ショートコーディングとは? ショートコーディングとはその名の通り短くコードを書く、ということに重きをおいて行われるプログラミングです。 普通ではやらないような記法を使ってでも、1バイトでも短くなるようにコードを組みます。もちろんこれはかなり…