多相からプログラミング言語を見る

こんにちは。ホビー型システミストの岡本です。

最近 C++ の習得をしていて、なんとなく多相(polymorphism)の視点からいくつかのプログラミング言語をまとめてみようという気になったので書いてみます。

部分型多相(subtype polymorphism)

クラスベースオブジェクト指向言語でよく使うのは部分型多相ですかね。

JavaC#C++ にある、名称的部分型多相(nominal subtype polymorphism)はこんな感じ。次の例は Java です。

class A {}

class B extends A {}

public class Main {
    public static void main(string[] args) {
        A foo = new B();
    }
}

変数 fooA 型だけど、型(クラス)BA の部分型(サブクラス・派生クラス)なので、fooB 型の値に束縛することができます。

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, "");

BA の部分型であると明記していませんが、BA として扱うに足るフィールドを持つので 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)

パラメーター多相JavaC#C++ でそれぞれジェネリクスジェネリック・テンプレートと呼ばれるものです(C++ のテンプレートはちょっと違うかも)。

恒等関数を JavaC#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

一般的には型変数になった型(上記でいう Ta)に関する性質は使えません。Ta にはどんな型も来られるようにしないといけないためです。性質を使いたい場合は後述します。

アドホック多相(ad-hoc polymorphism)

例えば + 演算子について Int -> Int -> Int という型としても使いたいし Double -> Double -> Double としても使いたく、そして実装が違う、という場合に出てくるのがアドホック多相です。

JavaC#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

アドホック多相が他の多相と組み合わさると、どの実装が選ばれるのかのアルゴリズムを知るために言語仕様を読むはめになってちょっとやっかいです(個人の感想)。

オーバーロード

JavaC#オーバーロードは機能がちょっと弱くて返り値に関する多相にできません。

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 ではインプリシットパラメーターというらしいです。

多相の組み合わせ

先述したパラメーター多相のパラメーターを性質で制限したい場合について記述します。それにはアドホック多相を採用する言語と部分型多相を採用する言語があります。

パラメーターを部分型多相で制限する

部分型多相で制限する場合は「特定の型の部分型でないといけない」というように制限します。JavaC# などがそうです。下記は Java の例です。

public class Main {
    public static <T extends Hello> String greet(T target) {
        return target.hello() + "!";
    }
}

interface Hello {
    String hello();
}

THello の部分型であることが保証されるので target.hello が呼べるわけですね。

パラメーターをアドホック多相で制限する

型クラスで制限する場合は「特定の型クラスを実装している型でないといけない」というように制限します。Haskell などがそうです。下記は Haskell の例です。

greet :: Hello a => a -> String
greet a = hello a ++ "!"

class Hello a where
  hello :: a -> String

aHello 型クラスを実装していることが保証されるので hello が呼べるわけです。

C++ の場合はちょっと変わっていて関数を使用すると暗黙にその関数の存在が要求されるようです。次のコードは、JavaC# と違ってエラーなくコンパイルできます。

#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 のコンセプトなのかな?

他の多相

線形型があると線形性に関する多相とか他にもいろいろあるだろうけどよく知らないのでこの辺で。

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 -- 実際は多態、構築子と引数の順番が反対

  1. case analysis の名前は booleither のドキュメントで使われています。eliminator 派もあるようです。

続・刹那的純粋関数的データ構造と線形型

The English version is at Dev.


前回の記事の追加情報です。

kakkun61.hatenablog.com

pure 抜け道はなかった

まあ、こういうインターフェースでありがちな pure で外に出す抜け道が存在するのですが。

最後にこういうことを無思慮に書いたわけですが、Dev に書いた英語版を Reddit に載せたところ有益な情報を教えてもらえました。

www.reddit.com

I think the solution to the problem with empty might be to use the Ur (for "unrestricted") datatype from linear-base:

empty :: (Queue a #-> Ur b) #-> Ur b

Trying to run empty Ur shouldn't typecheck, because the Ur constructor 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 にしなくていいことに気付きました。

線形関数の中でその引数に別の線形関数を適用するとその返り値にも線形性が付くようです。この辺りちゃんと型付け規則を確認しないとな。

つまり、empty の継続 Queue a #-> Ur b の中で enqueue などを呼ぶとその返り値も1回しか使えないわけなので、enqueue などは CPS にしなくてよかったです。逆に nullBool は何回使ってもいいので 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章に刹那的純粋関数的キューというものが出てきます。

https://asciidwango.jp/post/160831986220/%E7%B4%94%E7%B2%8B%E9%96%A2%E6%95%B0%E5%9E%8B%E3%83%87%E3%83%BC%E3%82%BF%E6%A7%8B%E9%80%A0
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 の線形型については前回の記事を参考にしてください。

kakkun61.hatenablog.com

実装

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 mlm再帰的に「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 記法を使って読みやすくすることができます。

qiita.com

さて線形型版でもできるのでしょうか?やってみましょう。……(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 で外に出す抜け道が存在するのですが。

リポジトリ

github.com

追記(2021.01.01)

続編を書きました。 kakkun61.hatenablog.com

  1. ここでいう線形関数は一次関数という意味ではありません。