Just $ A sandbox

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

MonadPlusとNearSemiringで反例探し

"MonadPlusは単なる自己関手の圏における近半環だよ。何か問題でも" の理解を試みる - scalaとか・・・d.hatena.ne.jp 上の記事を読んでちょっと考えたこととかをまとめる. NearSemiringとは和についてモノイド, 積について半群で, 0が左吸収元で…

Haskellで大富豪を作ろう (5)勝敗の判定をしよう

前回までの記事 Haskellで大富豪を作ろう (1)トランプを用意しカードを配ろう - Just $ A sandbox Haskellで大富豪を作ろう (2)ターンを進めよう - Just $ A sandbox Haskellで大富豪を作ろう (3)カードの組を判定しよう - Just $ A sandbox Haskellで大富豪…

Haskellで大富豪を作ろう (4)基本のルールと場の流れを作ろう

前回までの記事 Haskellで大富豪を作ろう (1)トランプを用意しカードを配ろう - Just $ A sandbox Haskellで大富豪を作ろう (2)ターンを進めよう - Just $ A sandbox Haskellで大富豪を作ろう (3)カードの組を判定しよう - Just $ A sandbox 第四回 基本のル…

Haskellで大富豪を作ろう (2)ターンを進めよう

前回までの記事 Haskellで大富豪を作ろう (1)トランプを用意しカードを配ろう - Just $ A sandbox 第ニ回 ターンを進めよう 実際にゲームとして動かすために, まずはいわゆるメインループにあたる部分を作ろう. ゲームに必要な変数をGame型として定義してお…

Haskellで大富豪を作ろう (1)トランプを用意しカードを配ろう

まえがき Haskellでなんか動くものを作ろうと思った. 規模と知名度等を考えて大富豪あたりが妥当なところかと思ったので, 今回はCUIの大富豪を作ろうということにした*1. コード自体は完成しているので, 何回かに記事を分けて説明をつけて投稿していくつもり…

Haskellで大富豪を作ろう (3)カードの組を判定しよう

前回までの記事 Haskellで大富豪を作ろう (1)トランプを用意しカードを配ろう - Just $ A sandbox Haskellで大富豪を作ろう (2)ターンを進めよう - Just $ A sandbox 第三回 カードの組を判定しよう 前回はカードを捨てられるようになったので, 次は同じ数字…

Lens from Scratch

久しぶりのLensの記事です. 5億回は繰り返されてきたであろうLens再実装を通して, Lens, Getter, Setter, Iso, Equality, Traversal, Prism, Foldの仕組みを理解するのが目的です. 亜Lens family Getter Getterは基本的にはConstをかぶせる操作とそれを剥が…

無限ループによる証明

Software FoundationsのIMPあたりをやってて疑問が湧いた. w = while True do Skip endが停止しないことを示したい. つまり, $\langle w, s \rangle \to s' \Rightarrow False$ を示したい. ($s, s' : \mathbb{Z} \to \mathbb{Z}$ は変数の値を保持する環境)…

de Bruijn Indexとβ変換

$ KMN \equiv (\lambda xy. x)MN \longrightarrow_{\beta} M $を示したいとする. α変換 $y \notin \text{FV}(M)$ならば, $ (\lambda xy. x)MN \to (\lambda y. M) N \to M[y:=N] \equiv M $となる. 問題は$y \notin \text{FV}(M)$ならば$ M[y:=N] \equiv M $…

原始帰納的函数で素数を計算

原始帰納的函数; prf 原始帰納的函数(primitive recursive function; prf)とは, 以下で定義される函数 $ \mathbb{N}^n \to \mathbb{N} $ のこと: 定数函数 $zero : \mathbb{N}^0 \to \mathbb{N}$, 後続函数 $suc : \mathbb{N} \to \mathbb{N}$, 射影函数 $p^…

戦略を予約しておくRPGの戦闘システムについて(アイデア)

概要 RPGの戦闘システムとして考えたやつ。戦闘は普通のターン制。各ターンに1つのアクションが取れる(攻撃・防御・回復 など)。 プレイヤーは戦闘の前に、アクションを並べて作った列をスロットという形で保存しておく。 敵との戦闘時、プレイヤーの作った…

DataKindsとGADTの使い方について

Haskellで型レベルプログラミング(あるいはごく簡単な証明)を書くときに, DataKindsでデータ型をそのまま持ち上げると困る場面がある. {-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies #-} data a :=: b where Refl :: a :=: a data Nat = Zero…

ワンナイト人狼の基本戦略

ワンナイト人狼とは ワンナイト人狼は一夜で決着が着く人狼(ジャンルとしては多人数推理ゲーム)。 ワンナイト人狼のルール ゲームは3~5人向けだが、今回は4人でプレイするとして解説をする。 初めに6枚のカードを用意する。 内訳は「人狼2枚、村人2枚、占い…

Linuxで音声読み上げ

ゆっくりしていってね! 棒読みちゃん http://chi.usamimi.info/Program/Application/BouyomiChan/ 環境はwine 1.6.2, Bouyomichan 0.1.11.0 (beta 16) wineを32bit環境で動かすことと、.NET framworkをwinetricksで入れておくこと mscoree.dllに関するエラ…

Grothendieck群とBurnside環の定義

局所有限トポス上の離散数学の構築を目指して という論文で、Burnside環という環を扱っていた.定義は「局所有限トポスの同型類から得られるGrothendieck ring」らしく, これではよく分からなかったので調べた. Grothendieck群 Grothendieck群は可換モノイド…

美少女と学ぶ圏論(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)とは、コンピュータ等の計算機を用いた自然言語処理の基礎技術のひとつ。かな漢字変換等にも応用されている。対象言語…