Tagless final, First-class module, Modular implicit

はじめにこれは ML Advent Calendar 2017 の 19日目の記事です．最近 Typed final (tagless-final) style を読みました。このレクチャーノートではサンプルコードとして Haskell で型クラスを用いたものと OCaml でファンクターを用いたものが示されてい…

2016-12-17

プログラミング言語 idris

これは Theorem Prover Advent Calendar 2016 17日目の記事として書かれました. idrisは依存型を持つ純粋関数型プログラミング言語です. ちなみにアイコンはこんな感じ. *1 今月の初め, バージョン 0.99 がリリースされました. 機能もほぼ安定したといことで…

2016-09-08

LLVMのOCaml bindingをためす

前からLLMVが気になっていて, きつねさんの本をざっと読んだりしたが手を動かしてなかったのでチュートリアルをやることにした. LLVM Tutorial: Table of Contents — LLVM 3.8 documentation 古いチュートリアルだということは知っていたが他にないので仕方…

2016-03-09

ラムダ計算の評価器とBöhm tree

気持ち『きつねさんでもわかるLLVM』を読んだので何か書いてみようと思い, 一回書いておくかというのもあってラムダ計算の評価器を書くことにしました. 書いた結果, LLVMを使っても仕方ないことに気がついた(遅い！) のでLLVMはつかっていません. ついでにB…

2015-07-19

Billiard-ball computer

Billiard-ball Computerという計算モデルがあると知った。 Billiard-ball computer - Wikipedia, the free encyclopedia ボールの存在で1と0をあらわし、うまく衝突させることで論理回路を作るというものである。チューリング完全性があるらしい。具体的には…