[PureScript]Indexed Monad で変数を作りたい

最初に現状

まだ発展的なことはできないです．関数定義で詰まってしまったので，とりあえず記事を書いて整理します．

概要

変数を型レベルの文字列と見て，型安全に管理します(いわば変数の再実装)．実験的であり，実用的ではありません．
リポジトリ
https://github.com/yukikurage/typed-variable

どんな感じ

以下この「再実装した」プログラミング言語を仮にY言語と呼びます．(自分のユーザー名の頭文字であり，深い意味はありません)
Y言語にリテラルや関数を作る構文はない(そもそもリテラルに関しては"作る"とか無さそう)ので次のような感じで外界(PureScript)側から提供します．

_1 = ipure 1
_2 = ipure 2
_3 = ipure 3
_add = iliftA2 (+)

infixl 6 _add as (<+>)

リテラルはipure，n変数関数はiliftA{n}でY言語へ変換できます．(liftA{n}に関してはn毎に関数を用意しなければならない)
変数は型レベル文字列なのでProxyで用意しますが，いちいち書くのは面倒なので，_x, _yあたりを作っておきます．

_x = Proxy :: Proxy "x"
_y = Proxy :: Proxy "y"

Y言語本文は次のような感じです．

testExpr = Ix.do
  _x := _1
  _x @= read _x <+> _2
  _y := read _x <+> _3
  read _y

:=は変数定義です．_x := _1はxを定義し，xに1を代入してます．
@=は代入です．_x @ = {右辺}はxに{右辺}を代入してます．
readは変数から中身を読み取る関数です．したがって_x @= read _x <+> _2は，通常のプログラミング言語で言うところのx = x + 2 です．

最後のread _yがプログラムの結果となります．

全体としてこのプログラムはjavascriptで表すならば次のように働きます．

let x = 1
x = x + 2
let y = x + 3
// 最後にyを出力する(この部分はjavascriptで書けない)

したがって出力は6です．

外界からプログラムを走らせるにはrunExpressionを使います．

main :: Effect Unit
main = logShow $ runExpression testExpr

コンソールに6が出力されます．

型レベルで変数名を管理しているので次のようにするとちゃんと型チェックでエラーが出ます．

-- エラー: xが定義されていない
..
runExpression testExpr
..
testExpr = Ix.do
  _x @= _1

補足: runExpression testExprがなければ上のtestExprはエラーなく定義できます．これは，_xという変数があるもとではtextExprを実行することは出来るからです．runExpressionは対象が変数が空の状態から実行出来ることが保証されていないと実行できません．したがって_xを前提とするtextExprは実行できません．

-- エラー: xが重複して定義されている．
testExpr = Ix.do
  _x := _1
  _x := _2
  read _y

仕組み

以下がインポートされている状況です．

import Prelude

import Control.Applicative.Indexed (class IxApplicative, iapply, imap)
import Control.Apply.Indexed (class IxApply)
import Control.Bind.Indexed (class IxBind)
import Control.Monad.Indexed (class IxMonad)
import Data.Functor.Indexed (class IxFunctor)
import Data.Symbol (class IsSymbol)
import Prim.Row (class Cons, class Lacks)
import Record (get, insert, set)
import Type.Proxy (Proxy)

Expression型

プログラムそれ自体や，それぞれの式(_x := _1など)はExpression型を持っています．Expression型は次のように定義されています．

data Expression p q a = Expression 
  (Record p -> { variables :: Record q, result :: a })

ここで p, q は型レベル連想配列，(Row Typeカインドを持つ)です．Recordは型レベルコンストラクタRow Type -> Typeであり，Row Typeを値を持つ型に変換します．(詳しい説明は他記事にまかせます．)
ex) {x: 1, y: "hoge"} :: Record (x: Int, y: String)

Expressionは，変数一覧(::Record p)を取って，新たな変数の一覧(variables)と計算の結果(result)を格納したレコードを返す関数をくるんだものです．これは「変数を使った処理」を表すものです．

runExpression関数

runExpression :: forall p x. Expression () p x -> x
runExpression (Expression f) = (f {}).result

