Just $ A sandbox

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

Free Monadic Parser

動機 Haskellでは * -> * カインドを持つデータ型からFreeモナド(Operational)を使って5秒でDSLが作れることは有名だけど、 そうやって作ったDSLをスクリプトとして外部ファイルから読み込むようなことがしたいこともあるかもしれない。 そういう時にわざわ…

Object型とOpenUnion

Table of Contents 1. Widget型 1.1. 直和と直積 2. 内部状態 3. Widget Operation 4. 継承、合併 5. 関係ないけれど 6. おわりに 今現在Haskellを使ってゲームを作っていて、そこで「オブジェクト」的なものが欲しくなってあれこれした結果を説明として残し…

ゲーム制作進捗報告会その3

ようやく本質的な進捗が生まれ始めていて嬉しい 進捗報告 設計 前回異様に苦しんでいた設計問題はめでたく解決し、ちゃんと進捗しつつあってよい 結論だけ言うと newtype W = W (forall (m:Monad) x. Union xs m x -> br W (m x)) の形の型を使っている。 再…

ゲーム制作進捗報告会その2

なんとまだエターナってません バンザイ 進捗報告 あんまり進んでない, 設計で悩んだりしてたら調査とかで時間が無限に溶けてる ゲームシステム 調合システム: レシピを用意したのでポーションを使えるようにすることとUIを作る所に入れそう TODO:9/16 パラ…

ゲーム制作進捗報告会その1

ちょっと前にゲーム作る機運が高まってきたなって言っていたのだけれど myuon-myon.hatenablog.com まぁ作ろうということになり、ここ1週間位ずっと作業していたので 進捗報告ということで こういうことでもしないとモチベーションを保ち続けられる自信がな…

ゲームを作る機運が高まってきた

