はてなブックマーク

日記です。 リポジトリ: LayerXcom/cbc-casper-proof 概要 (私は LayerX の人ではないですが)LayerX 社の人と色々あって CBC Casper というブロックチェーンのプロトコルの検証作業を行いました。(主に定理証明士としてのお手伝い) 半年くらいかかったけどやりたかった証明についにたどり着いたよという話。 CBC Casper って何 わからん。(無知) 何かブロックチェーンのプロトコルの名前らしい。Ethereum 財団が目をつけてるらしい。いわゆるビットコインとは違ってブロックを頑張ってマシンをぶん回してマイニングしたりしないらしい(ビットコインは PoW で CBC Casper は PoS)。 詳しいことは詳しい人に聞いたほうがいいよ(真理)。 cf: CBC Casper と形式的検証 Isabelle で検証って何するの ブロックチェー

最近HaskellでAtCoderの問題を解いたりしているのでごく基本的な知見をまとめておく。 テクニック集 多くは割と色んな人がすでに言っていることではある。また、想定解法を正しく実装すれば以下のようなことを守らなくても時間内に収まるだろうが、GHCは最適化が効かなければ10倍遅くなる言語であるので普段から守っておくに越したことはないと思う。 環境: AtCoderのGHCは2019.04現在7.10なので注意が必要。そのうち上がるかもしれないけど。 Strict拡張がない BangPatterns拡張はある 環境構築がhaskell-platformらしいのでそれに入ってるライブラリしか使えない 文字列 基本はData.ByteString.Chan8 Stringは死んでも使わない(遅いので) Unicode文字列の扱いが必要(今の所みたことないけど)とかならtextを使うといいかも

タイトルがふわっとしてるけど見れば多分わかる。 ghc-compiler-notes 経緯とか 注意: 作ったと書いてるが私の力ではなく主に水無さん(@mizunashi-mana)とわどさん(@waddlaw)のお力添えによるところが大きい。 GHCのソースコードにはNoteと称して有益な(GHCの内部実装等に関する)情報が書いてあることは有名だと思うけど、実際にそれはまとまったりはしてなかったので知る人ぞ知る、みたいな情報であった。こういう他のドキュメントには書いてないような貴重な情報が誰にも読まれることなく眠っているのはもったいないと常々感じていたのでそれを読めるようにしたかった。 このプロジェクトは最近GitLabに移った方のghc/ghcのソースコードに埋められているNotes部分を抜粋しそれを比較的読みやすい形で並べて整理したものである。 現在の仕様一覧(ざっくり) compi

gRPCしたくなった。具体的にはRustで作ってるデスクトップアプリケーションで、GUIをElectronで書きたいのでNode.jsと通信が発生するのでそれに使えないかなと思って調査した。 gRPC(protocol buffers)とは gRPCはgoogleが作ったRPC(remote procedure call)のフレームワークで、簡単に言うとサーバー/クライアント間の通信が言語を問わずできるよ！みたいなやつ。 RPC自体は見た目は普通の関数呼び出しみたいな感じで書けて、裏ではHTTP/2の通信に乗ってやりとりが行われるようになっている。実際にはRPCを定義してからそれを呼び出すためにはサーバーやクライアントで言語ごとにインターフェイスの定義とかをしなければいけないが、それを自動で生成してくれるのがgRPCコンパイラという感じ。 gRPCを使うには、protocol buffer

定理証明、特に定理証明支援系(Proof Assistant)はその存在こそ少しずつ浸透しつつあるような気がしないでもないけれど資料とか全然まとまってないのが不便だなと前々から思っていたのでリソースをまとめておきます。 これも追加してほしいみたいなのあったら教えてください。 Proof Assistants 始めるなら次の中から選ぶのがよいと思います。 Coq Calculus of constructionsベースの型システムとリッチなコマンドを備えた言語 このリストの中では最もコミュニティが大きい、入門書等も豊富 型システムと項を書くためのGallina, コンパイラへの命令を記述するためのVernacular, タクティクスの定義に使うLtacなどの言語が混ざって出てくるのが初心者には混乱必至 結構複雑な言語なので使いこなすのはそれなりに大変 Agda Martin-Löf type

これ https://elm-lang.org/assets/papers/concurrent-frp.pdf はじめに 某所でFRPをeffect systemとみなせないか、という大変示唆的な質問をいただいて、気になったのでFRPについて調べてた流れで教えてもらったElmの作者が書いた論文。 自分はFRPについては「なんかEventとBehaviorがあってArrowになったりMonadになったりするやつ」くらいの感覚しかなかったので論文読んでみることにした。 ところでmarkdownで数式や図を記述するのは大変つらいので記事は適当に日本語で書きます。詳しく知りたい人は論文の方を読んでください。 あと、ElmはFRP捨てたって言ってた気がするので多分今のElmはもう論文にあるような仕組みで動いてないような気がしないでもない。 2章 背景 FRPにはClassical, Real-ti

