GHC 9.0.1 alpha 1 がリリースされたときに線形型をいじってみていたことをメモしていなかったので思い出しながらメモしていく。

使用バージョン

GHC 9.0.0.20200925
- 上記リンクのもの

ghcup ならそれ経由でインストールできる。

ghcups の場合は手動インストール後、下記のような設定ファイルで切り替えができるようになる¹。

ghc:
  9.0.1-alpha1: H:\programs\ghc-9.0.0.20200925-x86_64-unknown-mingw32\bin

線形型とは

GHC では引数が1回しか使えない（1回は使わないといけない）関数型として線形型が実装されている。

一般の関数： $\displaystyle{a \to b}$
線形型の関数： $\displaystyle{a \multimap b}$

線形型の GHC プロポーザルはこちら。

github.com

$\displaystyle{a \multimap b}$ は 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 の時点では $\displaystyle{a \multimap b}$ は 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 は $\displaystyle{\omega}$ （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 ポリモーフィズムはない

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 拡張²を使ったイディオムが必要となる（参考）。

{-# 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:

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