型レベルプログラミングとTypeScriptとPureScript

導入

TypeScriptで型のループを計算する という記事で、TypeScriptでタプルの型を逆順にする方法が紹介されていました。これが非常に興味深く、この方法を応用すれば、以前断念していた型付リスト的なもののライブラリを作り直せるのではないかと思い、そのためにまずはPureScriptで同じものが作れるか調べてみよう、というのが今回の動機です。

TypeScriptで型のループを計算する で定義されているReverse総称型(ジェネリクス、多相型)を使うと、例えば要素数が3で、それぞれの要素の型が「文字列、数値、論理型」である

 [string,number,boolean]

というタプル型があった場合に、タプル内の型の並び順を逆にした型 Rを次のように構成することが出来ます。

 type R = Reverse<[string,number,boolean]>
 const r:R = [true, 123, "Hogehoge"];

（この例では、要素数を3としていますが、もちろん、任意の要素数で並び順を逆に出来ます）
Reverse総称型の実装は、TypeScriptの持つ条件型(Conditional Type)という強力な機能を用いて再帰的に定義されているのですが、本記事では、これと同様なことを、PureScriptで扱う方法について調べてみました。

なお、今回使ったコードはこちらにあります。

また、TypeScriptの総称型(ジェネリクス、多相型)　条件型(Conditional Type)については、TypeScriptの型入門やTypeScriptの型初級の記事がとても丁寧に説明されています。（大変参考にさせてもらいました）

問題点と解決方法

さて、TypeScriptと同じようなことをPureScriptで実現しようとすると、そのままでは難しく、いくつか問題が発生しました。

1. そもそも、TypeScriptのようなタプル型が用意されていない。
2. 型の演算においてTypeScriptのような条件型がなく、条件分岐が出来ない
3. 標準では、型はShowクラスのインスタンスになっていないので、確認が難しい

それぞれの問題について、次のように対応していくことにしました。

問題1の解決方法

まず、1の問題は、単純にData.Nested.Tuple を使うことにしました。見た目はだいぶ違いますが、TypeScriptで

  [string, number, boolean]  

という型は、PureScriptのData.Nested.Tupleでは、

  String /\ Number /\ Boolean /\ Unit

となります。（最後にUnitが必要なことに注意。これないと、最後がBoolean型なのか、最後がNumberとBooleanのタプルなのか区別出来なくなってしまうので）

問題2の解決方法

　次に、2の問題は、型クラスを使って代用することにしました。A, B, Cを型として

  (Reverse A/\B/\C/\Unit m)

とすると、m が C/\B/\A/\Unit という型であることを満たすように 型クラス Reverse を実装することにします。この場合、型クラス制約

  forall m. (Reverse A/\B/\C/\Unit m) => ...

は、mが C/\B/\A/\Unit という型であることを要求するようになります。

問題3の解決方法

最後に、3の問題ですが、TypeScriptの場合は、エディタ上の機能で型チェックすれば簡単に分かりました。PureScriptでもLanguage Serverを組み込めばいけるのかも知れませんが、私は普段使っていないので、PureScriptのコード内で、タプルの型を表示するユーティリティーを作成することにしました。この記事の本題ではないので、詳細は割愛しますが、こちら に ShowTuple.purs モジュールとして用意しました。

例えば、Int /\ String /\ Number /\ Unit というタプル型を表示するには

log $ show (TProxy :: TProxy (Int /\ String /\ Number /\ Unit))

とすれば、

(Int,String,Number)

と表示されるようになっています。

TProxy は、

data TProxy tupleType = TProxy

定義されていて、Showクラスのインスタンスにしてあります。

また、3.14 /\ "ABC" /\ 10 /\ unitというタプル値を表示するには

log $ show $ TupleView (3.14 /\ "ABC" /\ 10 /\ unit)

とすると、

(3.14,"ABC",10)

と表示されるようになっています。

TupleViewは、タプルをShowクラスのインスタンスにするためのnewtypeで、

newtype TupleView a b = TupleView (Tuple a b)

