PrologコードをHaskellの型システムで書く

prologサンプルコードをふと書いてみる - ラシウラでのprologコード、eval.pl

%% example
%% consult(eval).
%% eval(nil, apply(lambda(x, ref(x)), 10), Result).

eval(Env, lambda(Arg, Body), closure(Env, Arg, Body)).
eval(Env, apply(Operator, Operand), Result) :-
        eval(Env, Operator, closure(CEnv, Arg, Body)),
        eval(Env, Operand, Val),
        ext(CEnv, Arg, Val, ExtEnv),
        eval(ExtEnv, Body, Result).
eval(Env, ref(Var), Result) :-
        get(Env, Var, Result).
eval(_Env, Const, Const) :-
        number(Const).

ext(OldEnv, Var, Val, cell(Var, Val, OldEnv)).

get(nil, _Var, not_found).
get(cell(Var, Val, _Rest), Var, Val) :- !.
get(cell(Name, _Val, Rest), Var, Result) :-
        Name \= Var,
        get(Rest, Var, Result).

とほぼ同等のことを、GHCの型システム上でも行うこともできる。

そのHaskellコードは以下のようになる(要GHC、要オプション)

{-# OPTIONS
  -XMultiParamTypeClasses
  -XFunctionalDependencies
  -XFlexibleInstances
  -XFlexibleContexts
  -fallow-undecidable-instances
  -fallow-overlapping-instances
#-}

-- name and equiv
data X = X
data Y = Y
data True = True
data False = False

class TEq a b result | a b -> result where
    teq :: a -> b -> result
    teq a b = undefined
instance TEq X X True
instance TEq X Y False
instance TEq Y X False
instance TEq Y Y True

-- constant values
data Zero = Zero
data Succ n = Succ n
type One = Succ Zero
type Two = Succ One
type Three = Succ Two
zero = undefined :: Zero
one = undefined :: One
two = undefined :: Two
three = undefined :: Three

data NotFound = NotFound

-- env and value getter
data ENil = ENil
data Env name value next = Env name value next

class Get env name value | env name -> value where
    get :: env -> name -> value
    get env name = undefined
instance Get ENil name NotFound
instance Get (Env name value next) name value
instance (TEq name oname False, Get next name value) =>
    Get (Env oname ovalue next) name value

-- tenv = undefined :: Env X Three (Env Y Two (Env X One ENil))
-- get tenv X :: Three
-- get tenv Y :: Two

class Ext env name value extenv | name value -> extenv where
    ext :: env -> name -> value -> extenv
    ext env name value = undefined
instance Ext ENil name value (Env name value ENil)
instance Ext env name value (Env name value env)

-- Terms
data Const value = Const value
data Ref name = Ref name
data Lambda arg body = Lambda arg body
data Apply operator operand = Apply operator operand

-- Values
data Closure env arg body = Closure env arg body

-- Eval
class Eval env term value | env term -> value where
    eval :: env -> term -> value
    eval env term = undefined
instance Eval env (Const value) value
instance (Get env name value) => Eval env (Ref name) value
instance Eval env (Lambda arg body) (Closure env arg body)
instance (Eval env operator (Closure cenv arg body),
          Eval env operand value,
          Ext cenv arg value extenv,
          Eval extenv body result) => Eval env (Apply operator operand) result

-- examples
exterm1 = undefined :: (Apply (Lambda X (Ref X)) (Const Three))
-- :t eval ENil exterm1 :: Three

このコードは、eval.hsとでも保存して、

$ ghci eval.hs
GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( eval.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t eval ENil exterm1
eval ENil exterm1 :: Three
*Main>

というように、結果にあたる部分が、型チェック/型推論により式の型として決まり、:tによって出せるようになる。

基本は、prologのpredicate部分を、classにして各パターンごとにinstanceを定義する感じ。定数やシンボルはdataやtypeで定義する。

classには結果部分がvalueの型になるような同名の関数を用意したり、dataやtypeにはデータコンストラクタや(値はundefinedになる)適当な式があると使いやすい。(式の値のほうは適当でもいいのが味噌。もちろん関数をきちんと定義すれば、値としても意味を成すものが取り出せるようになる。たとえば、例のeval TNil exterm1の場合に、(Succ (Succ (Succ Zero))) :: Threeを返す素直な実装ができる。しかし、この関数処理はプログラム実行時で出る値だが、型Threeは意味解析での型チェック/推論時に決定する違いがある。)

PrologとHaskell型システムとの対応付けは、applyをevalする部分を比較するとわかりやすいかも。

eval(Env, apply(Operator, Operand), Result) :-
        eval(Env, Operator, closure(CEnv, Arg, Body)),
        eval(Env, Operand, Val),
        ext(CEnv, Arg, Val, ExtEnv),
        eval(ExtEnv, Body, Result).

instance (Eval env operator (Closure cenv arg body),
          Eval env operand value,
          Ext cenv arg value extenv,
          Eval extenv body result) => Eval env (Apply operator operand) result

prologコードだとA :- B, C, ..となるものが、Haskellだとinstance (B, C, ...) => Aになるかんじで対応付けられる。

C++ template版

ほぼ同じものをC++ templateで静的に解くevalを書くと:

#include <string>
#include <iostream>
using namespace std;

// names
struct X {};
struct Y {};

// values
struct Ten {
  static string value;
};
string Ten::value = "10";
struct Nine {
  static string value;
};
string Nine::value = "9";
struct notfound {
  static string value;
};
string notfound::value = "not found";

template <typename Env, typename Param, typename Body>
struct closure {
  typedef Env env;
  typedef Param param;
  typedef Body body;
};

// expr
template <typename Val>
struct con {
  typedef Val value;
};
template <typename Name>
struct var {
  typedef Name name;
};
template <typename Name, typename Body>
struct lam {
  typedef Name param;
  typedef Body body;
};
template <typename Operator, typename Operand>
struct app {
  typedef Operator opr;
  typedef Operand opd;
};


// env
struct nil {};
template <typename Var, typename Val, typename Next>
struct cell {};

template <typename OldEnv, typename Var, typename Val>
struct ext {
  typedef cell<Var, Val, OldEnv> ret;
};

template <typename Env, typename Var>
struct get {};
template <typename Var>
struct get<nil, Var> {
  typedef notfound ret;
};
template <typename Var, typename Val, typename Rest>
struct get<cell<Var, Val, Rest>, Var> {
  typedef Val ret;
};
template <typename Var, typename Val, typename AVar, typename Rest>
struct get<cell<Var, Val, Rest>, AVar> {
  typedef typename get<Rest, AVar>::ret ret;
};

// eval
template <typename Env, typename Expr>
struct eval {};
template <typename Env, typename Val>
struct eval<Env, con<Val> > {
  typedef Val ret;
};
template <typename Env, typename Name>
struct eval<Env, var<Name> > {
  typedef typename get<Env, Name>::ret ret;
};
template <typename Env, typename Name, typename Body>
struct eval<Env, lam<Name, Body> > {
  typedef closure<Env, Name, Body> ret;
};
template <typename Env, typename Opr, typename Opd>
struct eval<Env, app<Opr, Opd> > {
  typedef typename eval<Env, Opr>::ret opr;
  typedef typename eval<Env, Opd>::ret opd;
  typedef typename opr::env env;
  typedef typename opr::param param;
  typedef typename opr::body body;
  typedef typename ext<env, param, opd>::ret extenv;
  typedef typename eval<extenv, body>::ret ret;
};

// examples
int main() {
  get<cell<X, Ten, cell<Y, Nine, nil> >, Y>::ret a;
  cout << a.value << endl;

  eval<nil, app<lam<X, var<X> >, con<Ten> > >::ret v;
  cout << v.value << endl;
}

書き方

データも関数も全部structにする

データ
- レコード型はtemplateに、メンバーは型パラメータにする
  - 取り出したい型パラメータは、それぞれtypedefでメンバーにしておく
  - cellのようにパターンマッチングでのみアクセスするデータには、メンバー不要
- データを表示したい場合は、その型に対応する何らかの値やC++関数をstaticメンバーにでも入れておく

関数/述語
- 引数を型パラメータにする
- 戻り値はメンバー名をretなど決めておいて、戻り値となる型をそのretにtypedefしてやる
- 途中の式や条件は、typedefで並べる

メンバーアクセス
- データメンバーや戻り値など、typedefしたメンバー型を使うときは、それをメンバーアクセスすればよい。ただ、メンバー型にアクセスするときtypenameをつける必要がある。

実行
- main中などで、計算したいものを型として記述しそのretメンバーのデータを作る
- 表示は結果の値型に対応する値メンバーを使う