κeenです。連休中にIsabelleを少しばかり触ったのでその時のまとめを。

κeenです。またしても深夜になってしまいましたがSML#のpthreadバインディングを作ったのでその報告を。

κeenです。深夜にですが小ネタを。

2016年個人的に注目したいというか力を入れたいというか成行を見守りたいというか、そんな技術達を書き連ねていく。ものによっては「何を今更」と思うかもしれないがあくまで私にとって、だ。

順不同。

κeenです。ATS2には3つの世界があります。動的な世界、静的な世界、証明の世界。 前回の記事では静的な世界を色々扱ってみました。 今回は証明の世界である観について少し。

κeenです。少しばかりATS2を触ってみたので成果報告でも。

AVL木は左右のノードの高さが高々1しか違わない平衡二分木です。OCamlやSMLでナイーブに実装すると本当に1しか違わないことを保証するのは難しく、精々テストなどで部分的に検査するだけです。

ところがSMLに似た文法を持つATS2には依存型があり、左右のノードの高さが高々1しか違わないことを型で保証出来ます。 つまり、左右のノードの高さが2以上違う木を作ろうとしてもコンパイルエラーになるのでコンパイルが通れば高さについてはバグがないこと保証されます。

そういうAVL木を使ってTreeSetを作ってみたので紹介します。

κeenです。Advent Calendarのためにネタやアイディアを用意したものの時間/場所的都合でAdvent Calendarとして出せなかったボツネタでも供養しようかと。 Advent Calendarが終わってしまったので投げやり気味ですね。 第3段はSML#とCプリプロセッサで連携する話。

SML#のC FFIを使ってるとマクロで定義された値などを触りたくなるのですが、触れないのでどうにかしようかと。

κeenです。Advent Calendarのためにネタやアイディアを用意したものの時間/場所的都合でAdvent Calendarとして出せなかったボツネタでも供養しようかと。 Advent Calendarが終わってしまったので投げやり気味ですね。 第2段はSML#のオレオレREPLを作る話の初級。

SML#にはFFIがあり、任意のオブジェクトファイル/ライブラリをリンクしてC関数を呼び出すことが出来ますが、REPLで試そうとしてもREPLにリンクされていないので呼び出せません。 そこで呼び出したいオブジェクトファイルをリンクしたREPLを作れば捗るよね、という発想です。

κeenです。Advent Calendarのためにネタやアイディアを用意したものの時間/場所的都合でAdvent Calendarとして出せなかったボツネタでも供養しようかと。 Advent Calendarが終わってしまったので投げやり気味ですね。 第1段はRustのロガーを作る話。

Rust Advent Calendarの初日でロガーはfacadと実装に分かれてると書きましたが、実装を作る話ですね。

この記事はApache Drill Advent Calendar 201521日目のエントリです

最初は備忘録がてら普段使うMySQL、BigQuery、SQLite、Apache DrillのSQLシンタックスの違いでも書こうかと思ったのですが調査が思ったより大変だったのでやめました。ANSI SQLも色々変わってるということは理解出来ました。

ということでApache Drillを使ってて「ん？」と思った挙動をいくつか出してみようかと。1.4時点での情報です。