TypeScript で GADT っぽいの

TypeScript で Haskell にあるような GADT (Generalized Algebraic Data Type) っぽいものをどう表現できるかという話.

GADT を使いたくなる例

式をデータとして表現したいことありますよね. あると言ってくれ.

例えば数値と数値上の関数, そして関数適用がある式を考えます. 素朴に表現すると以下のようになるでしょう.

type Expr =
  | { type: "num", val: number }
  | { type: "fun", val: Fun }
  | { type: "app", fun: Expr, arg: Expr };
type Fun = (x: number) => number;

いちいちオブジェクトリテラルを書くのは面倒なのでコンストラクタを作っておきます.

const num = (val: number): Expr => ({
  type: "num", val
});
const fun = (val: Fun): Expr => ({
  type: "fun", val
});
const app = (fun: Expr, arg: Expr): Expr => ({
  type: "app", fun, arg
});

これらを使うと以下のように式を書けます.

const expr = app(
  fun(x => x * 2),
  num(42)
);

式があればその値を評価してやるのが人情というものでしょう. 式を評価する関数を書いてみます.

const evalExpr = (expr: Expr): number | Fun => {
  switch (expr.type) {
    case "num":
      return expr.val;
    case "fun":
      return expr.val;
    case "app": {
      const fun = evalExpr(expr.fun);
      const arg = evalExpr(expr.arg);
      if (typeof fun !== "function") {
        throw new Error("function is expected");
      }
      if (typeof arg !== "number") {
        throw new Error("number is expected");
      }
      return fun(arg);
    }
  }
};

これを使って上で定義した式を評価してみると, 無事期待した値が得られます.

const r = evalExpr(expr);
console.log(r); // 84

ところが Expr の定義上, 不正な式 (= 評価時にエラーが発生してしまう式) も書くことが出来てしまいます.

const invalidExpr = app(
  num(666), // !?
  num(42)
);
evalExpr(invalidExpr); // Error: function is expected
const invalidExpr = app(
  fun(x => x * 2),
  fun(x => x + 1) // !?
);
evalExpr(invalidExpr); // Error: number is expected

かといって, 単純に app の第 1 引数を fun, 第 2 引数を num のように制限するだけでは, 次のような正しく評価されるはずの式も書けなくなってしまいます.

const expr = app(
  fun(x => x * 2),
  app(
    fun(x => x + 1),
    num(42)
  )
);
const r = evalExpr(expr);
console.log(r); // 86

このような正しい式はすべて許容しつつ, 不正な式は弾く, ということを静的に型の力で行えないか, というのが GADT を使うモチベーションです.

GADT っぽいのに挑戦してみる (失敗)

まずは Expr が評価された結果の型 (A) を含むようにしてみましょう. これでひとまず app が持っている関数 fun と引数 arg の型が何であるべきかがはっきりしました.

type Expr<A> =
  | { type: "num", val: number }
  | { type: "fun", val: Fun }
  | { type: "app", fun: Expr<Fun>, arg: Expr<number> };
type Fun = (x: number) => number;

これだけでは numfun が評価された時にどのような値になるかわからないので, コンストラクタで型を指定してこれを表現するようにしてみます.

const num = (val: number): Expr<number> => ({
  type: "num", val
});
const fun = (val: Fun): Expr<Fun> => ({
  type: "fun", val
});
const app = (fun: Expr<Fun>, arg: Expr<number>): Expr<number> => ({
  type: "app", fun, arg
});

さて先ほどの評価時にエラーになってしまう式はどうかというと, 残念ながら依然書けてしまいます.

const invalidExpr = app(
  num(666), //No errors
  num(42)
);

これはなぜかというと, TypeScript の型定義は単にエイリアスを定義しているだけなので, もし定義時に A が右辺に出現しなければ, 定義した型を使ったときには A は完全に抜け落ちてしまうのです.

さらに悪いことに, evalExpr を定義しようとしても型をうまく合わせることができません.

const evalExpr = <A>(expr: Expr<A>): A => {
  switch (expr.type) {
    case "num":
      return expr.val; // error: Type 'number' is not assignable to type 'A'.
    case "fun":
      return expr.val; // error: Type 'Fun' is not assignable to type 'A'.
    case "app": {
      const fun = evalExpr(expr.fun);
      const arg = evalExpr(expr.arg);
      return fun(arg); // error: Object is of type 'unknown'.
    }
  }
};

というわけでこれは失敗.

GADT っぽいのに挑戦してみる (成功)

ではどうするとうまく表現できるでしょうか.

まずは不正な式を書けないようにするためには, Expr<A> の定義の右辺に A を出現させることが必須です. それに加えて, evalExpr をうまく定義するためには, 多相に定義した evalExpr の中で式の種類を絞り込んだ時に, 型についてもそれに応じた扱いができるようにする必要があります.

これらを満たすような定義として, 以下のようなものが考えられます.

type Expr<A> =
  | { type: "num", val: number, t: (x: number) => A }
  | { type: "fun", val: Fun, t: (x: Fun) => A }
  | { type: "app", fun: Expr<Fun>, arg: Expr<number>, t: (x: number) => A };
type Fun = (x: number) => number;

ここで tA を含むことで一つ目の条件を満たしつつ, 型変換を行う関数になっていることで二つ目の条件も満たすようになっています. やっていることは Haskell において GADT を使うと型の等価性の制約が付与される (参考) のとおおよそ似たようなもので, ここではそれに準じたものを手で書いているというだけです.

コンストラクタは次のように定義できます. t には最も自然なものとして恒等関数 id を設定しています.

const id = <T>(x: T): T => x;
const num = (val: number): Expr<number> => ({
  type: "num", val, t: id
});
const fun = (val: Fun): Expr<Fun> => ({
  type: "fun", val, t: id
});
const app = (fun: Expr<Fun>, arg: Expr<number>): Expr<number> => ({
  type: "app", fun, arg, t: id
});

まずは不正になる式を書いてみると, 以下のようにきちんと型エラーが報告されます.

const invalidExpr = app(
  num(666), // Error: Argument of type 'Expr<number>' is not assignable to parameter of type 'Expr<Fun>'.
  num(42)
);

続いて evalExpr を定義してみましょう. これは t を使って型変換することでつつがなく書くことが出来ます.

const evalExpr = <A>(expr: Expr<A>): A => {
  switch (expr.type) {
    case "num":
      return expr.t(expr.val);
    case "fun":
      return expr.t(expr.val);
    case "app": {
      const fun = evalExpr(expr.fun);
      const arg = evalExpr(expr.arg);
      return expr.t(fun(arg));
    }
  }
};

const expr = app(
  fun(x => x * 2),
  num(42)
);
const r = evalExpr(expr);
console.log(r); // 84

よかったですね. よかったですね と めでたし 以外の締め方を知らない.