ML のサブセットの型推論器を Coq で検証する - fetburner.core
この記事は言語実装 Advent Calendar 2020 の5日目の記事です． 一度でも型推論器を書いたことがあれば，そのあまりの邪悪さ，あるいはその複雑さに恐れ慄いたことでしょう． 参照を用いて単一化を実現しようものなら構文木は参照に汚染され，純粋関数型に実装しようものなら大量の型代入をどのような順序で適用したものか悩まされる． これは Hindley-Milner 型推論器を実装する上での宿命のようなものです． 本記事では，MLのサブセット——型付きλ計算をletと参照で拡張した，let多相をサポートする言語——の型推論器を Coq で実装し，その正当性を証明します． Coq で検証を行うことで我々は型推論器のバグへの恐怖とデバッグの労力から真に解放され，枕を高くして眠ることができることでしょう． もっとも、型付きλ計算を let 多相で拡張した言語の型推論器の正当性は実はすでに証
Menhir と ocamllex のサンプルコードをいくつか - Qiita
はじめに プログラムを書いていると、ちょっとした言語処理系を作りたくなることがあります。ちょっとした言語処理系を作ろうとしたとき、OCamlは良い選択肢です。何故良い選択肢なのかはよくわかりませんが、実際書いてみて快適でしたし、えらい人もそう言ってましたし、まあいいや、とにかく良い選択肢です。 しかし、素のOCamlで構文解析器や字句解析器を作るのはしんどいです。手を抜こうと思ったら構文解析器生成器Menhirと字句解析器生成器ocamllexを使うのが常套手段でしょう。 が、普通の人はそう頻繁に新しく言語処理系を作ったりしませんので、 Menhir や ocamllex の使い方を忘れがちです。こうなると困ります。例えば「半年ぶりに言語処理系を作りたい気分になっちゃった」というとき、「あれっ？ Menhir ってどう書くんだっけ？」となり、こうなると気分が重くなり、結果「言語処理系つくら
バージョンの充足可能性問題 | POSTD
(注：2017/02/06、いただいたフィードバックを元に翻訳を修正いたしました。修正内容については、 こちら を参照ください。) Dependency HellはNP完全ですが、この状況から脱却できるかもしれません。 パッケージにおけるバージョン選択の問題とは、完全である（全ての依存関係を満たしている）かつ互換性のある（互換性のない2つのパッケージが選択されていない）トップレベルパッケージPをビルドするために使われる依存関係の集合を見つけることです。ただし、菱形依存問題があるので、このようなセットは存在しない可能性があります。菱形依存問題とは、AはBとCが必要、BはDのバージョン2ではなくバージョン1が必要、CはDのバージョン1ではなくバージョン2が必要といったような問題のことです。この場合、Dの両方のバージョンを選択することはできないため、Aをビルドすることができないわけです。 パッケ
JavaScriptをOCamlから生成するトランスパイラ「BuckleScript 1.0」、米ブルームバーグがオープンソースで公開。TypeScriptよりタイプセーフかつ効率的で高速と
JavaScriptをOCamlから生成するトランスパイラ「BuckleScript 1.0」、米ブルームバーグがオープンソースで公開。TypeScriptよりタイプセーフかつ効率的で高速と 金融情報などの提供を行っている米ブルームバーグは、OCamlのコードからJavaScriptのコードを生成するトランスパイラ「BuckleScript 1.0」をオープンソースで公開しました。 BuckleScriptはTypeScriptやBabelJSなどからインスパイヤを得て開発されたと説明されていますが、最大の特徴はTypeScriptなどが独自の構文を備えているのに対し、BuckleScriptは既存の言語であるOCamlを採用しているところです。 OCamlはオブジェクト指向型と関数型の両方の特長を備え、特に海外では金融系システムの開発でよく使われているプログラミング言語です。 Buckl
Real World OCaml が出ました - camlspotter’s blog
一昨年から少しずつ書かれていた OCaml プログラミングの本、 Real World OCaml (以下 RWO)がついに public beta になり公開されました。 ( https://realworldocaml.org/beta1/en/html/ ) 版元の O'Reilly ではこのベータ版の状態の e-book が 今なら安く手に入ります。完全版には後から無料でアクセスできるように なるそうです。( http://shop.oreilly.com/product/0636920024743.do ) ！！！！！安く買いたい人は http://shop.oreilly.com/category/deals/early-release.do?code=WKERRLS をよく読んでね！！！！！ この本は、今まで外に伝わりづらかった OCaml プログラミングの最前線の一面を 伝
数理科学的バグ撲滅方法論のすすめ 第4回 関数型言語とオブジェクト指向，およびOCamlの"O"について
関数型言語とオブジェクト指向は相容れない，という説をよく聞く。たしかに「オブジェクトは状態を持つ」「関数型プログラミングでは，できるだけ破壊的代入を行わない」とすれば，二つの概念は矛盾しているようにも思われる。また，技術的観点以外にも，「とかくシンプルさを好む多くの関数型言語プログラマが，何かと物事を複雑にする（と思われている）オブジェクト指向を嫌っている」という面があるかもしれない。 しかし，個人の好き嫌いはさておき，実際問題として，関数型言語とオブジェクト指向は大いに関係がある。むしろ，基礎理論については，ほとんど同じコミュニティの人たちが取り組んでいる，と言ってもいい。例えば，以下のような研究が，1980年代から現在に至るまで行われている。 関数型言語のモデルであるλ計算という体系において，オブジェクトを表現する研究（参考リンクなど） λ計算にならい，（プロトタイプベースの）オブジェ
OCaml: 型注釈って面倒ですね。 - type t (* void *)
卒論で死にそうです。色々。 PPLのポスター発表に間に合うのでしょうか、その前に卒論発表会に間に合うのか…。 それはさておき、型注釈を色々見ていたら、MLも闇だなぁと思ってたのでちょっとメモしてみます。 追記の追記の追記： @camloebaさんにツッコミをいただきました。型注釈という言葉は不適切ということでした。 毎度ありがとうございます[´･_･`] @no_maddo 型注釈とは言わない。型制限と言う— 星のキャミバ様 (@camloeba) 2014, 2月 17 @no_maddo Parenthesized expressions can contain a type constraint, as in ( expr : typexpr ). それを type annotation と呼ぶところから間違いが始まります— 星のキャミバ様 (@camloeba) 2014, 2月
OCaml library : Printf
fprintf outchan format arg1 ... argN formats the arguments arg1 to argN according to the format string format, and outputs the resulting string on the channel outchan. The format string is a character string which contains two types of objects: plain characters, which are simply copied to the output channel, and conversion specifications, each of which causes conversion and printing of arguments.
OCaml 4.01.0 変更点 - camlspotter’s blog
スペルチェック 識別子のミスタイプがあった場合訂正を提案します: # List.lentgh ;; Characters 0-11: List.lentgh ^^^^^^^^^^^ Error: Unbound value List.lentgh Did you mean length? 個人的には、はあだから？と言った感じかと思っていたのですが、今のところスペルミスを指摘されるとそれはそれでうれしいことが判明しております。 Parser rewriter -ppx CamlP4 がヘビー過ぎて使えないという虚弱体質な人のために新しい -ppx という物が入りました。はっきり言うと P4 をマスターしている 人には機能が縮小されたものなので嬉しくありません。 まあ使い慣れた Parsetree のレベルでいじれるのが幸いですが… ocamlc -dsource コンパイラが受け取ったパース
OCaml 標準ライブラリ探訪 #1: Pervasives: 最も使われてるのに最も名前が知られていない奴 - camlspotter’s blog
関連リンク: OCaml 標準ライブラリ探訪 #0 標準ライブラリ探訪第一回は Pervasives です。 OCaml ソースファイルを持っている場合には ${srcdir}/stdlib/pervasives{.ml,.mli}、ライブラリディレクトリを見ている場合には ${libdir}/pervasives{.ml,.mli} *1 を見てください。 ところで、Pervasives って単語、知ってましたか？私はいまだに OCaml 以外でこの単語を見たことがありません。"pervert" じゃないですよ、"pervasives" です: Pervasives : [adj] 行き渡る、普及する、広がる傾向にある、(全面的に)広がる、拡散的な、広範囲な、まん延する 英辞郎 なんだかよくわかりませんね。でも、 Pervasives モジュールは OCaml で最もよく使われるモジュー
OCaml の let と let rec はなぜ別扱いになっているのか、決定版、もしくは OCaml 暦十何年だったか忘れたけど仕事で Haskell を一年使ってみた - camlspotter’s blog
はじめに断っておくが、全部Pros/Consのあるデザインチョイスなので、こうじゃなきゃいけないってことではない。ただ、 OCaml はこの選択をした、そいう事だ。 前回の「経験15年の OCaml ユーザーが Haskell を仕事で半年使ってみた」 http://d.hatena.ne.jp/camlspotter/20101212/1292165692 のような易しい文章ではないのでわからない人はとことん判らないだろう。まあ勘弁して欲しい。 あと、面倒だろうが、読む人は全部常体を敬体にして最後に「と思います」をつけて読んでくれ。ください、と思います。 Shadowing は便利であると思っている OCaml の let は非再帰なので以前定義された名前に別の値の束縛をオーバーライドできる。OCaml の人はこれが便利だと思っており皆普通に使っている。詳しくは http://d.hat
The Astrée Static Analyzer
Bruno Blanchet (Nov. 2001 — Nov. 2003), David Monniaux (Nov. 2001 — Aug. 2007), Laurent Mauborgne (Nov. 2001 — Aug. 2010). Astrée stands for Analyseur statique de logiciels temps-réel embarqués (real-time embedded software static analyzer). The development of Astrée started from scratch in Nov. 2001 at the Laboratoire d'Informatique of the École Normale Supérieure (LIENS), initially supported by t
syntax in OCaml
The "Unknown:"s below indicate that an entry is incomplete. either the entry exist in the language, and please tell. either the entry doesn't exist in the language, and please tell so. The entry will be marked as such and won't appear as missing anymore. Category: Object Oriented, Functional, Statically typed Various
GitHub - cohama/the-ocamlspot.vim: A wrapper Vim plugin for OCamlSpotter written in pure Vim Script.
Haskell厨を6年やってる俺がOCamlを仕事で2ヶ月使ってみた - keigoiの日記
Haskell Advent Calendar jp 2010のためのエントリです（17日目）． 6日目の id:camlspotterさんの 経験15年のOCaml ユーザーが Haskell を仕事で半年使ってみた に対するカウンター（になってるかどうか分からないですが）みたいな感じです． 近くて遠い隣人：HaskellとOCaml OCamlはHaskellと違って副作用があり，更にHM型推論をもつためプログラマは本質的な部分の記述に注力しつつ，コードのチューニングもできる． つまり働くHaskellプログラマがシリアスなソフトウェアを書く時に使えるほとんど唯一の選択肢だ．しかし，同じ静的型付けの関数型言語でありながら，OCamlとHaskellの見た目はかなり異なる． この記事では， HaskellプログラマがOCamlを使い始めると，どういうトラップにハマるかを書く． なかでも，
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://courses.cms.caltech.edu/cs134/cs134b/book.pdf
Real World OCaml
サービス終了のお知らせ
http://ocamloscope.herokuapp.com/
OCaml library : Index of modules