Just $ A sandbox

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

ペンタブを買った

追記

DIGImendを公式からパッケージを落として入れたら何かと競合したみたいで
ペンタブが一切認識されなくなった。

sudo rmmod hid_uclogic && sudo insmod /lib/modules/$(uname -r)/kernel/drivers/hid/hid-uclogic.ko
で直ったけど、USB挿して動くならDIGImend入れない方がいい可能性がある。


前に使っていたWacom BAMBOO(前のシリーズの方 今はIntuosとかいう名前になったらしい)の描画領域が狭すぎて
FullHDモニタで絵を描くのがつらくなってきたので新しいものを買った

買ったのはHUION H610 Proというやつ これ?

ペンタブ自体のサイズはA4より少し大きいくらい。
描画できる領域はB5くらい。

レビューで「ペン先がすごく沈む」ことばかり書かれていて不安だったけど、
少なくともシャーペンでは2Bしか使わない弱筆圧マンの自分には全然気にならなかった。
というか、ペン先がガタガタしてるわけじゃなくて力をかけるとそれに応じて沈む感じなので(筆圧を上げると深く沈む。必要な力は滑らかに段々大きくなる感じ)
むしろ硬いペン先よりは手が疲れにくい気がするので大丈夫です。

また、Ubuntu + Kritaで絵を描いているけれど特にドライバ周りの不具合もなし。
USBを刺しただけでちゃんと認識しました。

ネットによるとGIMPは筆圧をちゃんと認識しない可能性があるらしいのでGIMP使いたい人は注意。

(wacom製じゃないペンタブのカーネル用のドライバはDIGImendというのがあるらしく、
HUION H610はこのパッケージに対応していることを確認してから買いました。
あとどうもDIGImendはもう開発ストップしてるっぽい?)

ドライバ関係の話は?を見ると良いと思う

kaiware-daikon.hatenablog.com

以下、購入を検討したペンタブ:

  • Parblo A610

よさそうではあった。HUIONのよりちょっと安いし(HUIONのもセールしてたので実はそんなに変わらないけど)。
ただしDIGImendが対応してるペンタブリストに入ってなかったので
ドライバ関係でうまく行かなくなるとつらいなということでやめた。

言わずとしれたWacomなので別にこれでもよかったのだけれど、
Intuos Proは少し高すぎて手が出ないし、
そうでないやつは同梱ソフトが要らなかった(Mサイズで同梱ソフトなしはない)ので、ソフト代無駄だな〜と思ってやめた。

ていうかIntuos使っている人で、ペンタブ壊れたとかサイズ大きいのが欲しいみたいな人は
どうしているんだろう。ソフト余るよね?ってめっちゃ思った。

おわり

2016年のまとめ

もうすぐ2016年も終わるので今年したこととかをまとめる。

研究・勉強

割とずっとtyped lambda calculusのsyntaxやらsemanticsやらやってた気がする。
Proof Assistantももう少し調べなきゃなーと思いながらあんまり欲しい結果を出してる論文とかもないしこっち方面はあんまり何もやることない感じもある。

来年はもう少し手を広げたり具体的に何をするかを考えたり手を動かしたりすることになると思う。

あと下でも言うけど実装もやったね。

プログラミング

Githubリポジトリは10個くらい増えてた。
色々やり過ぎてあんまり覚えてないけど、実質何もしてないのを除くと、実用系アプリケーションいくつかと定理証明系とその他って感じ。

定理証明は趣味でいいや〜ってなったような気もする。
証明のテクニカルな話とか、今の段階だとつらいだけだから証明士の人に任せた方がよさ気な感じではあるなとか思った。

あとScalaを始めたけど結構良かったのでこれからちょいちょい書いていくかもしれない。

GIMPをやめてKritaに乗り換えた。
これのおかげでちょっと絵を描くモチベーションが上がって、12月くらいからはpixivも積極的に使おうという気持ちが湧いてきたのでこのままたまに絵をかいていければいいなという感じ。

絵に関してはとりあえずモチベーションの維持をどうやって行うかが一番問題になりそうなので、
とりあえず趣味でいいからちょいちょい描いてネットに上げるぐらいのことはしようと。
それにしても全然上手くならないからもうちょっと基礎的な練習も混ぜていきたい。

動画編集

動画編集は今年初めて手を出したジャンルだったけど、結構自分にも合っている感じがしてよかった。
ちまちま動きを作っていってかっこ良く動くとすごく楽しいので、たまにやれればいいな〜と思う。
(その前にスペック高いPC欲しい)

それと、動画編集に手を出したおかげで、かっこ良く動く動画の中のオブジェクトの動かし方や画面の構成に気を配って人の作品を見たりできるようになったので、新しい視点で動画を見ることができるようになったのは非常によかった。
動くものを作るときはきっと汎用的に役に立つスキルなので、たまにはそっち方面のセンスも磨いていきたい。

