重ね着したバービー人形 in Haskell

うやむやで終わる記事なので事前にご了承ください。

前回のあらすじ

(前回などないので探さなくていいです。)

高カインドデータ型(Higher-kinded Datatypes; HKD)というものがあります。

fumieval.hatenablog.com

qiita.com

簡単に説明すると下記のようなデータ型 D があるとき

data D =
  D { a :: A
    , b :: B
    }

D の代わりに H のようなデータ型を作ると便利という発想です。

data H f =
  H { a :: f A
    , b :: f B
    }

H Identity だと D と同じ意味になりますし、H Maybe だと部分的に(もしくは全部)値が欠けたものを意味します。

HKD をサポートするライブラリーとして barbies がポピュラーです。

hackage.haskell.org

HD のように使うには Identity をたくさん書くことになりますが barbies の提供する機能を使うと Identity を書く手間が減らせます。

こういうものが用意されているので、

data Bare
data Covered

type family Wear t f a where
  Wear Bare    f a = a
  Wear Covered f a = f a

HB のように書き換えます。

data B b f =
  B { a :: Wear b f A
    , b :: Wear b f B
    }

このとき B Bare fD と同じ構造に B Covered fH と同じ構造になります。

こういうデータ型に対する操作も barbies は提供しています。

class FunctorB (b Covered) => BareB b where
  bstrip :: b Covered Identity -> b Bare Identity
  bcover :: b Bare Identity -> b Covered Identity

ここまでが「前回のあらすじ」です。

重ね着

ここからは「なんかこういうのがほしいな」という発展です。

data L f =
  L { a :: f A
    , d :: f (D f) -- D も HKD
    }

HKD が入れ子になっててもいいじゃない。

経緯としては、抽象構文木(Abstract Syntax Tree; AST)のデータ型を書いていて、位置情報を持つファンクター(例えば WithLocation とする)を f に与えるようにするとすっきりならんかと思いました。

data Expression f
  = Abstract
      { variable :: f Variable
      , expression :: f (Expression f)
      }
  | Application
      { expression1 :: f (Expression f)
      , expression2 :: f (Expression f)
      }

ファイルをパースして構築するときは Expression WithLocation として、テスト時は Expression Identity として使用します。

こうするとノードに付与する追加データと AST 自体の構造とが分離できて嬉しいです。

ここで barbies にあった Wear を使うとこうなります。

data Expression b f
  = Abstract
      { variable :: Wear b f Variable
      , expression :: Wear b f (Expression b f)
      }
  |

ここで ExpressionBareBインスタンスになるか考えます。

そのためには FunctorBインスタンスでないといけません。

FunctorB は次のような型クラスです。

class FunctorB b where
  bmap :: (forall a . f a -> g a) -> b f -> b g

Expression に対する bmap を実装してみます。

instance FunctorB (Expression Covered) where
  bmap f (Abstract v e) = Abstract (f v) (_ $ f e)
  bmap f (Application e1 e2) =

_ の部分の型は g (Expression Covered f) -> g (Expression Covered g) となるはずですが、うーん実装できなさそうです。

入れ子 HKD では bmap の型は Functor g => (forall a. f a -> g a) -> b f -> b g もしくは Functor f => (forall a. f a -> g a) -> b f -> b g となる必要がありそうです。

そんなわけで入れ子 HKD は barbies の提供する FunctorBBareB とは別の型クラスが必要となります。

さて、ここでリストを考えます。

newtype List x b f = List { unlist :: [Wear b f (x b f)] }

こういうデータ型があると、これに関して bmap を定義できて便利そうです。

同様にタプルについてもこんな Tuple2 を考えると……

newtype Tuple2 x y b f = Tuple2 { untuple2 :: (Wear b f (x b f), Wear b f (y b f)) }

というふうに考えて進めてたんですが、元の型と Wear 版の型との相互変換がいっぱいになったり、List x Bare Identity[] になってほしくなって型族を使いだしたりして収拾がつかなくなって一旦やめます、というお話です。

なんやそら。

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

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

最近 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