Just $ A sandbox

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

アレ活が終わっていた

もう5億ヶ月前の話になるのだけどアレ活が終わっていた これによってとりあえず卒業後の進路は確保できたので路頭に迷ったりニートになる必要はなくなったのでアンシンアンシン 来年から東京の某企業で仕事をするらしい。 何するか具体的にはよく知らないんだけど開…

【宣伝】C92で「簡約!? λカ娘 10」が出ます

ほーむ - 参照透明な海を守る会 C92にてサークル「参照透明な海を守る会」より「簡約!? λカ娘 10」が出ます。 1日目 金曜日 東た11b だそうです。 今回私も初めて参加させていただきました。 簡約!? λカ娘 10 - 参照透明な海を守る会 「モナドとひも」という…

foldって難しくないですか

foldって難しい、というか書きづらくて読みづらくないですか、と思った話を書きます(そういう感じの話題でTLが盛り上がってたので) 以下、foldをrecursion schemeの観点から理解していることは前提とします foldをかく foldを書きたい foldを書こうと思う場…

ゲーム進捗報告会その5

更新忘れたわけでもプロジェクトが崩壊したわけでもないぞ 進捗報告 スタイルシート: デザインに関するあれこれは全部リソースファイルで記述できるようにしたい、と思ったので、画面上のWidgetにidを割り振り、対応するidに関連するコードをファイルから読…

Haskellでつまずいた所まとめ への回答その2

lugendre.hatenablog.com こちらの記事への回答です。 前回の続き ただ割と前回と被ってるのでそこはスルーしますねGOMENNNASAI 適切な入門記事がない: 日本語は話者が英語に比べて少なすぎるので敢えて日本語で記事を書くことのうま味がね、はい(英語なら割…

Haskellで躓いた(躓いてる)ポイントまとめ への自分なりの回答

各位はHaskell初心者を脱する前に初心者的つまづきポイントをまとめておいてくれると後続の初心者と上級者に喜ばれるのでなにとぞ— みょん (@myuon_myon) 2017年8月2日 qiita.com こんなふうに各位を焚き付けてしまったのでせっかく色々まとめていただいた記…

処理の切り替えとFreezeパターン

以下、Objectというとメソッドと適当な引数を与えると自分自身を返したり返さなかったりするデータ型、またはobjectiveのObjectということにしておきます。 newtype Object xs = Object { runObject :: forall a. Methods xs a -> ctx (Object xs) a } さて…

Notions of Computations and Effects

前回のeffect systemに対するボヤキ、あるいは予言が色んな人に読まれたみたいなので興味がある人が一定数いるならeffect systemの紹介記事をちゃんと書こうと思った次第。 というわけでmonadを前提としてプログラミング言語的な見方と圏論的な見方を通してe…

monadからeffectへ

追記 もう少しまともなeffect入門記事を書きました myuon-myon.hatenablog.com この文章は今から5-10年後に万が一effect systemが流行り始め、今のHaskellのような立ち位置になった場合に備えて書いています。 effect systemについて Haskellはモナドを用い…

ゲーム進捗報告会その4

進捗進捗ゥ!!! 進捗報告 ゲームシステム スクリプトエンジン 簡単なスクリプトとスクリプトエンジンを作った これでキャラクター画像の管理とかメッセージをリソースとして外部ファイルに丸投げできるようになったので良い感じ。演出とかで使っていく エ…

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に名前をつける)が追加される。 型なしの項を受け取って、それにうまく型をつ…