エンジニアのソフトウェア的愛情

または私は如何にして心配するのを止めてプログラムを・愛する・ようになったか

型システム入門

型システム入門 −プログラミング言語と型の理論−

型システム入門 −プログラミング言語と型の理論−

  • 作者: Benjamin C. Pierce,住井英二郎,遠藤侑介,酒井政裕,今井敬吾,黒木裕介,今井宜洋,才川隆文,今井健男
  • 出版社/メーカー: オーム社
  • 発売日: 2013/03/26
  • メディア: 単行本(ソフトカバー)
  • クリック: 68回
  • この商品を含むブログ (11件) を見る

本書の中の「第3章 型無し算術式」を「第4章 算術式のML実装」ではOCamlで実装しているのですが…


Ruby

パタンマッチングをするのに pattern-match という gem を利用しています。


実装。

require 'pattern-match'

=begin
| 構文での定義          | コード内での表現  |
|-----------------------|-------------------|
| true                  | :True             |
| false                 | :False            |
| if t1 then t2 else t3 | [:If, t1, t2, t3] |
| 0                     | :Zero             |
| succ t                | [:Succ, t]        |
| pred t                | [:Pred, t]        |
| iszero t              | [:IsZero, t]      |

`Kernel.#eval` が既に存在するので、`evaluate1`, `evaluate` にしています。
=end

def isnumericval(t)
  match(t) do
    with(:Zero) { true }
    with(_[:Succ, t1]) { isnumericval(t1) } 
    with(_) { false }
  end
end

def evaluate1(t)
  match(t) do
    with(_[:If, :TRUE, t2, t3]) { t2 }
    with(_[:If, :False, t2, t3]) { t3 }
    with(_[:If, t1, t2, t3]) { [:If, evaluate1(t1), t2, t3] }
    with(_[:Succ, t1]) { [:Succ, evaluate1(t1)] }
    with(_[:Pred, :Zero]) { :Zero }
    with(_[:Pred, _[:Succ, nv1]], guard { isnumericval(nv1) }) { nv1 }
    with(_[:Pred, t1]) { [:Pred, evaluate1(t1)] }
    with(_[:IsZero, :Zero]) { :TRUE }
    with(_[:IsZero, _[:Succ, nv1]],  guard { isnumericval(nv1) }) { :False }
    with(_[:IsZero, t1]) { [:IsZero, evaluate1(t1)] }
  end
end

def evaluate(t)
  begin
    evaluate(evaluate1(t))
  rescue PatternMatch::NoMatchingPatternError
    t
  end
end


こんな感じ。

p evaluate1([:If, :TRUE, [:If, :False, :False, :False], :TRUE]) # => [:If, :False, :False, :False]
p evaluate([:If, :TRUE, [:If, :False, :False, :False], :TRUE]) # => :False
p evaluate([:Pred, [:Succ, [:Succ, :Zero]]])


それ、( ) を [ ] に置き換えただけの Lisp じゃないの? とか言われそうでそうが…言われそう…。


C++ Templateで

パタンマッチングといえば、お約束の C++ Template プログラミングです。今回もやりました。

struct True {};
struct False {};
struct Zero {};

template<typename T1, typename T2, typename T3> struct If { typedef If<T1, T2, T3> type; };
template<typename T> struct Succ { typedef Succ<T> type; };
template<typename T> struct Prev { typedef Prev<T> type; };
template<typename T> struct IsZero { typedef IsZero<T> type; };

template<bool C, typename T, typename U> struct If_;
template<typename T, typename U> struct If_<true, T, U> { typedef T type; };
template<typename T, typename U> struct If_<false, T, U> { typedef U type; };

template<typename T> struct IsNumericVal { static const bool condition = false; };
template<> struct IsNumericVal<Zero> { static const bool condition = true; };
template<typename T> struct IsNumericVal<Succ<T>> { static const bool condition = IsNumericVal<T>::condition; };

template<typename T> struct IsVal { static const bool condition = IsNumericVal<T>::condition; };
template<> struct IsVal<True> { static const bool condition = true; };
template<> struct IsVal<False> { static const bool condition = true; };

template<typename T> struct Eval1 { typedef T type; };
template<typename T2, typename T3> struct Eval1<If<True, T2, T3>> { typedef T2 type; };
template<typename T2, typename T3> struct Eval1<If<False, T2, T3>> { typedef T3 type; };
template<typename T> struct Eval1<Succ<T>> { typedef typename Succ<typename Eval1<T>::type>::type type; };
template<> struct Eval1<Prev<Zero>> { typedef Zero type; };
template<typename T> struct Eval1<Prev<Succ<T>>> { typedef typename If_<IsNumericVal<T>::condition, T, Prev<Succ<T>>>::type type; };
template<typename T> struct Eval1<Prev<T>> { typedef typename Prev<typename Eval1<T>::type>::type type; };
template<> struct Eval1<IsZero<Zero>> { typedef True type; };
template<typename T> struct Eval1<IsZero<Succ<T>>> { typedef typename If_<IsNumericVal<T>::condition, True, False>::type type; };

template<typename T> struct Eval { typedef typename Eval<typename Eval1<T>::type>::type type; };


ここで次の式を評価(コンパイル)すると…

typedef typename Eval<If<True, If<False, False, False>, True>>::type t6;


これ以上評価のできないところまで評価が進みFalseが得られます。

error: no type named 'type' in 'Eval<False>'

ちゃんと「Falseの評価は存在しません」と表示されています(爆)。




…。

ごめんなさいごめんなさい。今回はここで力尽きました。