ブログ更新

気軽な気持ちで書くようにしたので、そんな気合の入ったものは書かなくなってしまったけど
どうせ趣味だしまぁいいやって気持ち。
割と頑張ってたと思うのでこれからもこんな感じで行こう。

コンテンツ消費

今年はコンテンツ消費(小説・漫画・映画・ゲーム等々)にかけたお金が人生で一番多かったんじゃないかというくらいコンテンツを消費してる気がした。

「好きなものにお金を払うことは正しい経済活動」なのだという気持ちを胸に来年もコンテンツ消費には一定以上のお金を投じていきたい。

その他

スケジューリング・タスク管理の重要さを自覚することが多かったような気がする。(いいこと)
まだ正しい方法論は身についてないけど、ちゃんとやるべきことを管理して計画的に作業を進められるようにしたい。

Recursive Typeの実装

前回はsimply-typedの拡張としてλμを実装したけれど、
今回はsimply-typedにrecursive typeを実装してみた。

recursive typeはいわゆる(G)ADT相当の機能だけど、型パラメータを持たないのでADTの真面目な実装に比べると楽だと思う。


recursive typeはType -> Typeなるmappingのleast fixed pointが取れるよってやつ。
あるいは任意のF-algebraに対してinitial objectが存在する*1ことなので、単なるCCCに比べれば相当強い構造が入ることになる。

さて、initial F-algebra Iが取れているとすると、定義より任意のF-alg f:FX -> Xに対して一意的な射I --> Xが存在してそれが誘導する図式が可換になるけれど、
このとき取れるI --> XIのelimination rule(destructor, recursor, induction function, etc)になって、
図式の可換性がelim[f](intro[ConI] a) => f (ConI a)という、言葉で言えば「コンストラクタつけてデストラクタつけたら元に戻る」というcomputation ruleを生成する。

ちなみに、initial F-algebraの構造射fI: FI -> Iがコンストラクタ(の直和)になる。

で、少し考えればこのfIは同型になるので、その逆射はI -> FIという、いわば「データ型を定義に従って直和に分解する」射になる。

このときunfold: I -> FIおよびfold: FI -> Iの2つのruleと、上に書いたようなintro[-]: (A -> FI) -> A -> Ielim[-] : (FI -> X) -> I -> Xなる2つのruleは同値になるので、結局recursive typeの実装はこのunfold, foldを実装すればよいことになる。

という前置きをしておいて実装の話。


型のleast fixpoint operatorをμでかく。

- fold rule:
f: F(μX.FX)
--------------
fold(f): μX.FX


- unfold rule:
f: μX.FX
-------------------
unfold(f): F(μX.FX)

- computation rule:
unfold (fold (f)) => f

で、typing functionは次のような感じ。
(例によって証明もしてないし何も見てないので合ってる保証はない)

typing(fold[F](e)) = unify(typing(e), F(μX.FX)); μX.FX
typing(unfold[F](e)) = F(unify(typing(e), μX.FX))

(fold, unfold以外のtypingについては前回のλμの記事参照)

あとはこれを気合で実装すれば動く。
コードは[2]を参照。

それと、inductive datatypeだけではあんまり遊べないので、ついでに1と直和(fin. colimit)も入れておいた。
これでめでたくNat = μX. 1 + Xが定義できて、ちゃんとrecursive typeで遊べるようになった???


コードについて

exceptionsパッケージを始めて使ってみて、これはエラーを投げて別の場所でキャッチするだけならすごく簡単なんだけど、投げたエラーをきっちりデータとしてハンドリングするにはあんまり向いてなさそうだな(そもそも例外とはそういうものかもしれないけど)と思った。
CatchTやら何やらを使うとEitherに変換はできるけどエラーはSomeExceptionというexistに囲まれた謎の型が落ちてくるので、欲しいエラー型を持っているかどうかはこれだけではよくわからないし…。

一応、テストを書くときはMaybe型にして(うまく動くかどうかだけを気にする。エラーが発生するケースのテストも、どのエラーが出たかは気にしない)、実際に例のプログラムを動かすときはIO型にすることでエラーメッセージを表示、みたいな感じで使い分けている。
でも、こういう感じで「あるときはMaybeでエラーを握りつぶして、またある時はちゃんと画面に表示して」ってことが同じプログラムに対してどのrun関数を適用するかだけで変えられるのでそこはすごく便利。


次は真面目に型パラメータつきのGADTの実装でもやろうかなと思ってる。

ただ、それをやるならどうしてもカインド推論もしないといけないし色々めんどくさいからやだな〜という。
そもそも未だにパーサーすら用意してないのでそっちが先かも(流石にいちいちApp expr1 expr2とか書くのめんどくさくなってきた気もするし…)

まぁその時の気分で✌✌✌

参考文献

*1:任意のデータ型はinitial F-algebraでかける