はじめに Reason MLを最近始めました。よき。 Reason MLとは Reason MLとはOCamlにインスパイアされたAltJSの一種。見た目は型の付いたJSみたいな感じだけど実際はJSのsyntaxに寄せたML。 BuckleScriptというコンパイラ(この名前もどうなんという感じだけど)を使ってJSに変える。BuckleScriptはReason MLとOCamlをJSに変換するコンパイラであり、Reason MLとOCamlのいずれのsyntaxも混ぜて使うことができるっぽい。便利～。 実際に使うときはBuckleScriptの方のドキュメントもちゃんと読んでおく必要がある(似たような見た目のページだけど内容は違う)。BuckleScriptにはコンパイラ拡張みたいなものが載っておりそれを上手く使うことで生成されるJSを制御したりJS側の関数を読み込んだりするのでこの辺

2018年に静的解析をとにかく強力につけまくるのは多分あんまりコストに見合わないのでよくない じゃあ静的解析を窓から投げ捨ててよいかというとそれはただの愚行 (以下、静的解析を普通に使えてる人には自明なことしか言いません) 私が最初に静的解析の限界を感じたのは多分依存型で遊んでいたとき 依存型の力はすごくて、まぁそれもそのはず命題論理から述語論理に進んで元への言及ができるので見かけ上表現力はとんでもなく上がるわけです。例えば「ある方程式を満たす解のみを受け取って何かする」みたいな関数が型として表現できるようになる。 一見すると最強に見えるんだけどこれは実質定理証明をすることなので、制限の強い型をつければつけるほど実装で苦しむ羽目になるということを割とすぐ痛感することになった。 例えば head : Vect (Suc n) a -> a で長さ1以上のvectorの先頭を安全に取り出す関数

設計の話 設計の話です。 責務 責務、誰がその仕事を行うかということを考えましょうというのはまぁさんざん言われていることだけど実際大事だと思う。 テクニックとしては委譲だのなんだのとあるけど、結局は「その仕事はその人に任せて本当にいいの？」にYesと答えられる場合にのみその作業をそのモジュールなり関数なりクラスなりに任せましょうという話ですね。 層の分離 プログラムが行う仕事は通常いくつかのオペレーションを組み合わせて実現されるわけだけど、それらの重要度というのは普通は一様ではない。 仕事によってはドメインレベルにしっかり固定されそれ以外のオペレーションがあり得ないものもあるし、今は一旦こうして実装しておくがあとで高確率で置き換える必要があるとかそういうやつ。 例えば今はハードコードしているが設定ファイルから読み込んだ値にしたい、DBを切り替えたい、データの中身が変更したいとかそういう感じ

DI DIの重要性はここ数年で急速に高まってきている。 依存性が注入されたりとかそういうことはどうでもよくて、設計と実装を分けたい、人類はそれだけのために色々と工夫をこらし最終的にたどり着いたのがDIであったのだろう。 Haskellでも設計と実装を分けるためにDIしたいというのは自然な流れである。 ここでは型も含めて設計が実装に依存してはいけないということを要求する。 例えば設計でMySqlConnection、みたいな型が出現することも分離できていないので禁止とする。 問題点 設計を定義するときには他の言語ではインターフェイスなどの仕組みが使われることが多い。 Haskellには型システムという仕組みがあるのでこれがインターフェイス相当の機能として紹介される場合がある。 しかし型システムはインターフェイスとは違い、型を固定する仕組みがない。型クラス TypeClass a のインスタン

