遊ぶ金ほしさに、先月から HERP の業務委託を受け働きはじめました。
19ヶ月ぶりの労働は体にしみます。
まずは週3日の労働から。
多相からプログラミング言語を見る
こんにちは。ホビー型システミストの岡本です。
最近 C++ の習得をしていて、なんとなく多相（polymorphism）の視点からいくつかのプログラミング言語をまとめてみようという気になったので書いてみます。
部分型多相（subtype polymorphism）
クラスベースオブジェクト指向言語でよく使うのは部分型多相ですかね。
Java や C#・C++ にある、名称的部分型多相（nominal subtype polymorphism）はこんな感じ。次の例は Java です。
class A {} class B extends A {} public class Main { public static void main(string[] args) { A foo = new B(); } }
変数 foo は A 型だけど、型（クラス）B は A の部分型（サブクラス・派生クラス）なので、foo は B 型の値に束縛することができます。
C や Haskell にはこれはありませんね。ML 系言語もないのかな。
部分型多相には名称的の他に構造的部分型多相があります。次の例は TypeScript です。
class A { public readonly foo: number; public constructor(foo: number) { this.foo = foo; } } class B { public readonly foo: number; public readonly bar: string; public constructor(foo: number, bar: string) { this.foo = foo; this.bar = bar; } } const bar: A = new B(0, "");
型 B が A の部分型であると明記していませんが、B は A として扱うに足るフィールドを持つので A として扱うことができます。
構造的部分型多相は TypeScript や Go にあります。
静的なダックタイピングと見ることもできるかも。
PureScript にある列多相（row polymorphism）も構造的部分型多相の一種なのかな。こっちは余分なものがあるということを r で明記していますが。
foo :: { name :: String, age :: Int } foo = { name: "foo", age: 0 } name :: forall r. { name :: String | r } -> String name p = p.name name foo
パラメーター多相（parametric polymorphism）
パラメーター多相は Java・C#・C++ でそれぞれジェネリクス・ジェネリック・テンプレートと呼ばれるものです（C++ のテンプレートはちょっと違うかも）。
恒等関数を Java・C#・C++・Haskell で書くと次のような感じ。
<T> T id(T value) { return value; }
T Id<T>(T value) { return value; }
template<typename T> T id(T value) { return value; }
id :: a -> a id a = a
一般的には型変数になった型（上記でいう T や a）に関する性質は使えません。T や a にはどんな型も来られるようにしないといけないためです。性質を使いたい場合は後述します。
アドホック多相（ad-hoc polymorphism）
例えば + 演算子について Int -> Int -> Int という型としても使いたいし Double -> Double -> Double としても使いたく、そして実装が違う、という場合に出てくるのがアドホック多相です。
Java・C#・C++ だとオーバーロードと呼ばれます。Haskell だと型クラスで、他言語だと同様のものはトレイトやプロトコルなどと呼ばれるようです。
std::string hello(int a) { return std::to_string(a); } std::string hello(std::string a) { return a; }
class Hello a where hello :: a -> String instance Hello Int where hello = show instance Hello String where hello = id
アドホック多相が他の多相と組み合わさると、どの実装が選ばれるのかのアルゴリズムを知るために言語仕様を読むはめになってちょっとやっかいです（個人の感想）。
オーバーロード
Java・C# のオーバーロードは機能がちょっと弱くて返り値に関する多相にできません。
C++ でもストレートにはできませんが、テンプレートを使って実現できます。基本的にパラメーター多相のためのテンプレートですが、アドホック多相にも使うというのがややこしいところ。
#include <climits> int max() { return INT_MAX; } long int max() { return LONG_MAX; } // prog.cc:19:10: error: ambiguating new declaration of 'long int max()' // 19 | long int max() { return LONG_MAX; } // | ^~~ // prog.cc:18:5: note: old declaration 'int max()' // 18 | int max() { return INT_MAX; } // | ^~~
#include <climits> template<typename T> T max(); template<> int max<int>() { return INT_MAX; } template<> long int max<long int>() { return LONG_MAX; }
型クラス
型クラスのコードはパラメーター多相を使ったコードに変換することができます。下記は Haskell での例です。
{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances #-} main :: IO () main = do putStrLn $ hello (0 :: Int) putStrLn $ hello "Job" putStrLn $ hello' fooDictInt 0 putStrLn $ hello' fooDictString "Job" -- 型クラスを使ったコード class Foo a where foo :: a -> String instance Foo Int where foo = show instance Foo String where foo = id hello :: Foo a => a -> String hello a = "Hello, " ++ foo a ++ "!" -- パラメーター多相に変換したコード data FooDict a = FooDict { foo' :: a -> String } fooDictInt :: FooDict Int fooDictInt = FooDict { foo' = show } fooDictString :: FooDict String fooDictString = FooDict { foo' = id } hello' :: FooDict a -> a -> String hello' FooDict { foo' = f } a = "Hello, " ++ f a ++ "!"
実際 Haskell のデファクトスタンダードのコンパイラーである GHC は型クラスを上記のように脱糖します。Int に関する Foo のインスタンスは一意に決まるので fooDictInt を自動的に挿入できるという寸法です。この辞書を暗黙に挿入するので Scala ではインプリシットパラメーターというらしいです。
多相の組み合わせ
先述したパラメーター多相のパラメーターを性質で制限したい場合について記述します。それにはアドホック多相を採用する言語と部分型多相を採用する言語があります。
パラメーターを部分型多相で制限する
部分型多相で制限する場合は「特定の型の部分型でないといけない」というように制限します。Java や C# などがそうです。下記は Java の例です。
public class Main { public static <T extends Hello> String greet(T target) { return target.hello() + "!"; } } interface Hello { String hello(); }
T は Hello の部分型であることが保証されるので target.hello が呼べるわけですね。
パラメーターをアドホック多相で制限する
型クラスで制限する場合は「特定の型クラスを実装している型でないといけない」というように制限します。Haskell などがそうです。下記は Haskell の例です。
greet :: Hello a => a -> String greet a = hello a ++ "!" class Hello a where hello :: a -> String
a は Hello 型クラスを実装していることが保証されるので hello が呼べるわけです。
C++ の場合はちょっと変わっていて関数を使用すると暗黙にその関数の存在が要求されるようです。次のコードは、Java や C# と違ってエラーなくコンパイルできます。
#include <string> template<typename T> std::string greet(T target) { return hello(target) + "!"; }
std::string hello(int) のない int について greet(0) のように呼ぶとエラーになります。
int main() { std::cout << greet(0) << std::endl; } // prog.cc: In instantiation of 'std::string greet(T) [with T = int; std::string = std::__cxx11::basic_string<char>]': // prog.cc:10:25: required from here // prog.cc:5:17: error: 'hello' was not declared in this scope; did you mean 'ftello'? // 5 | return hello(target) + "!"; // | ~~~~~^~~~~~~~ // | ftello
ここで下記のような std::string hello(int) を用意してやるとエラーが解消されます。
std::string hello(int n) { return std::to_string(n); }
暗黙の型クラスのようなものが要求されていると見ることもできます。これが C++ 20 のコンセプトなのかな？
他の多相
線形型があると線形性に関する多相とか他にもいろいろあるだろうけどよく知らないのでこの辺で。
GHC 演算子優先順位トリビア
GHC の演算子の優先順位には -1 がある（たぶん組込でしか使えない #Haskell pic.twitter.com/Xa0OIjvw5i
— o̞͑kä̝mo̞͑to̞͑ kä̝zʊ̠kɪ̟ (@kakkun61) January 3, 2021
Case Analysis 関数
今回は case analysis と呼ばれる関数の話です1。
data D a b c = C0 a b | C1 c
例えば上記のようなデータ型があった場合 case analysis 関数は次のようになります。
d :: (a -> b -> d) -> (c -> d) -> D a b c -> d d f _ (C0 a b) = f a b d _ f (C1 c) = f c
値構築子の数だけ関数を引数とし、対象のデータを最後の引数とします。それぞれの関数の型は値構築子の型に似ます。
C0 :: a -> b -> D a b c C1 :: c -> D a b c d :: (a -> b -> d) -> -- C0 の型から決まる (c -> d) -> -- C1 の型から決まる D a b c -> -- 対象のデータ型 d
使い方としては case 式でのパターンマッチの代わりにワンライナーとして使うことが多いです。次の2つのコードは等価です。
case v of C0 a b -> f a b C1 c -> g c
d f g v
base にある case analysis 関数としては次のようなものがあります。
Data.Bool.bool :: a -> a -> Bool -> a Data.Maybe.maybe :: b -> (a -> b) -> Maybe a -> b Data.Either.either :: (a -> c) -> (b -> c) -> Either a b -> c Data.List.foldr :: (a -> b -> b) -> b -> [a] -> b -- 実際は多態、構築子と引数の順番が反対
-
case analysis の名前は
boolやeitherのドキュメントで使われています。eliminator 派もあるようです。↩
続・刹那的純粋関数的データ構造と線形型
The English version is at Dev.
前回の記事の追加情報です。
pure 抜け道はなかった
まあ、こういうインターフェースでありがちな
pureで外に出す抜け道が存在するのですが。
最後にこういうことを無思慮に書いたわけですが、Dev に書いた英語版を Reddit に載せたところ有益な情報を教えてもらえました。
I think the solution to the problem with
emptymight be to use theUr(for "unrestricted") datatype from linear-base:
empty :: (Queue a #-> Ur b) #-> Ur bTrying to run
empty Urshouldn't typecheck, because theUrconstructor is not linear. This seems to be an idiom used in other places of linear-base.
継続の返り値を Ur にすることで Queue を外に出せなくなります。Ur :: a -> Ur a に渡すと何回も使われるかもしれないため1回しか使えない Queue は渡すことができません。なるほどー。
CPS にしなくてよかった
生成する関数（ここでは empty）以外は CPS にしなくていいことに気付きました。
線形関数の中でその引数に別の線形関数を適用するとその返り値にも線形性が付くようです。この辺りちゃんと型付け規則を確認しないとな。
idl の返り値の a も1回しか使えないという性質を引き継いでるんだな。まあそうじゃないと困るが。 pic.twitter.com/PoZCkWkO5e
— o̞͑kä̝mo̞͑to̞͑ kä̝zʊ̠kɪ̟ (@kakkun61) December 21, 2020
つまり、empty の継続 Queue a #-> Ur b の中で enqueue などを呼ぶとその返り値も1回しか使えないわけなので、enqueue などは CPS にしなくてよかったです。逆に null の Bool は何回使ってもいいので Ur でくるみます。
null :: Queue a #-> (Ur Bool, Queue a) null (Queue l m) = (Ur (P.null l), Queue l m) enqueue :: a -> Queue a #-> Queue a enqueue a (Queue l m) = check l (a:m) dequeue :: Queue a #-> (Ur (Maybe a), Queue a) dequeue (Queue (a:l) m) = (Ur (Just a), check l m) dequeue (Queue l m) = (Ur Nothing, Queue l m)
そんなわけで使用感としてはこんな感じになりました。let 式が使えるなら見やすいのですが。
it "empty → enqueue → dequeue" $ do let f :: Queue Int #-> Ur Int f q = enqueue 0 q PL.& \q -> dequeue q PL.& \(Ur (Just a), q) -> q `lseq` Ur a Ur a = empty f a `shouldBe` 0
刹那的純粋関数的データ構造と線形型
The English version is at Dev.
『純粋関数型データ構造』（以降 PFDS）の5.2章に刹那的純粋関数的キューというものが出てきます。
asciidwango.jpこのキューは計算量の関係から1つの値に対して1回しか操作をしてはいけません。例えば下記操作列なら大丈夫ですが、その次の操作列では計算量が大きくなる可能性があります。
-- よい例 ops = let q0 = empty q1 = enqueue 0 q0 q2 = enqueue 1 q1 Just (a, _) = dequeue q2 in a
-- ダメな例 ops = let q0 = empty q1 = enqueue 0 q0 q2 = enqueue 1 q1 q2' = enqueue 2 q1 -- q1 を2回使っている Just (a, _) = dequeue q2 Just (b, _) = dequeue q2' in (a, b)
この1回しか操作してはいけないという性質を線形型で守れないか、というのがこの記事の主題です。
GHC の線形型については前回の記事を参考にしてください。
実装
GHC での線形型は線形関数（linear arrow）1として実装されているため、操作は継続渡しスタイルで実装していきます。例えば empty は下記のような型になります。
empty :: (Queue a #-> b) #-> b
継続の型が Queue a #-> b となっているのでこの関数の中では引数の Queue a 型の値は1回しか使えません。型検査器が検査してくれます。
そんなこんなで実装すると下記のようになります。計算量については PFDS を参照してください。
{-# LANGUAGE GADTs #-} {-# LANGUAGE LinearTypes #-} {-# LANGUAGE Strict #-} data Queue a where Queue :: [a] -> [a] -> Queue a deriving (Show) empty :: (Queue a #-> b) #-> b empty f = f (Queue [] []) null :: Queue a #-> Bool null (Queue l _) = Prelude.null l enqueue :: a -> Queue a #-> (Queue a #-> b) #-> b enqueue a (Queue l m) f = f (check l (a:m)) dequeue :: Queue a #-> (Maybe (a, Queue a) #-> b) #-> b dequeue (Queue (a:l) m) f = f (Just (a, check l m)) dequeue (Queue _ _) f = f Nothing check :: [a] -> [a] -> Queue a check [] m = Queue (reverse m) [] check l m = Queue l m
Queue を GADT を使って実装しているのは null のような関数を実装するためで GADT を使わなければ Queue l m の l や m も再帰的に「1回使う」という制約（線形性）が付くため _ でマッチすることができません。線形型版の null があったとして null l && null m と書けたとしてもリストに対しても再帰的に線形性を求められるため結局リストの構造を全部たどることになります。
ただ、この実装だと困ったことがあって、線形型では1回は使わないといけないため Queue a の値を消すことができません。返り値にしないといけなくなります。そこで前回の記事にも出てきた Consumable 型クラスの consume で消費できるようにインスタンスにします。
instance Consumable a => Consumable (Queue a) where consume (Queue l m) = l `lseq` m `lseq` ()
さてこれで使えるようになりました。
> import Prelude.Linear (lseq) > import Data.Queue.Ephemeral > empty (\q0 -> enqueue 0 q0 (\q1 -> dequeue q1 (\(Just (a, q2)) -> q2 `lseq` a))) :: Int 0
……いや、確かに使えるか使えないかで言ったら使えますが、使いやすいか使いにくいかで言ったら使いにくいですね？
継続モナド
継続渡しスタイルならモナドにすることができるため do 記法を使って読みやすくすることができます。
さて線形型版でもできるのでしょうか？やってみましょう。……（3日が経過）できました！全文はリポジトリーを見ていただくとして下記の型を線形型版モナドのインスタンスにすることができました。線形型に慣れていなかったため型合わせが想像以上に大変でした。
newtype ContT r m a = ContT { runContT :: (a #-> m r) #-> m r }
使ってみましょう。
> :set -XQualifiedDo > import Prelude.Linear (lseq) > import qualified Prelude.Linear as PL > import Data.Queue.Ephemeral > import Control.Monad.Trans.Cont.Linear > import qualified Control.Monad.Linear as ML > :{ | PL.flip runCont PL.id $ ML.do | q0 <- cont empty | q1 <- cont (enqueue (0 :: Int) q0) | Just (a, q2) <- cont (dequeue q1) | q2 `lseq` ML.pure a | :} 0
やったぜ。
まあ、こういうインターフェースでありがちな pure で外に出す抜け道が存在するのですが。
リポジトリー
追記（2021.01.01）
続編を書きました。 kakkun61.hatenablog.com-
ここでいう線形関数は一次関数という意味ではありません。↩
とりとめのない GHC 線形型メモ
GHC 9.0.1 alpha 1 がリリースされたときに線形型をいじってみていたことをメモしていなかったので思い出しながらメモしていく。
使用バージョン
- GHC 9.0.0.20200925
- 上記リンクのもの
ghcup ならそれ経由でインストールできる。
ghcups の場合は手動インストール後、下記のような設定ファイルで切り替えができるようになる1。
ghc: 9.0.1-alpha1: H:\programs\ghc-9.0.0.20200925-x86_64-unknown-mingw32\bin
線形型とは
GHC では引数が1回しか使えない（1回は使わないといけない）関数型として線形型が実装されている。
- 一般の関数：
- 線形型の関数：
は Haskell 文法としては
a %1 -> b として書く。
a %1 -> b は a %'One -> b の別名で（' は data kinds 拡張のシングルクォート）、a %'One -> b は FUN 'One a b の別名となっている。これにともなって a -> b は FUN 'Many a b の別名となった。FUN の型は下記のようになっている。
FUN :: Multiplicity -> forall (r1 r2 :: RuntimeRep). TYPE r1 -> TYPE r2 data Multiplicity = One -- represents 1 | Many -- represents ω
最終的には上記のようになるようだが 9.0.1 alpha 1 の時点では は
a #-> b と記述する。
a #-> b から a %1 -> b に変わった理由の1つとしては overloaded labels が将来的に型レベルに持ち上げられたときの文法の衝突を回避することがあるらしい。
マージ前だと a ->. b の時期もあったようだ。
ちょうど1回
準備ができたらコードを書いてみる。下記コマンドで REPL を起動する。
ghc --interactive -XLinearTypes
まず最初にエラーを起こしてみる。
f :: Int #-> (Int, Int) f a = (a, a)
<interactive>:3:3: error:
* Couldn't match type 'Many with 'One
arising from multiplicity of `a'
* In an equation for `f': f a = (a, a)
a が2回使用されているので推論される f の型は a -> (a, a) つまり FUN 'Many a (a, a) だが、注釈は Int #-> (Int, Int) つまり FUN 'One Int (Int, Int) なので FUN の第1引数である Multiplicity が不一致だと言っている。
引数を1回も使用しなくても同じエラーとなる。
f :: Int #-> (Int, Int) f a = (1, 2)
<interactive>:7:3: error:
* Couldn't match type 'Many with 'One
arising from multiplicity of `a'
* In an equation for `f': f a = (1, 2)
ちょうど1回使用するともちろんうまくいく。
f :: Int #-> (Int, Int) f a = (a, 1)
注釈がない場合、ちょうど1回しか使っていなくても multiplicity は （many）となる。multiplicity ポリモーフィズムは今のところない。
Prelude> g a = ((a, 1) :: (Int, Int)) Prelude> :type g g :: Int -> (Int, Int)
a #-> b を a -> b としても使えるというような部分型関係はない。
h :: Int -> (Int, Int) h = f
<interactive>:21:5: error:
* Couldn't match type 'One with 'Many
Expected: Int -> (Int, Int)
Actual: Int #-> (Int, Int)
* In the expression: f
In an equation for `h': h = f
引数を明記すると、これは妥当である。
h :: Int -> (Int, Int) h a = f a
f = g と f a = g a の意味が同じでないというのはこれまでの Haskell の感覚からすると注意が必要なところに思える。
パターンマッチをすると1回使ったとカウントされるので下記のようなコードも妥当である。
consume :: Bool #-> () consume False -> () consume True -> ()
引数に関係なく返り値が同じだからと次のように書くと、これは引数未使用となるためエラーとなる。これもうっかりまちがえそうだ。
consume :: Bool #-> () consume _ -> ()
<interactive>:1:33: error:
* Couldn't match type 'Many with 'One
arising from a non-linear pattern
* In the pattern: _
In an equation for `consume': consume _ = ()
linear-base
GHC への線形型を提案して実装した Tweag が作っている線形型対応の base パッケージが linear-base で、ここからはそれを使っていく。使用リビジョンは 341007891ae77959ac7b147f008e3a1d9c46e96b である。
multiplicity ポリモーフィズムはない
multiplicity ポリモーフィズムがないので ($) は線形版との使い分けが必要である。
f $ 1 -- error: Couldn't match type ‘'Many’ with ‘'One’ arising from an application
import qualified Prelude.Linear as L f L.$ 1
現状 case 式は線形型非対応なので case x of … と書くと x は複数回使用したとみなされてしまう。それを回避するために lambda case 拡張2を使ったイディオムが必要となる（参考）。
{-# LANGUAGE LambdaCase #-} import Prelude.Linear ((&)) maybeFlip :: Int #-> Int #-> (a,a) -> a maybeFlip i j (x,y) = i < j & \case True -> x False -> y
let や where も線形型非対応なので注意が必要である（参考）。
Consumable 型クラス
先述した consume 関数は Data.Unrestricted.Linear モジュールの Consumable 型クラスで提供されている（参考）。
class Consumable a where consume :: a #-> ()
Dupable 型クラス
最初の例で2回使えないという話をしたが、アドホックポリモーフィズムを使えば実装できる（参考）。V :: Nat -> Type -> Type は型レベル長さ付きベクトルである（参考）。
-- | The laws of @Dupable@ are dual to those of 'Monoid': -- -- * @first consume (dup2 a) ≃ a ≃ second consume (dup2 a)@ (neutrality) -- * @first dup2 (dup2 a) ≃ (second dup2 (dup2 a))@ (associativity) -- -- Where the @(≃)@ sign represents equality up to type isomorphism. -- -- When implementing 'Dupable' instances for composite types, using 'dupV' -- should be more convenient since 'V' has a zipping 'Applicative' instance. class Consumable a => Dupable a where {-# MINIMAL dupV | dup2 #-} dupV :: forall n. KnownNat n => a #-> V n a dup2 :: a #-> (a, a)
Bool に対する実装は下記になっている。ここで Data は Data.Functor.Linear.Internal である。
instance Dupable Bool where dupV True = Data.pure True dupV False = Data.pure False
pure は線形型版アプリカティブファンクターのもので下記の型を持つ。
class Functor f => Applicative f where pure :: a -> f a …
dupV の引数はパターンマッチで1回しか使っていなくて、pure に渡した True や False は何回でも使えるから pure に渡せて pure は線形関数じゃないから複製ができるということかな。
Ur 型
linear-base で1つキモになる型に Ur 型がある（参考）。
-- | @Ur a@ represents unrestricted values of type @a@ in a linear -- context. The key idea is that because the contructor holds @a@ with a -- regular arrow, a function that uses @Ur a@ linearly can use @a@ -- however it likes. -- > someLinear :: Ur a #-> (a,a) -- > someLinear (Ur a) = (a,a) data Ur a where Ur :: a -> Ur a
線形型文脈の中に何回も使える普通の値を埋め込む型で、Ur 値構築子の型が a #-> Ur a ではなく a -> Ur a となっているので中身の a 型の値は何回でも使えるようになっている。
追記（2020.12.19）
Ur の定義を下記のようにすると型構築子のカインドも値構築子の型も上記と同じとなるが線形関数と一緒に用いると型検査に違いが出る。
data Ur a = Ur a下記のような線形関数を考える。
f :: Ur a #-> (a, a) f (Ur a) = (a, a)GADT を使った定義だと問題なく型検査が通るが、後者の定義だと下記のエラーが出る。
<interactive>:40:31: error:
• Couldn't match type ‘'Many’ with ‘'One’
arising from multiplicity of ‘a’
• In the pattern: Ur a
In an equation for ‘f’: f (Ur a) = (a, a)
Movable 型クラス
線形関数の引数を Ur で包む関数をもつのが Movable 型クラスである（参考）。
-- | The laws of the @Movable@ class mean that @move@ is compatible with -- @consume@ and @dup@. -- -- * @case move x of {Ur _ -> ()} = consume x@ -- * @case move x of {Ur x -> x} = x@ -- * @case move x of {Ur x -> (x, x)} = dup2 x@ class Dupable a => Movable a where move :: a #-> Ur a
Functor・Applicative・Monad 型クラス
linear-base の提供する Functor と Applicative には2種類ある。
まず Data.Functor.Linear.Internal から見ていく。
class Functor f where fmap :: (a #-> b) -> f a #-> f b class Functor f => Applicative f where pure :: a -> f a (<*>) :: f (a #-> b) #-> f a #-> f b liftA2 :: (a #-> b #-> c) -> f a #-> f b #-> f c
もう1つは Control.Monad.Linear.Internal にある。Data は上記の Data.Functor.Linear.Internal である。
class Data.Functor f => Functor f where fmap :: (a #-> b) #-> f a #-> f b class (Data.Applicative f, Functor f) => Applicative f where pure :: a #-> f a (<*>) :: f (a #-> b) #-> f a #-> f b liftA2 :: (a #-> b #-> c) #-> f a #-> f b #-> f c class Applicative m => Monad m where (>>=) :: m a #-> (a #-> m b) #-> m b (>>) :: m () #-> m a #-> m a
前者は一部普通の関数だが後者は全部線形関数になっている。
fmap :: (a #-> b) -> f a #-> f b fmap :: (a #-> b) #-> f a #-> f b pure :: a -> f a pure :: a #-> f a liftA2 :: (a #-> b #-> c) -> f a #-> f b #-> f c liftA2 :: (a #-> b #-> c) #-> f a #-> f b #-> f c
前者だとモナドっぽいものにならないのかな（よく分かってない）。
ほか
linear-base にはまだ見るべきところがあるようだが、まだ見てないので終わり。User guide に記載の下記などは気になる。
Here's a list of new abstractions made possible by linear types:
Tweag のブログの線形型応用例。なるほどとなった。
参考
- ghc-proposals/0111-linear-types.rst at master · ghc-proposals/ghc-proposals · GitHub
- プロポーザル
- これを読まなきゃ始まらない
- GitHub - tweag/linear-base: Standard library for linear types in Haskell.
- イディオムが学びになる
- GHCの線形型プロトタイプを試すだけ - syocy’s diary
- 文法が古いが線形型とリソース管理に関する日本語記事