個人のゲーム制作といえばRPGがなんとなく花形感がありますが(多分ツクールのせいや) じゃあ作ろうって思って完成まで行くのは結構大変ですよねみたいな 以下言い訳が並びます グラフィック 多分一番問題になるのはここで、スキルはないが人間はいる(人間を…

typecheckerとTagless-final, revised

1個前の記事でTagless finalについて触れたんだけどどうも全く頭が回っていなかったらしくほとんど内容がない記事になってしまったので書き直す、というかちょっと違う話を。 はじめに、TaPLにあるλ計算のtypecheckerをHaskellで実装することをやっている: g…

Tagless-finalによるデータ型の間の変換

Q. Tagless-finalってなんぞや A. (in short) データ型DをF[D]のinitial algebraとみなしたとき、initialityより、任意のalgebra F[D](X) --> Xに対してunique transformation D --> Xがある。 このときfamily forall X. F[D](X) --> XをDのTagless-final re…

Freer Monadじゃあないんですよ

Extensible Effectsという、大変有名なモナドの合成方法があって、まぁこれはいいんだけど、関連する話でFreer monads, more extensible effectsという論文があり、これまた界隈では有名なんだけどなんやねんって話。 とりあえずext effはモナドを直和してい…

functor, あるいはarrow equalityについて

Category TheoryのFormalizationがらみの話。 Category TheoryのFormalizationをするときは、基本的にSetoid-enrichedでやるのが筋がよいということはこの業界(?)では有名な話だし、少し前のブログ記事にも書いたのでそのことを前提として次のようなことを…

あのとき知りたかったCoqの話

Coq

最近Coqをかいていて、まぁ自分は基本姿勢として「CoqにはProof Assistantの方向性として共感できないのでもっとよいものが出てきて早く駆逐してほしい」だったのだけれど、 たくさん書いてると多少偏見もなおって考えを改めたりした部分があるのでまとめる…

Formalization of Setoids-enriched category theory

Coq

最近書いてるCoqの話。 主にこれの解説をします: Yoneda.v · GitHub Setoidをベースにすることについて 多分圏論formalize業界(狭そう)では有名な話。 Coqの場合はSetoidのequalityに対してもrewrite tacticが使えるのでそれでやる。 Proper Setoid morphism…

Coq 8.6のインストールほか

Coq

Coq 8.6をインストールしたときのあれこれ Coqのインストール Coq/SSReflect/MathCompの設定 これの通りにやるだけ aptのパッケージは古いからだめってあったので言われたとおりにopamでいれた それと~/.opam/4.04.0/binにパスを通すのもやった. どうもopam…

minecraft 1.11 MOD開発メモ

1.11準拠のMOD開発に関するメモ 詳しいことは自力で調べてね的なスタンス 概要 proxyを用意して、common proxy側にMOD本体の処理、client proxyに描画関係の処理をかくようにする ゲーム内のオブジェクトの管理はすべてナントカregistryがやってくれてる だいた…

自作PC組んだよ2017

構成は次の通り niku.webcrow.jp 自分で使うPCを自作したのは初めてだったので色々調べながらパーツを選んだ。 一応個人的な選定基準とかを書いておく。 用途は、主に開発・たまにコンパイルとか動画編集・たまーーーにゲーム とか色々。 パーツ選び CPU Cor…

凝りたいけど凝りたくない妥協デスクトップLinux環境

今のデスクトップLinuxの環境をまとめておこうと思った。 新しいPC買った時に見る用ということで。 できればどんどんより良く設定していきたいので、またこの時点から色々変わってきたら新しく記事を書こうと思います。 (少なくともこの記事を書き換えること…

ペンタブを買った

追記 DIGImendを公式からパッケージを落として入れたら何かと競合したみたいで ペンタブが一切認識されなくなった。 sudo rmmod hid_uclogic && sudo insmod /lib/modules/$(uname -r)/kernel/drivers/hid/hid-uclogic.ko で直ったけど、USB挿して動くならDI…

2016年のまとめ

もうすぐ2016年も終わるので今年したこととかをまとめる。 研究・勉強 割とずっとtyped lambda calculusのsyntaxやらsemanticsやらやってた気がする。 Proof Assistantももう少し調べなきゃなーと思いながらあんまり欲しい結果を出してる論文とかもないしこ…

Recursive Typeの実装

前回はsimply-typedの拡張としてλμを実装したけれど、 今回はsimply-typedにrecursive typeを実装してみた。 recursive typeはいわゆる(G)ADT相当の機能だけど、型パラメータを持たないのでADTの真面目な実装に比べると楽だと思う。 recursive typeはType ->…

λμのTypeCheckerの実装

λμのtypecheckerを実装したので (ソースコードは参考文献[3]を参照) λμ[1]はλ→に継続(callCC)を入れたもの(CCC + Continuation monad)。 syntax的にはμ-abstractionとnaming(termに名前をつける)が追加される。 型なしの項を受け取って、それにうまく型をつ…

依存型による定理証明Tips: coherenceは型で表せ

この記事はTheorem Prover Advent Calendar 2016 12日目の記事です。 この記事は定理証明初心者向けの記事です。 普段から依存型を用いた定理証明をされている方は読む必要がありません。 "coherence condition"と呼ばれる条件があり、訳すと「一貫性条件」…

鬱モード全開だったときに

今から大体3年くらい前の、大学学部2回生の頃に唐突に精神が死んだことがあった。 という話をするけど、この先読んでも特にオチはありません。 ただの身の上話なので。 非常に運がよかったため自分は3回生の進路振り分け的なものに必要な単位を前期で全て揃…

Theorem Prover Haskellの紹介

この記事はTheorem Prover Advent Calendar 2016の1日目の記事です。 今年も残り1ヶ月になったことを信じたくないと思いつつ、 まあ学生的には4月始まりだから大丈夫と自分に言い聞かせてます。 今回のアドベントカレンダーのネタを必死に1週間くらい前から…

Programming in Scalaを読んでいる時のメモ

Programming in Scala: A Comprehensive Step-by-Step Guide, Third Edition (English Edition)作者: Martin Odersky,Lex Spoon,Bill Venners出版社/メーカー: Artima Press発売日: 2016/04/27メディア: Kindle版この商品を含むブログを見る を読んでいる時…

λ→のtyping & unification algorithm

この記事のunification algorithmは間違っているので λμのTypeCheckerの実装 - Just $ A sandboxを参考にしてください λ→のtypingアルゴリズム. variableとabstractionは型が一意に決まるので, 問題はapplication. MN:aからM:?x -> aの?xをどうやって決定す…

tmuxからのpowerlineで優勝せえへん?

メモです. 現状イマイチなところがありありなのでどうにかしたい. 環境 以下に同じ端末環境を作りたかった. Ubuntu 16.04 Mac OS X El Capitan Debian jessie (Mac上のVM環境) zsh zshを入れてデフォルトのshellをzshにする. prezto github.com を入れる. 入…

React ComponentにImmutable.jsは(多分)だめ

github.com ここにもはっきり書いてあるように, Note that state must be a plain JS object, and not an Immutable collection, because React's setState API expects an object literal and will merge it (Object.assign) with the previous state. Reac…

variable-free type theoryの圏論的な解釈について

myuon-myon.hatenablog.com の続き. いくつか疑問が解消されたのでそれについて. var-free type theoryについて syntaxはcontext, type, term, substからなる. contextはtypeの有限列(通常はvariableとそのtypeの組の列だが, 今回はvariable-freeなのでtype…

データ型のCPS変換について

HaskellでCPS変換とか調べているとデータ型のCPS変換というのが出てくる. 関数のCPS変換は継続を引数に追加して末尾再帰の形にすればだいたいOKなのでまあわかるのだけど, データ型のCPS変換というのは何なんだという話. 継続は何を継続しているのかがいまい…

type theory with variable-free syntax

(追記) 解決した: variable-free type theoryの圏論的な解釈について - Just $ A sandbox -- 文献に突然登場して?ってなったので. 調べても情報がヒットしないのでよくわからないけど, simply typed lambda calculusを変数を使わずに定義するものらしい. で…

CoC7th キャラクターシート(印刷用)

CoC7用にキャラシを作った. 表面のみ. png: pdf: CoC7th キャラクターシート

Coinductiveのintro rule

Type Theory & Functional Programmingに出てきたCoinductive typeのintro ruleに少し悩んだので. Coinductiveは最大不動点の形でかけるような型. 例えばStream(無限リスト)はP X = N × Xの時のPの最大不動点である. テキストにはCoinductiveのintro規則と計…

AviUtlスクリプト 「自由落下と衝突」 v1.0

この前MAD動画を作るのに作ったAviUtl用のアニメーション効果を公開 概要 上からオブジェクトが落ちてきて, 地面に衝突して跳ね返る動きを実現します. オブジェクトの位置(Y座標)が地面の高さに対応. パラメータについて 加速度: 重力加速度. 落下にかかる時…

Theorem Prover Leanの紹介

Microsoftが開発したTheorem Prover Leanを紹介します. 特徴 他の言語と軽く比較する. あくまで個人的な感想です. Lean Coq*1 Agda Isabelle 証明の書き方 structured proof, tactic, 函数定義 tactic 函数定義 structured proof, tactic 開発環境 emacs ema…

オートマトンで遊ぶやつを作った

この記事はHaskell Advent Calendar 2015 18日目の記事です. Automatoy(オートマトン)で遊ぶやつを作ったので紹介します. github.com ブラウザで遊べる. 以下それっぽい解説. Automatoyについて http://myuon.github.io/automatoy/ "Def"タブでオートマトン…

『ふたりのハードプロブレム』 感想

ncode.syosetu.com 以下, ネタバレ注意. ジャンルとしてはSFでしょうが, 話自体は人間ドラマに重きが置かれているという印象でした. 登場人物がみんな感情豊かで人間臭いのがまた良いところ. あまりあらすじ等を確認していなかったので, 前情報なしだといい…

『Normalize Human Communication のまひゅ』 感想

http://mukiryokukan.sakura.ne.jp/NormalizeHumanCommunication.htm以下, ネタバレ注意.ずっと前から友人から勧められていたのでやりました. プレイしてから多少時間が空いてしまったので記憶が少し曖昧ですが感想を述べることに. 一言で言うと「緩やかな死…

ノベルゲーム「人形劇が終わる夜」をリリースした

もう2週間近く前ですがノベルゲームをリリースしました.www.freem.ne.jp反省会を兼ねてその話. 企画 前のノベルゲームをリリースしたのが2年近く前ということもあり, そろそろなんとなくノベルゲーム作りたいなと思ったこと. 諸般の事情で現実逃避先として「…

ListのT代数の非自明な射は何か?

ListのT代数の非自明な射は何か?という感じの話. List Monad, T-Algebra 以下のようなmonoid free functorとforgetful functorの随伴がある: free functorは集合を自由モノイド(wordの集合, 演算は結合)に飛ばし, forgetful functorはモノイドを底集合に飛…

ノベルゲームシナリオ論

※ 以下は全て個人の感想です。 長さは「正義」 長いゲームは飽きられやすいけれど、その点さえ解決できれば長さは完全に正義である。 長時間プレイしてくれたプレイヤーは大抵どのキャラにも相応の愛着が沸いているので、キャラクターらしささえ損なわなけれ…

Monadic functor(後で調べる)

$G : \mathcal{C} \to \mathcal{D}$がmonadic functorということは、圏同値の差を無視してforgetful T-algebra functor $G ^ T : \mathcal{C}^T \to \mathcal{C}$と同じだと思えるってことだ. ここから何か分かったりしないんだろうか.

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 $…