ruExpressionはプログラムを動かします．プログラムは変数が何もない状態から動くべきであるのでExpressionの第一引数は()です．

Indexed Monadのインスタンスにする

これによってdo記法を使ってY言語を構成したり，PureScriptのリテラル/関数をY言語のリテラル/関数に変換することができます．

instance IxFunctor Expression where
  imap f (Expression g) = Expression \r ->
    let
      { variables, result } = g r
    in
      { variables, result: f result }

instance IxApply Expression where
  iapply (Expression f) (Expression g) = Expression \r ->
    let
      { variables: v0, result: r0 } = f r
      { variables: v1, result: r1 } = g v0
    in
      { variables: v1, result: r0 r1 }

instance IxApplicative Expression where
  ipure result = Expression \variables -> { variables, result }

instance IxBind Expression where
  ibind (Expression f) g = Expression \r ->
    let
      { variables: v0, result: r0 } = f r
      Expression h = g r0
    in
      h v0

instance IxMonad Expression

ibindは複数のプログラムを合成して次に進める関数となっています．

ついでにiliftA2を実装します．

iliftA2 :: forall f x y z p q r. IxApplicative f => (x -> y -> z) -> f p q x -> f q r y -> f p r z
iliftA2 f x y = f `imap` x `iapply` y

iliftA3は次のように実装でき，その他のnについてiliftA{n}も同様です．

iliftA3 f x y z = f `imap` x `iapply` y `iapply` z

define関数(:=)

Y言語における変数を定義する関数です．

define
  :: forall s p q r x
   . IsSymbol s
  => Lacks s q
  => Cons s x q r
  => Proxy s
  -> Expression p q x
  -> Expression p r Unit
define s (Expression f) = Expression \r ->
  let
    { variables, result } = f r
  in
    { variables: insert s result variables, result: unit }

infix 2 define as :=

Lacks s qによって現在の文脈に_xが定義されていないことを保証します．
更にCons s x q rによって計算した後の変数群に_xが含まれていることが保証されます．

通常のプログラミング言語と違って，変数を定義する際に作った変数は捨てることができません(スコープという概念がなく，すべてグローバルになってしまう)．
すなわち，

testExpr = Ix.do
  _x := Ix.do
    _y := _1
    read _y
  read _y

のように_xを定義する際に使った_yを参照できます．

read関数

変数からリテラルを読み込む関数です．

read :: forall p q x s. Cons s x p q => IsSymbol s => Proxy s -> Expression q q x
read proxy = Expression \variables -> { variables, result: get proxy variables }

read前後で変数の一覧は変化しないのでExpressionの第一引数と第二引数は同じです．
resultにget関数で読み込んだ変数を渡すことで表現しています．

write関数(@=)

変数を上書きする関数です．

write
  :: forall p q r x s
   . Cons s x r q
  => IsSymbol s
  => Proxy s
  -> Expression p q x
  -> Expression p q Unit
write proxy (Expression f) = Expression \r ->
  let
    { variables, result } = f r
  in
    { variables: set proxy result variables, result: unit }
    
infix 2 write as @=

こちらにもスコープという概念はありません．

考察

変数の定義/代入それ自体を値として扱えることは，非同期処理などのプログラム自体をコントロールしなければならない時に役に立つかもしれません．
参考:
https://qiita.com/hiruberuto/items/98598af2b0e9a6206ef3
プログラムの中で自身のプログラムを型安全に組むことことができる時点で，なかなかおもしろい挙動です．

今後

まずはスコープの概念を実装してみたいです．具体的には型

Expression p q x -> Expression p p x

を持つ関数，つまり内部で定義された変数をすべて忘れるものです．これにより任意の場所でのスコープのつけ外しが可能となります．

しかし，かなり探しているのですが PureScript においてレコードからその部分的なレコードを取り出す関数が見つかりません．すなわち{x: 1, y: 2, z: 3}を{x: 1, y: 2}に変更するような関数です．

自前で実装するべきか，あるいはunsafecoerceで解決するか悩んでいます．(Union p q rでpのキーはすべてrのキーでもあることが保証出来るので，Record r型の値からRecord p型の値へのunsafecoerceは問題無いだろうと思っています．)