Linear PureScript

PureScript には Linear 型はないが既存の型システムでエミュレートできないか？

現状 : 若干できたが実用には堪えない

以下コード

module Linear
  ( LFunction
  , Linear(..)
  , app
  , appL
  , fin
  , lift
  , make
  , run
  , test
  , test2
  ) where

import Prelude

newtype LFunction a b = LFunction (a -> b)

newtype Linear :: forall k. k -> k -> Type -> Type
newtype Linear r s a = Linear a

infixr 0 type LFunction as -.

run :: forall a b. (a -. b) -> a -> b
run (LFunction f) = f

app :: forall a b. (a -. b) -> (forall r s. Linear r s a -> Linear r s b)
app (LFunction f) (Linear x) = Linear (f x)

appL :: forall a b r s. Linear r s (a -. b) -> (forall t. Linear s t a -> Linear r t b)
appL (Linear (LFunction f)) (Linear x) = Linear (f x)

appL' :: forall a b r s. Linear r s (a -. b) -> (forall t. Linear t r a -> Linear t s b)
appL' (Linear (LFunction f)) (Linear x) = Linear (f x)

make :: forall r s a b. (forall t. Linear t r a -> Linear t s b) -> Linear r s (a -. b)
make f = Linear (LFunction \a -> case f (Linear a) of Linear b -> b)

fin :: forall r a. Linear r r a -> a
fin (Linear a) = a

lift :: forall a. a -> (forall r. Linear r r a)
lift = Linear

subL :: Int -. Int -. Int
subL = LFunction \x -> LFunction \y -> x - y

{-
微妙な点 : appL と appL' を使い分ける必要がある
-}

-- 消費する順番が大切
test :: Int -. Int -. Int
test = fin $ make \x -> make \y -> app subL x `appL'` y

test2 :: Int -. Int -. Int
test2 = fin $ make \x -> make \y -> app subL y `appL` x

ゆきくらげ

なお、let などには対応していない

仕組み
Linear r s a において、 r と s が異なるような型は make の引数でしか作れない
また、消費するのは app と appL, app' のみであるので、make が引数にとる関数

forall t. Linear t r a -> Linear t s b

は、返り値を作るのに引数を一回だけ使っていることが保証されるはず（返り値に関係ない let 等は除く）

将来的に Linear の内部表現を Defer などにすれば let も使えるようになりそう

ゆきくらげ

バージョン2

Row を使って管理する

リソース（線形にとった引数）の名前を自分で決めなきゃいけないが、appL appL' 問題は解決した　割と使いやすいかも？

異なるリソースに別の名前とったらバグるだろと思っていたけどちゃんとコンパイルエラーは出してくれた　なんで？

module LinearR where

import Prelude

import Data.Symbol (class IsSymbol)
import Prim.Row (class Cons, class Nub, class Union)

-- Record を使った実装？

newtype LFunction a b = LFunction (a -> b)

newtype Linear :: Row Type -> Type -> Type
newtype Linear r a = Linear a

infixr 0 type LFunction as -.

run :: forall a b. (a -. b) -> a -> b
run (LFunction f) = f

mapL :: forall a b r. (a -. b) -> Linear r a -> Linear r b
mapL (LFunction f) (Linear x) = Linear (f x)

applyL :: forall a b r s t. Union r s t => Nub t t => Linear r (a -. b) -> Linear s a -> Linear t b
applyL (Linear (LFunction f)) (Linear x) = Linear (f x)

make
  :: forall @l r s t u a b
   . IsSymbol l
  => Cons l Unit () t
  => Cons l Unit r u
  => Cons l (Linear t a) () s
  => (Linear t a -> Linear u b)
  -> Linear r (a -. b)
make f = Linear (LFunction \a -> case f (Linear a) of Linear b -> b)

fin :: forall a. Linear () a -> a
fin (Linear a) = a

lift :: forall a. a -> Linear () a
lift = Linear

subL :: Int -. Int -. Int
subL = LFunction \x -> LFunction \y -> x - y

test :: Int -. Int -. Int
test = fin $
  make @"x" \x ->
    make @"y" \y ->
      subL `mapL` x `applyL` y

-- 次のやつはちゃんとコンパイルエラーになる
{-

test :: Int -. Int -. Int
test = fin $
  make @"x" \x ->
    make @"y" \y ->
      subL `mapL` x `applyL` x -- x の二回適用
-}

-- 同じ名前を付けても何故かうまくコンパイルエラーが出る　どこで出てるんだ？
{-
 Could not match type

    ( ... )

  with type

    ( x :: Unit
    ...
    )

test2 :: Int -. Int -. Int
test2 = fin $
  make @"x" \x ->
    make @"x" \y ->
      subL `mapL` x `applyL` lift 10
-}

ゆきくらげ

なんか適当に頑張ったら配列の書き換えみたいなのが動いた


main :: Effect Unit
main = do
  let Ur x = arrayTest
  log $ show x

arrayTest :: Ur (Array Int)
arrayTest = withArray [ 0, 1, 2 ] $ fin $
  make @"x" \arr -> freeze <$>. (set <$>. pureL 0 <*>. pureL 20 <*>. arr)

全部はここにあります

ゆきくらげ

↑let と同名リソース組み合わせると安全じゃない操作ができるようになってしまう