最近巷では俄に型システムについての言及が増え、型システムポエマーが増えてる気がするので自分もその時流に乗りたい。 完全にポエムだけどなんかあったら随時指摘ください。直します。 TL;DR 言いたいことはまとめると次 型システムは程度問題なのでちょうどいいところを探すべき 型は万能でも強さが正義でもない(だから未だに研究されてる) よく知りもしないくせに計算機科学を侮辱するのはやめろ 予防線 あくまでポエムですので中身はないです 私は型理論専攻で学位はとったものの研究者ではないのであまり信用しすぎないように 型システムの過去 型システムは大まかに次のような利点があるとされてきた(個人的主観) 「異常」なプログラムを検出する仕組み 静的解析による分かりやすいエラーメッセージ 型そのもののドキュメント性 IDEでのcompletionに貢献 最適化に貢献 (数学に正しく裏打ちされたsemanti

前提になりそうなことをちょこっとPreliminariesに書いた. Recursion schemes 以下, C は適当な条件を満たすfunctor F: C -> C がFixをもち, さらにそれがCofixにもなっていることを仮定する1. 以下ではこの適当な条件を満たすfunctorしか考えないものとする. catamorphism F-algebra p: FA -> A に対し, D のinitialityにより得られる射 cata(p): D -> A を catamorphism とよぶ. これは in; cata(p) = fmap F cata(p); p: FD -> A を満たす. anamorphism catamorphismの双対. F-coalgebra q: A -> FA に対し, D のterminalityにより得られる射 ana(q): A ->

Rustを使い始めて1ヶ月だぜ体験記みたいなのを書こうとしたけどせっかくなので今やってることも全部まとめて1本の記事にすることにした。 最近日本語をかくのがめんどくさい以外の発言をしていない気がする。 1ヶ月ほど前に動画編集ソフトを作りたくなって、言語はRust メディアフレームワークにGstreamer GUIにGTK+を使うのだけどこの3つをどれも触ったことがない状態で作り始めるという完全に勢いだけのアレというのが前置き。 前回の記事でも色々言ってたけどその後分かったことなんかを記しておく(本当はWHAT I WISH I KNEW WHEN LEARNING RUSTみたいにしてまとめると良いのだろうなぁ) とりあえずメモリモデルとしてはスタックとヒープがあるということだけ分かっておけば大丈夫そう structのフィールドに参照をもたせるとlifetime parameterにコード

Rustに入門して2週間くらい経ったぜ TL;DR Rustは普通に便利ないい言語 入門した 入門にあたってはプログラミング言語Rustを読んだ。これの翻訳版ぽい。 読んでRustに対して思ったこと: 読んだやつは古いドキュメントの翻訳版だったようで一部記述が古いっぽかった 構文はシンプルだけど必要なものは揃ってる感 ML風でADTもパターンマッチもあるしtraitもあって言うことナシでしょ 所有権とか借用とかそういう聞いたことあるワードは参照という概念に対するアレっぽい ｽｨｰ言語を気軽に(unsafe)呼べるのはFFIするとき良さそう 強そう マクロ割と便利そうな雰囲気ある RcとかArcとかCellとかいう便利なものがあるらしい あとBoxはいつ使うんじゃ 参照わかったようでわからない とりあえずスタックとヒープの違いは覚えたぞ 入門書なのに普通にするする読めてしまったし特に難しいこ

Hask圏 Haskellをラムダ計算とみなした時のsyntactic categoryをHask圏というのがよく言われる定義である(と思う)。 Haskellのtypeをobject, hom(A,B) をjudgement x:A |- M:B 全体(を適当な同値関係で割ったもの)とみなして圏を作る(このときしばしばjudgementとこのjudgementから作ったfunction λx.M を区別しない)。 さて基本的な結果として次のことが知られている。 Hask#Is Hask even a category? Hask is not a category というわけでHask圏は圏にならないのでそのようなものは存在しない。 Why not? これはundefinedというヤバイ元の存在とcall-by-needの悪魔的評価規則が合わさりこのような現象が生み出される。 主にこの2

Notes on Type Theory View the Project on GitHub myuon/nott Type Theoryについてのノートです. Current Version: 0.1.6.4 ノートのキリが良くなったところでtagを付けてmasterブランチに対してpushします. 作業中のノートはdevelopブランチに置いてあります. Table of Contents category.pdf: Category Theory (Preliminaries) preliminaries.pdf: Preliminaries untyped.pdf: Untyped lambda calculus simply.pdf: Simply-typed lambda calculus monad.pdf: Monadic lambda calculus etc ccc-

Blog Recent Articles 2020-12-27 - 2020年のお絵描きの進捗を振り返る 2020-05-02 - 日本語のTypographyの設定 2020-04-03 - Lightsailでやっていくサービス開発 2020-02-29 - GoとRustの言語比較記事を書くのが流行ってるらしい 2019-12-30 - 2019年を振り返って ...more on archives Tags adc2017 25 haskell 24 isabelle 14 定理証明 10 計算機科学 8 ラムダ計算 5 aws 4 rust 4 日記 3 reason 2 webサイト 2 ポエム 2 cg 1 frp 1 go 1 gstreamer 1 gtk 1 javascript 1 linux 1 ml 1 ブログ 1 環境構築 1 静的解析 1