ツイッターでこういう話が出ていた（@nishio さん、面白いお題をありがとうございます！）： リテラル禁止FizzBuzz大会、開幕！(待て https://t.co/zpIirtNpmO— nishio hirokazu (@nishio) April 16, 2021 リテラルなしでFizzBuzz？出来らぁ！ class Fizz: d…

Logical Foundationsを進めがてら、基礎固め的に簡単な命題論理の命題を証明してみたいと思ってググったらこんなスレに遭遇した： coq.discourse.group このうちの最初の問題が簡単ながらもいくつか面白い点があったのでメモ。 証明する命題： Lemma a1 : fo…

このStack Overflow問答が大変面白かったのでメモ： stackoverflow.com サンプルコードは少し（自分にとっては）わかりやすいように変えてある。 何をしたいか 第一引数によって、それ以降幾つの引数をとるかが変化するような可変長引数関数を書きたい。 例…

OCamlの標準ライブラリは貧弱なことで知られている。 OCamlコミュニティの間でも「あれはOCamlコンパイラを書くためのライブラリだ」と言われていて、実際INRIAで必要最低限（つまりコンパイラを書くのに必要な分だけ）提供している側面がある。 基本的なデ…

Coqでソフトウェア工学の基礎をいろいろ証明するよという趣旨（多分？）のSoftware Foundationsというウェブ上で読める教科書シリーズがある。 softwarefoundations.cis.upenn.edu 第1巻Logical FoundationsはそのままCoqの教科書になっている。これを読み進…

ここまで zehnpaard.hatenablog.com zehnpaard.hatenablog.com zehnpaard.hatenablog.com とモジュール関連の機能で存在型を扱う話をしてきた。 しかし、OCamlでもっとも直接的に存在型をエンコードしたいならGADTが使える。 ダメな例 まずはうまくいかない…

シリーズ前々回と前回に続いて存在型を探っていく。 今回はパラメトリックな機構はまったく使わないただのモジュールと存在型について。 第１級モジュールやファンクタによる抽象化機能と存在型について書いてきたが、型としての「存在型」はどちらの場合で…

zehnpaard.hatenablog.com の続き。 前回は第１級モジュールを非常に綺麗に存在型に対応させられることが示せた。 しかし第１級モジュールを使わずとも、OCamlだとモジュールのシグニチャ自体が存在型的だ。（ただし微妙だが重要な差異もある） 今回はファン…

四月はCoqとClojureをやっていきたい— zehnpaard (@zehnpaard) March 27, 2021 というわけでemacsでcoq環境を整備したのでメモ。 インストールが必要だったもの： coq proof general spacemacs-coq 前提として spacemacs opam は入っているものとする（opam…

Types and Programming Languagesの24章の主題は存在型（Existential Types）である。 私は何回読んでもここでつまづく。 この章に到達するまでに部分型やら再帰型やら型推論やら全称型やら出てくるが、まあ難しくとも、なんとなくどういった言語機能に関連…

前回の記事で module type ADD = sig type t val add : t -> t -> t val to_string : t -> string (* ここ *) end のようなシグニチャを書いたが、書いていて「うーん、これはおかしいな」と思った。 MULでto_stringが必要だったからといってADDのインターフ…

Expression Problemという計算機科学・ソフトウェア工学の世界でそれなりに有名な問題がある。 この記事がいい感じにまとめていると思う： eli.thegreenplace.net Imagine that we have a set of data types and a set of operations that act on these type…

OCamlProのブログを過去に辿っていたらこういう記事を見つけた： www.ocamlpro.com OCamlの構文の１ページまとめと、標準ライブラリの２ページまとめ。（出たのは2019年9月） 流石に構文に関しては（Objects & Classes関連以外は）知らないところはなかった…

Chris HansonとGerald Jay Sussmanによる共著のSoftware Design for Flexibility（今後SDfFと略す）が昨日届いたので読み始めた。今は第二章を読んでいるところ。 Gerald Jay SussmanはStructure and Interpretation of Computer Programs（通称SICP)の共著…

Robert Harperのブログに（10年くらい前に）載っていたHaskellの型クラスに対する批判について@elpin1alさんに教えていただいたのでメモ。@elpin1al ありがとうございます！ 型クラスとモジュール 言語の抽象化機構の中心的存在は何かと考えると、Haskellな…

