GHC 9.0.1 alpha 1 がリリースされたときに線形型をいじってみていたことをメモしていなかったので思い出しながらメモしていく。
mail.haskell.org
使用バージョン
ghcup ならそれ経由でインストールできる。
ghcups の場合は手動インストール後、下記のような設定ファイルで切り替えができるようになる1。
ghc:
9.0.1-alpha1: H:\programs\ghc-9.0.0.20200925-x86_64-unknown-mingw32\bin
線形型とは
GHC では引数が1回しか使えない（1回は使わないといけない）関数型として線形型が実装されている。
- 一般の関数：
- 線形型の関数：
線形型の GHC プロポーザルはこちら。
github.com
は 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
| Many
最終的には上記のようになるようだが 9.0.1 alpha 1 の時点では は a #-> b と記述する。
a #-> b から a %1 -> b に変わった理由の1つとしては overloaded labels が将来的に型レベルに持ち上げられたときの文法の衝突を回避することがあるらしい。
gitlab.haskell.org
マージ前だと 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 である。
github.com
multiplicity ポリモーフィズムがないので ($) は線形版との使い分けが必要である。
f $ 1
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 は型レベル長さ付きベクトルである（参考）。
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 型がある（参考）。
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 型クラスである（参考）。
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:
- Mutable arrays, hashmaps, vectors, sets with a pure API. See
Data.Array.Mutable.Linear.
- Push and Pull arrays: a way to control when arrays are allocated and force array fusion. See
Data.Array.Polarized.
- A linear API for system heap (not GC) allocation of values. See
Foreign.Marshall.Pure.
Tweag のブログの線形型応用例。なるほどとなった。
www.tweag.io
参考
