foldって難しくないですか - Just $ A sandbox
foldって難しい、というか書きづらくて読みづらくないですか、と思った話を書きます(そういう感じの話題でTLが盛り上がってたので) 以下、foldをrecursion schemeの観点から理解していることは前提とします foldをかく foldを書きたい foldを書こうと思う場合は自分の場合は明白で、可換monoid積で畳むときは必ずfoldで書きます sum = foldl (+) 0 これは入力と出力の型が一致していて細かいことを考えなくて良いし、何しているのか見れば分かるし、畳み込み感があっていい感じだし文句はない ただこういうのは得てしてすでに欲しい関数が定義されてたりする foldを書きたい？？ これがアキュムレータ付き再帰をしたい場合になると若干微妙で、 f xs = go xs 0 where go [] acc = acc go (x:xs) acc = go xs (
処理の切り替えとFreezeパターン - Just $ A sandbox
以下、Objectというとメソッドと適当な引数を与えると自分自身を返したり返さなかったりするデータ型、またはobjectiveのObjectということにしておきます。 newtype Object xs = Object { runObject :: forall a. Methods xs a -> ctx (Object xs) a } さてオブジェクトを実行し続けて、あるタイミングで別の処理に切り替えたいということはままある。一番よくある例ではあるタイミングでオブジェクトが死ぬ、死んだらオブジェクトを破棄する処理に移行する、みたいなことがしたい、とか。 そのままオブジェクトを丸ごと破棄してGCに回収させればよいのであれば何も考えなくていいんだけれど、大抵の場合は後処理があり、後処理には死ぬ直前のオブジェクトからデータを拾ったり、ということはまぁあるよねと。 おそらく一番簡単なのは i
Notions of Computations and Effects - Just $ A sandbox
前回のeffect systemに対するボヤキ、あるいは予言が色んな人に読まれたみたいなので興味がある人が一定数いるならeffect systemの紹介記事をちゃんと書こうと思った次第。 というわけでmonadを前提としてプログラミング言語的な見方と圏論的な見方を通してeffectに関するお話をしてみます。 注意 以下のプログラムはHaskellに寄せたオレオレsyntaxで実際にそういう実装があるわけじゃないので注意してください。実際の実装されている言語の話は最後に少しします。 programming with effects effectは通常type-and-effect-systemと呼ばれるようにある意味で一種の型システムのようなものです。型システムがプログラムの入力と出力の値を見積もる仕組みだったのに対し、エフェクトシステムはプログラムを実行した際に「起きうる」エフェクトをコン
monadからeffectへ - Just $ A sandbox
追記 もう少しまともなeffect入門記事を書きました myuon-myon.hatenablog.com この文章は今から5-10年後に万が一effect systemが流行り始め、今のHaskellのような立ち位置になった場合に備えて書いています。 effect systemについて Haskellはモナドを用いて純粋・非純粋を切り分けることができる言語で、computational effectを扱うために導入されたものだった。 かつては関数 A -> B で一緒くたにしていたcomputationは、 A -> T B と、文脈 T をもった関数として表現できるようになった。ところでこのようなcomputational effectとしてのモナドを言語機能に組み込むには2つの方法があって、 Meta Language方式 (Haskell) Programming Language
Free Monadic Parser - Just $ A sandbox
動機 Haskellでは * -> * カインドを持つデータ型からFreeモナド(Operational)を使って5秒でDSLが作れることは有名だけど、 そうやって作ったDSLをスクリプトとして外部ファイルから読み込むようなことがしたいこともあるかもしれない。 そういう時にわざわざパーサーを頑張って1から書くのはしんどいし、うまい具合にやってくれてもいいのだろうか、という話。 結論から言うとある程度うまい具合にできます Freeモナドについて FreeモナドはFreeなので特別なprimitive operationは定義されていないから、モナドのoperationだけをパースすることを考えればいい。 つまり、 ex = do Con1 x y t <- Con3 a b c Con4 t のようなものがパースできればよさそうなことがわかる。 本来はモナドで定義可能な関数(whenとか)は
Object型とOpenUnion - Just $ A sandbox
Table of Contents 1. Widget型 1.1. 直和と直積 2. 内部状態 3. Widget Operation 4. 継承、合併 5. 関係ないけれど 6. おわりに 今現在Haskellを使ってゲームを作っていて、そこで「オブジェクト」的なものが欲しくなってあれこれした結果を説明として残しておきたいので書きます。 Haskellでオブジェクト指向をエミュレートするのには objective というのがあるんだけどまぁ大体そういう感じの話です。 Widget型 ゲーム内では、Widgetと呼ばれる、画面上に表示されたり内部状態が変化して見た目が変わったりするコンポーネントを扱うことにしている。 つまり画面に表示されたりするUIを司るための型を用意しておいて、それに対して特定の信号を送ると内部状態が変化したりしなかったりする。 Widget型の定義は以下の通り new
Freer Monadじゃあないんですよ - Just $ A sandbox
Extensible Effectsという、大変有名なモナドの合成方法があって、まぁこれはいいんだけど、関連する話でFreer monads, more extensible effectsという論文があり、これまた界隈では有名なんだけどなんやねんって話。 とりあえずext effはモナドを直和していい感じにするってことと、freerはOperational Monadを使ったんやなってことがわかっていればひとまずクリアという感じ。 よく知らない人はこれ読んで めっちゃわかりやすいから👇 Freer Monads, More Extensible Effects from Hiromi Ishii www.slideshare.net さて、まぁ上のような説明も上にあげた論文もHaskellのコードしか書いてなくてさっぱり分からないのでもっとちゃんと定式化しようねということを簡単にまとめ
Theorem Prover Haskellの紹介 - Just $ A sandbox
この記事はTheorem Prover Advent Calendar 2016の1日目の記事です。 今年も残り1ヶ月になったことを信じたくないと思いつつ、 まあ学生的には4月始まりだから大丈夫と自分に言い聞かせてます。 今回のアドベントカレンダーのネタを必死に1週間くらい前から頑張って探した結果 何も見つからなかったのでHaskellで証明を書きます。 みなさんHaskellで証明を書くのはつらいと思うかもしれませんが 実はEquational Reasoningも使えるし 最近バージョンが上がって少し賢くなったコンパイラの強力なサポートも受けられるので 意外とマシです。(当社比) さてHaskellで証明をすることについてですが、 ここでは定理証明界のFizzBuzzとも名高い*1、リストのreverse関数が2回やると元に戻ることを示します。 Leanで書いた同じ証明も置いとくので、
データ型のCPS変換について - Just $ A sandbox
HaskellでCPS変換とか調べているとデータ型のCPS変換というのが出てくる. 関数のCPS変換は継続を引数に追加して末尾再帰の形にすればだいたいOKなのでまあわかるのだけど, データ型のCPS変換というのは何なんだという話. 継続は何を継続しているのかがいまいち分からないので何故そのデータ型はCPS変換するとその型になるんだと不思議に思っていたのがちょっと解決したのでそれについて書く. 関数 is っょぃ パフォーマンスのことを考えれば, 関数型と基本型(ground type)が型の中では圧倒的に偉い. 基本型というのはまぁproductとかrecursionとかdependent typeとかを含まない基本的な型のこと. 例えばIntとか(Haskellのような言語ではIntというのは計算機の都合上特別扱いされているので, ここでのIntはN×Nにring構造を入れたもののことで
Theorem Prover Leanの紹介 - Just $ A sandbox
Microsoftが開発したTheorem Prover Leanを紹介します. 特徴 他の言語と軽く比較する. あくまで個人的な感想です. Lean Coq*1 Agda Isabelle 証明の書き方 structured proof, tactic, 函数定義 tactic 函数定義 structured proof, tactic 開発環境 emacs emacs, CoqIDE emacs jEdit ドキュメント × ◎ ○ △ implicit parameter ○ ○ △ (型を使わないので不要) Equational Reasoning ○(builtinなものはOK. 独自演算子は条件付き) ？(知らない) ◎ ○(基本的にbuiltinなもののみサポート) 自動証明 ×(なし？) ○(auto, omegaなど) △(emacsのautoコマンド) ◎(auto,
オートマトンで遊ぶやつを作った - Just $ A sandbox
この記事はHaskell Advent Calendar 2015 18日目の記事です. Automatoy(オートマトン)で遊ぶやつを作ったので紹介します. github.com ブラウザで遊べる. 以下それっぽい解説. Automatoyについて http://myuon.github.io/automatoy/ "Def"タブでオートマトンを定義. "Check"タブで与えられた文字列のacceptance checkができる. "Conversion"タブでいくつかのサンプルオートマトンを読み込んだり, NFAをDFAに変換(いわゆるpowerset construction)できる. また, 右上のImport/Exportでjsonに変換したり, jsonを読み込んだりできる. もう少し扱えるオートマトンのバリエーションを増やしたり, acceptance checkにアニメー
Haskellで大富豪を作ろう (1)トランプを用意しカードを配ろう - Just $ A sandbox
まえがき Haskellでなんか動くものを作ろうと思った. 規模と知名度等を考えて大富豪あたりが妥当なところかと思ったので, 今回はCUIの大富豪を作ろうということにした*1. コード自体は完成しているので, 何回かに記事を分けて説明をつけて投稿していくつもり. なおとにかく動くものを作りたいってことしか考えてなかったので完成したコードはあんまり綺麗じゃない模様. 第一回 トランプを用意しカードを配ろう まずはトランプを用意しよう. 今回は4種類A~Kまでの通常のカードとジョーカー2枚を使用する. これをまずはdata Cardとして定義する. ついでに, 大富豪ではカードの強さ比較をすることが多いのでOrdのインスタンスにする. このとき大富豪式に数字の強さを(3が弱く2が強くJokerが最強になるように)定義しておくと便利かもしれないということでそうした. data Suit = Sp
Lens from Scratch - Just $ A sandbox
久しぶりのLensの記事です. 5億回は繰り返されてきたであろうLens再実装を通して, Lens, Getter, Setter, Iso, Equality, Traversal, Prism, Foldの仕組みを理解するのが目的です. 亜Lens family Getter Getterは基本的にはConstをかぶせる操作とそれを剥がす操作で実現可能です. つまりgetConst (Const k) = kですが, このConst kがデータであり, getConstは値を取り出すgetterになります. アクセサの型がGetting r s aであるとき, sからaを取り出せる(=s -> aなるgetterである)という意味です. (^.)はGetterとデータから具体的に値を取り出し, toは函数をGetterに変換するための函数です. type Getting r s a =
原始帰納的函数で素数を計算 - Just $ A sandbox
原始帰納的函数; 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^n_i : \mathbb{N}^n \to \mathbb{N}$ はprfである prf $f : \mathbb{N}^m \to \mathbb{N}, f_i : \mathbb{N}^n \to \mathbb{N} (1 < i \leq m)$に対し, 合成 $g(\vec{x}) = f(f_1(\vec{x}), \cdots ,f_m(\vec{x}));\; g : \math
Codensity Monad - Just $ A sandbox
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) where return x = Codensity (\k -> k x) m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c)) これの何が良いかと言うと, これは以下のようにMonadFreeな作用を持つ. instance (Functor f, Mon
Classical set theory in Agda - Just $ A sandbox
Agda歴2週間くらいのザコです。 Agdaで圏論のライブラリを作って、流れで位相空間の定義をしようと思ったらそもそも集合を普通に扱えるライブラリがどこにもない。 標準ライブラリにRelation.Unaryとかいうのもあるけど、これは表面的には上手く行っているように見えるだけであんまり使い物にならない。 具体的に言うと和集合の公理がないので(binary cupとindexed bigcupはある)任意個のUnionがとれない。 他にも、そもそも∈の定義が函数適用なので X ∈ B と書いときにXとBでは型が違うのがすごくキモいとか。キモいというかこれのせいでZFの一部の公理は型があわなくて表現できなかったりもする。 そういうわけでまずは集合を使えるようにするというだけ。 コードは一番下に載っけました。 コードについて 二重否定除去 Relation.Nullary.Negation e
Printf実装を通して学ぶGADTs, DataKinds, ConstraintKinds, TypeFamilies - Just $ A sandbox
問題 問. 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:3.1415 Cのprinfとは異なり、%dや%fが文字列に直接埋め込まれていません。よって当然型が合わなければ、すなわち printf [_d] [(3.1 :: Float)] などとかくとコンパイルエラーになってほしいわけです。 解答 私が実装したものが以下にあります。 https://gist.github.com/myuon/9084939 以下ではこのコードについて
Haskellでもできる！実践・オブジェクト指向 - Just $ A sandbox
Lensにほとんど触れたことのない人にはこちらの記事がオススメです：Lensで行こう！ - Just $ A sandbox Haskellでもオブジェクト指向をしましょう！ Haskellは直接オブジェクト指向的な機能を提供してはいませんが、我らがLensの力を借りることでオブジェクト指向的な設計を意識したコーディングが可能です。 今回利用するのは主に以下のモジュールです。 Control.Lens.Lens Control.Lens.Getter Control.Lens.Setter Control.Lens.TH Lensのおさらい Lensを使ったことのある人にはおなじみだと思いますので、特に解説はしません。 type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t -- Lens型(GetterやSett
Pythonでsuper(self.__class__, self)は使うな - Just $ A sandbox
[追記:2013/11/02] この記事ではPython2.xを前提としていますが、Python3以降はsuperの引数を省略することができるようになっています。 [/追記] 次のPythonコードを見てください。 class A(object): def method(self): pass class B(A): def method(self): super(self.__class__, self).method() class C(B): def method(self): super(self.__class__, self).method() >>> c = C() >>> c.method() このコードを実行すると、 RuntimeError: maximum recursion depth exceeded while calling a Python object す
lxmlチュートリアル翻訳してみた - Just $ A sandbox
PythonでXML(HTML)を扱う高速で便利なライブラリがlxmlです。 非常に強力なメソッドが多数用意されているのですが、日本語の情報があまりないのが弱点です。なので今回、lxml.etree公式チュートリアルの一部を勝手に翻訳しました。 量が多いので全ては訳しきれていませんが*1、lxmlでおそらく一番よく使われるであろう、Elementクラスの部分を中心に訳を作りました。誰かのお役に立てれば幸いです。 また、翻訳にあたっては直訳よりも日本語として自然な訳を選んだ部分があります。正しくは原文を参照してください。ここの訳がおかしい、日本語が不自然、この文書も訳せ等ありましたらお知らせください。 lxml.etree チュートリアル lxml.etreeチュートリアル これはlxml.etreeを用いたXML処理に関するチュートリアルです。これはElementTree APIのメインコ
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