open recursionの記事に関して、より良い書き方があることに気づいたので書き留めておく。 あっちの記事ではシグニチャ二つを定義していて、GT.t = GT.s greet、NT.t = NT.s named greetと、GT.t型とNT.t型の形が違っていた： module type NT = sig type s t…

こういう記事を最近読んだ： tatta.hatenadiary.org （書かれたのは10年以上前だが） こういうコードは型チェック通らないよ、という話： let rec f x = x and g () = f 1 and h () = f true;; Line 3, characters 13-17: Error: This expression has type b…

なんとなく幽霊型がわかったので、その勢いに乗ってGeneralized Algebraic Data Typesについても調べてみた。 OCamlの言語機能としては： caml.inria.fr OCaml 4.00から導入された（ちなみに2021/3で最新版は4.12）とのことで、リリーススケジュールを見てみ…

open recursionなモジュールに型定義を持たせる（下） - Arantium Maestum のシグニチャ（シグネチャが正しいのか）についての話で module type S = sig type 'a t = 'a list end module M = struct type 'a t = int list end 的なコードを書いて「型が合わ…

最近のopen recursion関連記事を書いていてふと思い出したのがこちらの記事： camlspotter.hatenablog.com モジュールを使ったプログラミングではプログラマが情報を必要以上に減らしたモジュール型を書いてしまって 型の同値性が知らず知らずに失われてしま…

ようやくopen recursion関連の話もひと段落になる（予定）。それなりにしっかりOOP継承っぽい機能を実装する。 前回の記事では module GreetF(Self : GT) : GT with type t = Self.t and type ctor = Self.ctor = struct include Self let addressee _t = "w…

今回は今まで散々参考にしてきたこの記事の内容に近い形でopen recursionを実装してみる： blag.bcc32.com 題材もまったく同一なのでパクリと言われても仕方ない・・・ 前回までの記事の内容を踏まえて少し整理したり、スタイルをいじったりしてあるくらい。…

前回はこちらの記事の内容を非常に簡略化した実装を探ってみた： blag.bcc32.com 最大の簡略化ポイントはモジュール内でtype t = ...のような型定義がなされないところで、それによっていろいろなところでモジュール間の型の整合性を満たすための制約を明示…

前回の記事をツイートしたら@dico_lequeさんからこういう話を教えていただいた： 多相バリアントでのやり方を考えるとファンクタ経由で非再帰で書いておいてmodule rec M = F(M)みたいな、と思ってググったところOpen Recursion with Modules | bcc32https:/…

タイトルからも察していただいた方も多いと思うが、実用的な話はしません。あくまで「open recursionってなんだっけ」「こんな感じの開かれた再帰をOCamlで書いてみよう」という趣旨です。 Open Recursionってなんだ？ ソフトウェアデザイン誌の2021年3月号…

非常に限定された一部界隈では非常に有名なことで有名なTypes and Programming Languagesの公式サイトから、本に出てくる型システムの実装がダウンロードできる： www.cis.upenn.edu 以前も気になった部分を落として実装を覗いてみたりはしたのだが、コンパ…

私は趣味の言語処理系実装でocamllex/menhirというパーサジェネレータにお世話になることが多い。（このブログの過去記事を参照） js_of_ocamlは基本的にFFIを使わないライブラリだったらJavaScriptにコンパイルしてくれるはずなので、ブラウザでパーサが使…

OCamlでcanvasとLwtを使ってsnakeゲームを実装して、js_of_ocaml + duneでコンパイルしてみた： js_of_ocaml snake - compile to JS with command `dune build ./main.bc.js` · GitHub ポイントとしては ゲームロジックを比較的ステートレスな形でgame.mlに…

js_of_ocamlでゲームループ的なものを実装する方法を考えてみたい。 ゲームループというのは、特定の時間デルタごとに何らかの計算と出力が行われるようなコードのことだ。今回は例によって最小構成ということで、１秒ごとにコンソールに"hello"と出力してい…

前回、前々回に続いてjs_of_ocamlの話。今回はDOM要素をコード側で作成する。 だいたいの元ネタはjs_of_ocaml公式サンプルのこれ： https://github.com/ocsigen/js_of_ocaml/blob/master/examples/minesweeper/main.ml ただし、この記事ではCanvas要素を作成…