OCamlの型検査は決定不能
1990年代から(少なくとも一部の人に)知られていることですが、OCamlの型検査は決定不能です。この文書では、ML系モジュールシステムにおけるシグネチャマッチングの仕組みを説明した後、OCamlの型検査器がどのように無限ループに陥るかを確認します。 シグネチャマッチングML系言語において、シグネチャは、モジュールのインターフェイスを表すために用いられます。あるモジュールが何らかのシグネチャに適合していることを保証するためにsignature ascriptionという機構があります。 Standard MLでは、M : SやM :> Sという風に書くと、モジュールMがシグネチャSに適合していることを保証できます。M : Sはtransparent signature ascriptionと呼ばれ、M :> Sはopaque signature ascriptionと呼ばれます。 シグネチ
OCaml - Language extensions
☰The OCaml languageThe OCaml languageLanguage extensions Chapter 12 Language extensions This chapter describes language extensions and convenience features that are implemented in OCaml, but not described in chapter 11.
GitHub - tomprimozic/type-systems: Implementations of various type systems in OCaml.
This repository contains implementations of different type systems in OCaml. It is meant to help out anyone who wants to learn more about advanced type systems and type inference or experiment by extending or implementing their own. The implementations are minimal and contain code that is (hopefully) simple and clear. algorithm_w contains one of the most basic yet efficient implementation of Damas
Flow | A static type checker for JavaScript
Code Faster.Tired of having to run your code to find bugs? Flow identifies problems as you code. Stop wasting your time guessing and checking. Code Smarter.It's hard to build smart tools for dynamic languages like JavaScript. Flow understands your code and makes its knowledge available, enabling other smart tools to be built on top of Flow. Code Confidently.Making major changes to large codebases
#001 多相再帰 - λx. x K S K ＠はてな
OCaml では，違う型で再帰する多相関数を書くことが難しい． 以下のデータ型 ('a,'b) twist を考える． type ('a,'b) twist = Nil | Cons of 'a * 'b * ('b,'a) twist 例えば，次の値はデータ型 (int,bool) twist を持っている．let twist_data = Cons(1,true,Cons(false,2,Nil)) このデータ型に対し，長さ（Consの個数）を求める関数を定義してみよう．let rec length = function Nil -> 0 | Cons(a,b,rest) -> 1 + length rest 関数 length の定義は自然のように思えるが，実際には ('a,'a) twist -> int という型が推論されてしまい，上記の twist_data には適用できない．
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - hsk/tapl
Types and Programming Languages
