Zenn
Open6

Paper: 『Linear Haskell: practical linearity in a higher-order polymorphic language』

Haskell
#
lineartype
hatahata

Rust や Clean などの所有権のアプローチと Linear Haskell などの線形型のアプローチの比較

6.3 Uniqueness and ownership typing

The literature contains many proposals for uniqueness (or ownership) types (in contrast with linear types). Prominent representative languages with uniqueness types include Clean [Barendsen and Smetsers 1996] and Rust [Matsakis and Klock 2014]. Linear Haskell, on the other hand, is designed around linear types based on linear logic [Girard 1987].
Idris [Brady 2013] features uniqueness types, which have been used, in particular, to enforce communication protocols [Brady 2017]. Uniqueness types, in Idris, are being replaced by linear types based on qtt [Atkey 2017], a variant of McBride [2016].
Linear types and uniqueness types are, at their core, dual: whereas a linear type is a contract that a function uses its argument exactly once even if the call’s context can share a linear argument as many times as it pleases, a uniqueness type ensures that the argument of a function is not used anywhere else in the expression’s context even if the callee can work with the argument as it pleases. Seen as a system of constraints, uniqueness typing is a non-aliasing analysis while linear typing provides a cardinality analysis. The former aims at in-place updates and related optimisations, the latter at inlining and fusion. Rust and Clean largely explore the consequences of uniqueness on in-place update; an in-depth exploration of linear types in relation with fusion can be found in Bernardy et al. [2015]; see also the discussion in Sec. 7.1.
Because of this weak duality, we could have retrofitted uniqueness types to Haskell. But several points guided our choice of designing Linear Haskell around linear logic instead: (a) functional languages have more use for fusion than in-place update (if the fact that ghc has a cardinality analysis but no non-aliasing analysis is any indication); (b) there is a wealth of literature detailing the applications of linear logic — see Sec. 5; (c) and decisively, linear type systems are conceptually simpler than uniqueness type systems, giving a clearer path to implementation in ghc.

Rust & Borrowing. In Linear Haskell we need to thread linear variables throughout the program. Even though this burden could be alleviated using syntactic sugar, Rust uses instead a type-system feature for this purpose: borrowing. Borrowed values differ from owned values in that they can be used in an unrestricted fashion, albeit in a delimited scope.
Borrowing does not come without a cost, however: if a function f borrows a value v of type T, then the caller of the function must retain v alive until f has returned; the consequence is that Rust cannot, in general, perform tail-call elimination, crucial to the operation behaviour of many functional programs, as some resources must be released after f has returned.
The reason that Rust programs depend so much on borrowing is that unique values are the default. Linear Haskell aims to hit a different point in the design space where regular non-linear expressions are the norm, yet gracefully scaling up investing extra effort to enforce linearity invariants is possible. Nevertheless, we discuss in Sec. 7.2 how to extend Linear Haskell with borrowing.

6.3 独自性と所有権のタイピング

文献には、(線形型とは対照的に)一意性(または所有権)型に関する多くの提案が含まれている。一意型を持つ代表的な言語には、Clean [Barendsen and Smetsers 1996]やRust [Matsakis and Klock 2014]がある。一方、Linear Haskellは線形論理[Girard 1987]に基づく線形型を中心に設計されている。
Idris [Brady 2013]は一意型を特徴としており、特に通信プロトコルを強制するために使われてきた[Brady 2017]。Idrisの一意性型は、McBride [2016]の亜種であるqtt [Atkey 2017]に基づく線形型に置き換えられつつある。
線形型と一意性型は、その核心において二重のものである。線形型が、呼び出しのコンテキストが何度でも線形引数を共有できる場合でも、関数がその引数を正確に一度だけ使用するという契約であるのに対し、一意性型は、呼び出し側(callee)が好きなように引数を扱うことができる場合でも、関数の引数が式のコンテキストの他のどこにも使用されないことを保証するものである。制約のシステムとして見た場合、一意性型付けはノンエイリアス分析であり、一方線形型付けはカーディナリティ分析を提供する。前者はインプレース更新とそれに関連する最適化を目的とし、後者はインライン化と融合を目的としている。RustとCleanは、主にインプレース更新における一意性の結果を探求している。融合に関連する線形型の詳細な探求は、Bernardyら[2015]にある。
この弱い二重性のために、一意性型をHaskellに後付けすることもできた。しかし、いくつかの点から、線形論理を中心にLinear Haskellを設計することにした:(a)関数型言語には、インプレース更新よりもフュージョン(ghcにはカーディナリティ解析はあるが、ノンエイリアス解析はないという事実が示唆するものであれば)の方が使い道があること、(b)線形論理の応用を詳しく説明した文献が豊富にあること(第5節を参照)、(c)そして決定的なことは、線形型システムは一意性型システムよりも概念的に単純であり、GHCでの実装に明確な道筋を与えてくれることです。