と定義しました。(タプル型のままだと、Orphan インスタンスになってしまい Showクラスのインスタンスに出来ないため）

実は、この表示処理を用意するのが結構大変だったのですが、、、。あまり面白いものではないと思うのと、エディタで簡単に確認出来る環境なら、そもそもこれらの機能は不要なので、割愛します。

Reverseクラス の実装

ここからが本題です。

Step 1

さて、いよいよ実装なのですが、まず、Reverseクラス を実装する前に、補助的な機能を持つ GoThroughクラスとそのインスタンスを実装します。これは何をするかというと、タプルの一番最初の要素を、一番最後に移動するような型クラスです。

つまり、

class GoThrough a b | a -> b

で定義されていて、aが A/\B/\C/\Unit 型だとすると、bは B/\C/\A/\Unit 型になるようにしたいのです。

これは、実は再帰的に簡単に実装することが出来ます。まず、要素数が2つのタプルに対するインスタンスであれば要素を入れ替えるだけです。

instance goThroughTwo :: GoThrough (x /\ y /\ Unit) (y /\ x /\ Unit)

そして、要素数が3つ以上のタプルに対するインスタンスであれば、再帰的に、y /\ rに対して、GoThroughを適用したもの zがすでに得らていると仮定して、y /\ x /\ rに対してはGoThroughを適用したものがx /\ zと定義すれば実現できます。

else instance goThroughMany :: 
  ( GoThrough (y /\ r) z
  ) => GoThrough (y /\ x /\ r) (x /\ z) 

Step 2

次に、GoThroughクラスを利用して、Reverseクラスとそのインスタンスを実装します。

このときも再帰的に考えると、かなりシンプルに実装することが出来ました。

まず、要素数が2のタプルに対するインスタンスであれば、単に要素を入れ替えるだけなので、

instance reverseTwo :: Reverse (x /\ y /\ Unit) (y /\ x /\ Unit)

です。また、要素数が3つ以上のタプルに対するインスタンスであれば、すでに rをリバースしたr'がReverseクラスで得られているとして、(a /\ r)をリバースしたものzというのは、r'の最後にaをくっつけたものz と同じです。しかも、r'の最後にaをくっつけたものzは、GoThrough (a /\ r') zで得られますので、結局、

else instance reverseMany ::
  ( Reverse r r'
  , GoThrough (a /\ r') z
  ) => Reverse (a /\ r) z

です。

以上より、Reverseクラスの定義は全体で、

module ReverseTuple
( class GoThrough
, class Reverse
) where

import Prelude (Unit)
import Data.Tuple.Nested (type (/\))

class GoThrough a b | a -> b

instance goThroughTwo :: GoThrough (x /\ y /\ Unit) (y /\ x /\ Unit)
else instance goThroughMany :: 
  ( GoThrough (y /\ r) z
  ) => GoThrough (y /\ x /\ r) (x /\ z) 

class Reverse a b | a -> b

instance reverseTwo :: Reverse (x /\ y /\ Unit) (y /\ x /\ Unit)
else instance reverseMany ::
  ( Reverse r r'
  , GoThrough (a /\ r') z
  ) => Reverse (a /\ r) z

となります。

動作確認

型のReverse

Reverseクラスを読み込み、(Int /\ String /\ Number /\ Unit)型の逆順に出来ているかを確認してみましょう。

  log $ show (TProxy :: forall m. (Reverse (Int /\ String /\ Number /\ Unit) m) => TProxy m)  

を実行すると、ただしく

(Number,String,Int)

と型の並びが逆になっていました。

型制約のチェック

Reverseは、型クラスなので

let tuple = 3.14 /\ "ABC" /\ 10 /\ unit :: (forall m. (Reverse (Int /\ String /\ Number /\ Unit) m))

とすることは出来ません。この意味ではPureScriptのReverse型クラスは、TypeScriptのReverse総称型のようには使えません。（たぶん、こういうのはPureScriptでは無理だと思いますが、、。もしかしたら、他に良い方法があるかも知れません。ご存知の方はぜひコメントください！）

その代わり、次のようにして、tuple が Number /\ String /\ Int /\ Unit型であることを保証することは出来ます。

  let tuple = (identity :: forall m. (Reverse (Int /\ String /\ Number /\ Unit) m) => m -> m)
               $ 3.14 /\ "ABC" /\ 10 /\ unit

(identity :: forall m. (Reverse (Int /\ String /\ Number /\ Unit) m) => m -> m) が型を保証していて、tuple には、Number /\ String /\ Int型しか代入することが出来ません。

念のため、次のように

  log $ show $ TupleView tuple

表示してみると、期待通り

(3.14,"ABC",10)

となっています。

まとめと感想

PureScriptで、タプルの型の順番を逆にする型クラスを実装してみました。型クラスを再帰的に利用することで、わりとコンパクトに実装することが出来たのではないかと思います。（とはいえ、分かりやすいとは言えないと思います。慣れかもしれませんが、、、）

それにしても、型クラスって、なんというか、論理型プログラミング言語のPrologっぽい書き方になるというか、そんな感じがしました。右辺で左辺を定義する、という形ではなくて、パターンを定義していく造りなので、慣れるまでにまだまだ時間がかかりそうです。

さて、これを試してみる間になんとなく思ったのですが、TypeScriptの型付きの値定義

const x:SomeType = someValue

は、PureScriptでいうところの型付の値定義

let x = someValue :: SomeType

と対応するというよりも、型制約をした上での値定義

let x = (identity :: forall m. (TypeEquals SimeType m) => m -> m) someValue

に近いのではないか？　という気がしました。何故なのか、というとうまく説明出来なくて、感覚的なものなのですが、、、。

TypeScriptもPureScriptも、静的な型を持つという意味ではよく似ているのですが、Curry Styleな型（あるいは外在的な型）と、Church Styleな型（あるいは内在的な型）の違いなのではないかなぁ、、、と思っています。

なお、Curry Style、Church Styleについては、Church vs Curry Typesの記事に詳しく書いてあるのですが、ちょっと私には難しかったので、もし良かったらコメントいただけると助かります！（またはどなたか解説記事を、、、）