Rustと借用。Linear Haskellでは、プログラム全体に線形変数を通す必要がある。この負担は構文糖衣を使えば軽減できるにもかかわらず、Rustでは代わりに型システムの機能である借用を使っている。借用値は所有値とは異なり、限定されたスコープではあるが、無制限に使用することができる。
関数fがT型の値vを借用した場合、関数の呼び出し元はfが返されるまでvを保持しなければならない。その結果、Rustは一般的に、fが返された後にいくつかのリソースを解放しなければならないため、多くの関数型プログラムの動作にとって重要な tail call elimination を実行できない。
Rustのプログラムが借用に大きく依存するのは、一意な値がデフォルトだからだ。Linear Haskellは、正規の非線型式が標準でありながら、線形性不変量を強制するために余分な労力を投資して潔くスケールアップすることが可能な、設計空間の異なるポイントを目指す。とはいえ、Linear Haskellを借用で拡張する方法については第7.2節で説明する。

hatahata

Gauche の :immutable slot option

Gauche Devlog - :immutable slot option

スロットが :immutable スロットオプションにtrueの値を持つ場合、スロットは一度だけ初期化できます ― つまり、セッターはスロットが以前にアンバインドされていれば値を設定しますが、そうでなければエラーを投げます。

イニシャライザーがスロットをバインドしないままにしておき、後でユーザーが slot-set!を呼び出してスロットを一度だけセットすることも可能です。これは遅延初期化とみなすことができます。

hatahata

Erlang の queue における Okasaki-API

Erlang -- queue

This module has three sets of interface functions: the "Original API", the "Extended API", and the "Okasaki API".

The "Okasaki API" is inspired by "Purely Functional Data Structures" by Chris Okasaki. It regards queues as lists. This API is by many regarded as strange and avoidable. For example, many reverse operations have lexically reversed names, some with more readable but perhaps less understandable aliases.

「Okasaki-API」は、Chris Okasakiの「Purely Functional Data Structures」にインスパイアされています。これはキューをリストとみなしています。このAPIは多くの人から奇妙で避けるべきものだと思われています。例えば、多くの逆方向操作は辞書的に逆方向の名前を持っており、いくつかはより読みやすいが、おそらく理解しにくい別名を持っている。

『Purely Functional Data Structures』の日本語訳：

https://www.kadokawa.co.jp/product/301703000259/

hatahata

Haskell の LinearTypes を実際に試してみたメモ

何年も Haskell を触ってないので環境を作るところから

Installation

最近は ghcup というのを使って GHC の各バージョンを管理するのがよいらしい。

Haskellの環境構築2023 だと Mac での ghcup のインストール方法が書いてないけど Homebrew にあった。

brew install ghcup
ghcup --version
#=> The GHCup Haskell installer, version 0.1.20.0
ghcup install ghc 9.4.8  # そのときの最新の安定版
ghcup set ghc 9.4.8

パスを通す。このフォルダに ghci とか一通りのエイリアスが入っている。

export PATH="$PATH:$HOME/.ghcup/bin"
ghc --version
#=> The Glorious Glasgow Haskell Compilation System, version 9.4.8

Hello

hello.hs
main = putStrLn "Hello, World!"

$ ghc -o hello ./hello.hs && ./hello
Hello, World!

Linear Types を使ってみる

linear.hs
{-# LANGUAGE LinearTypes #-}

module Main where

tuple1 :: Int %1 -> Int %1 -> (Int, Int)
tuple1 a b = (a, b)

tuple2 :: Int %1 -> Int %1 -> (Int, Int)
tuple2 a b = (a, a) 

$ ghc -o linear ./linear.hs && ./linear
[1 of 2] Compiling Main             ( linear.hs, linear.o )

linear.hs:9:8: error:
    • Couldn't match type ‘'Many’ with ‘'One’
        arising from multiplicity of ‘a’
    • In an equation for ‘tuple2’: tuple2 a b = (a, a)
  |
9 | tuple2 a b = (a, a)
  |        ^

linear.hs:9:10: error:
    • Couldn't match type ‘'Many’ with ‘'One’
        arising from multiplicity of ‘b’
    • In an equation for ‘tuple2’: tuple2 a b = (a, a)
  |
9 | tuple2 a b = (a, a)
  |          ^

参考

脚注

  1. すごく詳しい記事です。ありがとうございます。 ↩︎