Just $ A sandbox

プログラミングとかPCとかの技術的なメモ

Codensity Monad

Codensity という型がある. 定義は以下.

newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }

instance Functor (Codensity k) where
  fmap f (Codensity m) = Codensity (\k -> m (k . f))

instance Monad (Codensity f) where
  return x = Codensity (\k -> k x)
  m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))

これの何が良いかと言うと, これは以下のようにMonadFreeな作用を持つ.

instance (Functor f, MonadFree f m) => MonadFree f (Codensity m) where
  wrap t = Codensity (\h -> wrap (fmap (\p -> runCodensity p h) t))

Codensityはnewtypeで実装されているから, 実行時には CodensityrunCodensity によるオーバーヘッドは考えなくて良い. だから, m のMonadFreeのメソッドを直接呼ぶよりも効率よくなる可能性が高い. 特に, 元々のmが「重い」モナドなら, Codensity をかぶせるだけで劇的に速くなることがある.

Codensityのパフォーマンスの話は http://www.iai.uni-bonn.de/~jv/mpc08.pdf などを参考にしてもらうことにして, 以下ではCodensityの(圏論的な)説明をしてみる.

以下, 定義などは逐一述べないので必要に応じてnLabなり参考文献に挙げたものを参照してください.

RanとCodensity

functor p : C → Dに対し, functor  p^{-1} \colon \mathcal{E}^\mathcal{D} → \mathcal{E}^\mathcal{C}を,  p^{-1}(F) = F \circ p によって定める. ただしここで  \mathcal{E}^\mathcal{D} とはDからEへの関手のなす関手圏のこと.

functor f : C → E, p : C → Dに対し, pに沿ったfの右Kan拡張  p \ddagger f を考える.
 p \ddagger が存在すれば, これは  p^{-1} の右随伴である.

D
↑ ↘ p‡f
| ⇓ ↘
C ――→ E

随伴の定義から,

 \hom(p^{-1}(-),f) \cong \hom(-,p \ddagger f)

ここで,  \mathcal{C} の対象aを一つ固定し, 米田関手yを用いて

 \hom(p^{-1}(ya),f) \cong \hom(ya,p \ddagger f)

 p^{-1} の定義に戻れば,

 \hom(ya \circ p,f) \cong \hom(ya,p \ddagger f)

さらに右辺で(共変)米田の補題を用いて,

 \hom(ya \circ p,f) \cong \hom(ya,p \ddagger f) \cong (p \ddagger f)(a)

なる同型を得る. ゆえに (p \ddagger f)(a) が存在したとすれば最左辺と同型になる.
さて今はHaskellでの話がしたいので, 対象とは型であり, 射とは函数である.  \hom(ya \circ p,f) とは, 自然変換の集合であるが, これを ya \circ p \rightarrow fなる自然変換からなる型と同一視する.

このような仕方で (p \ddagger f)(a)を最左辺で定義すると,
自然変換 ya . p ~> fRankNTypes を用いて, forall b. (a -> p b) -> f b なる型を持つ.

よって,

newtype Ran p f a = Ran (forall b. (a -> p b) -> f b)

を得る. これは http://hackage.haskell.org/package/kan-extensions-4.1.0.1/docs/Data-Functor-Kan-Ran.html で定義されている.

最後に, pもfもmで固定してしまうと,

newtype Ran     m m a = Ran       (forall b. (a -> m b) -> m b)
newtype Codensity m a = Codensity (forall b. (a -> m b) -> m b)

により, Codensityが得られた.

HaskellでのFunctor, Monad

上のような操作でCodensityは得られるが, 上の操作では pやfは関手 であった.
しかしCodensityはFunctorのinstanceで(Functor m) =>を要求しない (つまり, mがFunctorやMonadでなくとも, CodensityはFunctorおよびMonadになる).

最初の実装で確かにCodensityがFunctorやMonadになることは確認が必要なので, Agdaで証明を書いてみた.

確かに,

instance Functor (Ran p f)
instance Functor (Codensity k)
instance Monad (Codensity f)

なるインスタンスが正しく実装されていることが分かる.

参考文献

Agdaで集合論をやろうとして上手く行かなかった

この前の記事の方針でゴリゴリ公理を追加していたら, 問題が発生した.

写像の定義を

_⟶_ A B = ∀ x → x ∈ A → ∃ \y → y ∈ B

としたら, (これはとても自然な定義に見えるけれど)例えば A ≡ B から f(A) ≡ f(B) が導けなくなる.
x ∈ A を像の方に押し込めて

_⟶_ A B = ∀ x → ∃ \y → x ∈ A → y ∈ B

のように定義すると, 今度は x ∈ A に依って決まる写像が定義できなくなる.

最初の方法ではZFCから排中律を示すところで引っかかり(本来異なる集合 A,B に対して A ≡ B を言おうとするので型エラーになって上手く行かない), あとの方法では置換公理を使う場面でひっかかる(函数の像を扱うとき).
よっていずれにせよ上手く行かない.

この前の記事のコメントではAgdaの型を用いて を定義する方法も教えてもらった.

data _∈_ {l} {A : Set l} (x : A) (B : Set l) : Set (suc l) where
  in-eq : A ≡ B → x ∈ B

この方法だと, の定義がもろにAgdaの型システムに依存しているので, 方針はガラッと変わるはず.
多分これで今やっていることの模倣はできると思うけれど, そもそも何を公理として仮定して良いのかが分からないし, もともとAgdaの型システムではどういうことができるのかもよく分からないのでなんとも言えない.

Agdaの方に上手く寄れば, 多分普通の数学の模倣はできるような気がするけれど, 少なくとも数学のやり方をそのまま持ってくるだけでは上手く行かないのかなぁと思った.
こういうことをするなら, Agdaよりもっと向いている言語を他に探したほうがいいのかもとも思った.
でもAgdaはHaskellerの自分にとっては学びやすかったし, 気に入ったところも多かったので少し残念.

供養

https://github.com/myuon/agda-cate

(圏論はそれなりに上手く行っているので, 圏論方面はもう少し開発を続けるかもしれない)

矛盾の証明

矛盾を示すときに使える方法としては主に以下の2つだと思う

  • 命題 ¬PP をぶつける
  • 矛盾 の特徴付けを使う

矛盾の特徴付けというのは, 例えばAgdaだと⊥は空集合の公理を満たすことが示せるから,
空集合の公理がそのまま矛盾の特徴付けになる.
∃ \(A : Set) → (∀ x → ¬ (x ∈ A))

否定命題にPをぶつけるというのは口で言うほど簡単ではなくて, まずどの否定命題を選んでくるかからよく考えないといけない.

一体何の話かというと, Agdaで「ZFC ⇒ 排中律 (P ∨ (¬ P))」を示すときに,

https://myuon.github.io/agda-cate/Sets.Sets.NonDatur.html#660

A = ⟦ x ∈ [0,1] ∣ x ≡ 0 ∨ P ⟧ -- A := {x ∈ {0,1} ∣ x = 0 ∨ P}
B = ⟦ x ∈ [0,1] ∣ x ≡ 1 ∨ P ⟧ -- B := {x ∈ {0,1} ∣ x = 1 ∨ P}
X = [ A , B ] -- X := {A,B}

みたいにするんだけど, 以下の議論では, ここにさらっとでてくる自然数0と1が異なることが仮定されている.

0と1は上のように非順序対を作って使うので適当なsetでないといけないんだけど, 当然AgdaのData.Natで定義されているNatの元は(inductive data typesで定義されているから)setではない.
そこで 0 = ∅, 1 = ∅ ∪ {∅} に戻って0と1が異なることを示さないといけなかったけれど, これには空集合の公理や対の公理や和集合の公理が必要で, しかもそんなに明らかなことでもない.
https://myuon.github.io/agda-cate/Sets.Sets.Natural.html#793

Natの世界でもSetの世界でも0と1が異なることを示すには, 0=1を仮定して矛盾を導かなければいけないので, それがいつも自明なことではないなと実感した.

というかむしろ, Agdaの場合は同値なものがrewriteによって書き換えるだけで証明が済んでしまうことが多いので, 等しさが特別扱いやすいだけなのかもしれないけど.

Classical set theory in Agda

Agda歴2週間くらいのザコです。 Agda圏論のライブラリを作って、流れで位相空間の定義をしようと思ったらそもそも集合を普通に扱えるライブラリがどこにもない。

標準ライブラリにRelation.Unaryとかいうのもあるけど、これは表面的には上手く行っているように見えるだけであんまり使い物にならない。
具体的に言うと和集合の公理がないので(binary cupとindexed bigcupはある)任意個のUnionがとれない。
他にも、そもそも∈の定義が函数適用なので X ∈ B と書いときにXとBでは型が違うのがすごくキモいとか。キモいというかこれのせいでZFの一部の公理は型があわなくて表現できなかったりもする。

そういうわけでまずは集合を使えるようにするというだけ。
コードは一番下に載っけました。

コードについて

二重否定除去

Relation.Nullary.Negation

elem

属するの演算と2つの公理。
elem-∈は(x : A)と(x ∈ A)がcompatibleになるように。
≡-∈は示せなさそうで必要になったから入れたけど本当に必要なんだろうか。よく分からない。

postulate
  _∈_ : Set → Set → Set₁
  elem-∈ : {A : Set} → ∀ x → x ∈ A → A
  ≡-∈ : {A X Y : Set} → X ≡ Y → X ∈ A → Y ∈ A

公理

仮定したのは以下。

  • 外延性の公理
  • 対の公理
  • 和集合の公理
  • 無限公理
  • 分出公理
  • 冪集合の公理
postulate
  extensionality : {A B : Set} → A ≡ B ⇔ Lift {_} {zero} (∀ x → (x ∈ A ⇔ x ∈ B))
  ∃-paring : ∀(A B : Set) → ∃ \(P : Set) → ∀ x → x ∈ P ⇔ (x ≡ A) ∨ (x ≡ B)
  ∃-union : (A : Set) → ∃ \(B : Set) → ∀ X → X ∈ B ⇔ (∃ \C → (C ∈ A) ∧ (X ∈ C))
  infinite : ∃ \A → (∅ ∈ A) ∧ (∀ X → X ∈ A → X ⁺ ∈ A)
  replacement : (A : Set) → (P : Set → Set₁) → ∃ \B → ∀ x → x ∈ B ⇔ (x ∈ A) ∧ P x
  powerset : (A : Set) → ∃ \B → ∀ X → X ∈ B ⇔ X ⊆ A

空集合の存在だけは(Data.Empty.⊥を使って)示せるので示した。

あとは命題の表現に便利そうな函数とか部分集合とか共通部分とか適当な補題を示したりした。
本に載っているままのやり方だけど

-- ``Russellのparadoxを回避"する命題。
cor-1-4 : (A : Set) → ∃ \B → B ∉ A

も示せた。

コメント

これだけのことが検索しても全くヒットしなくてつらかった。誰もAgdaで数学しないのかなって思った。

あと、仮定した公理が適切なものかどうかもよく分からない。なんか変なことしてたら教えてください。
選択公理とかも入れてもう少し綺麗にしてから自分のライブラリに入れて使おうと思います。

参考にした本

たまたま手元にあった。

集合と位相 (岩波基礎数学選書)

集合と位相 (岩波基礎数学選書)

コード

https://gist.github.com/myuon/ea11f62f9a9a9fed02b0

Printf実装を通して学ぶGADTs, DataKinds, ConstraintKinds, TypeFamilies

問題

問. Haskellで以下のようなCライクなprintf函数を実装してください。

> printf ["Hello, ", _s, "\n", "an integer:", _d, "\n", "a float:", _f] ["World!", (10 :: Int), (3.1415 :: Float)] 

-- 出力結果:
> Hello, World!
> an integer:10
> a float:3.1415

Cのprinfとは異なり、%dや%fが文字列に直接埋め込まれていません。よって当然型が合わなければ、すなわち printf [_d] [(3.1 :: Float)] などとかくとコンパイルエラーになってほしいわけです。

解答

私が実装したものが以下にあります。

https://gist.github.com/myuon/9084939

以下ではこのコードについて解説していきたいと思います。

解説

まず、printfの第一引数も第二引数もそれぞれの元の型はバラバラです。今はまだ_d_fの型をどうするかについては考えていませんが、とにかく型が違うということだけ分かればまずはヘテロリストの実装からスタートすることになります。

GADTs, DataKinds

ヘテロリストは全ての型がバラバラなので型を保持するのではなくてカインドを保持するようにします。つまり、普通のリストは型がaのデータを並べたものですが、今回実装するヘテロリストはカインドが*のデータを並べたものと考えます。

data HList (as :: [*]) where
  Nil :: HList '[]
  (:::) :: a -> HList as -> HList (a ': as)
infixr :::

HListの定義にはGADTとDataKindsが使われています。GADTはデータコンストラクタ函数のように定義できる*1もので、確かに上ではdata ... whereという書き方がされています。

DataKindsは定義したデータコンストラクタを型に、型をカインドに同じ名前のまま持ち上げるものです。分かりやすい例を挙げてみましょう。以下は簡単な型レベル自然数の例です。

data Nat = Zero | Succ Nat

-- DataKinds拡張を使うと、以下のようなものも自動で生成される
-- data Zero
-- data Succ (n :: Nat)
-- ただし Zero :: Nat, Succ n :: Nat である

これによって、標準的なリスト型は[]カインドに持ち上げられ、'[], (':)というデータコンストラクタを昇格してできた型が作られ、*カインドをもつ型のリストが使えるようになります。 このことを踏まえれば上のコードは、HListというデータ型の定義であって、asという変数はカインド*をもつ型のリストになっていることが分かります。(:::) :: a -> HList as -> HList (a ': as)によって、与えられた型をそのままリストに追加しているのが分かります。さらに実際に動かして型を調べてみるとよいでしょう。

> :t Nil
Nil :: HList ('[] *)

> :t "100" ::: (10 :: Int) ::: Nil
"100" ::: (10 :: Int) ::: Nil :: HList ((':) * [Char] ((':) * Int ('[] *)))

TypeFamilies, ConstraintKinds

さて、HListShowインスタンスにできるでしょうか。HListに登場する全ての型がShowインスタンスであればできそうです。このように型への制限を表すのがConstraintで、それをカインドのレベルで扱えるようにするのがConstraintKinds拡張です。

import GHC.Prim (Constraint)

type family All (cx :: * -> Constraint) (xs :: [*]) :: Constraint
type instance All cx '[] = ()
type instance All cx (x ': xs) = (cx x, All cx xs)

TypeFamiliesを使えば型を直接扱う函数を定義できます。これによってAllという型への制限を表す函数を定義します。cx :: * -> Constraintの部分に適当な型クラスがきます。例えばAll Showは、カインド*のリストxsに対し、その全ての元がShowインスタンスになっているという制限を表すことができるわけです。

コレを使ってHListShowインスタンスにしてしまいます。

instance (All Show as) => Show (HList as) where
  show Nil = "[]"
  show (x ::: xs) = show x ++ ":" ++ show xs

-- 実行例
-- > "100" ::: 4.2 ::: 10 ::: [1..5] ::: Nil
-- "100":4.2:10:[1,2,3,4,5]:[]

TextFの実装

以上でヘテロリストが実装できました。これを使えば我々の目的であるprintf函数の型も大体見当がつくでしょう。

printf :: HList as -> HList bs -> IO ()
printf x y = undefined

printfは2つのHListxとyを受け取って、もしもxの先頭がString型であれば、それをそのまま出力します。そうでなければ、xの先頭とyの先頭の型があっているか(xの先頭が_dだったらyの先頭はInt型であるか)を判断して、合っていればそれを出力します。このようにprintfは型によって実装が変わるので、型クラスの出番です。

class TextF as bs where
  textf :: HList as -> HList bs -> String

また、printfはIO ()になって少し扱いにくいので、textf :: HList as -> HList bs -> Stringという純粋函数を定義して、それを使ってprintfを実装することにしました。

いよいよ実装です。まずは、それぞれのリストas, bsがともに空である場合。

instance TextF '[] '[] where
  textf _ _ = ""

そして、asの先頭がString型かどうかでパターンマッチを行います。

instance (TextF as bs) => TextF (String ': as) bs where
  textf (x ::: xs) y' = x ++ textf xs y'
 
instance (TextF as bs) => TextF ((x -> String) ': as) (x ': bs) where
  textf (x ::: xs) (y ::: ys) = x y ++ textf xs ys

asString型のデータか、x -> String型の函数が入っているということにしました。つまり、_d_f_d :: Int -> String, _f :: Float -> Stringの型であって、さらに_d 10_f 3.1415などの値が画面に出力されることになります。 よって、このような_d_fshowそのものですから、これを定義してあげることにします。

_d :: Int -> String
_d = show
 
_s :: String -> String
_s = id
 
_f :: Float -> String
_f = show

(String -> Stringだけは、そのままshowするとクォーテーションがついてくるのでそのままにしてあります。)

まとめ

以上で、printfの実装が完全に出来ました。 では実際に動かして遊んでみましょう。

> printf Nil Nil

> printf ("hello!" ::: _s ::: Nil) ("world!" ::: Nil)
hello!world!
> printf ("hoge:" ::: _d ::: Nil) (3.1415 ::: Nil)
*** 型エラー ***
> printf ("hoge:" ::: _d ::: Nil) ((20 :: Int) ::: Nil)
hoge:20
> printf ("hoge:" ::: 10 ::: Nil) (Nil)
*** 型エラー ***

はい、正しく動いているようです。

なお、問ではこれを printf ["hello","world!"] [] のようにリストカッコを用いて書くように言っていましたが、そのようなリストの表記を使えるようにするGHC拡張として、OverloadedListsが提案されているようです。 また、このprintfをCと同じように可変長引数にすることは頑張ればできると思うのでよければやってみてもいいかもしれません。(丸投げ)*2

GADTs, DataKinds, ConstraintKinds, TypeFamiliesなどのGHC拡張を使えば、このような型レベルプログラミングも比較的[要出典]簡単に実装することができます。便利なGHC拡張はドンドン使っていきましょう。

参考

参考にしたページと参考になりそうなページ

*1:各データコンストラクタの像を適当な形に制限するために使うものだと思っていますが正確なところは知りません

*2:型クラスを用いた可変長引数の実装はText.Printfが分かりやすいと思います。

Haskellでもできる!実践・オブジェクト指向

Lensにほとんど触れたことのない人にはこちらの記事がオススメです:Lensで行こう! - Just $ A sandbox

Haskellでもオブジェクト指向をしましょう!
Haskellは直接オブジェクト指向的な機能を提供してはいませんが、我らがLensの力を借りることでオブジェクト指向的な設計を意識したコーディングが可能です。

今回利用するのは主に以下のモジュールです。

Lensのおさらい

Lensを使ったことのある人にはおなじみだと思いますので、特に解説はしません。

type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t  -- Lens型(GetterやSetterの一般形)
type Lens' s a = Lens s s a a  -- Lensの省略形

(^.) :: s -> Getting a s a -> a  -- 値をgetする
(.~) :: ASetter s t a b -> b -> s -> t  -- 値をsetする
(%~) :: Profunctor p => Setting p s t a b -> p a b -> s -> t  -- 函数を適用したものをsetする
(.=) :: MonadState s m => ASetter s s a b -> b -> m () -- 値をMonadStateの文脈でsetする( (.~)のMonadState版 )
(%=) :: (Profunctor p, MonadState s m) => Setting p s s a b -> p a b -> m () -- 函数を適用したものをMonadStateの文脈でsetする( (%~)のMonadState版 )
(<~) :: MonadState s m => ASetter s s a b -> m b -> m ()  -- アクションを実行した結果をsetする

lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b  -- getterとsetterからLensをbuildする

特に最後のlens函数は重要です。例えば適当なdata型をmakeLensesするとき、何が起こっているかを明示すると

data Hoge a b = Hoge { _foo :: a, _baz :: b }
makeLenses ''Hoge

-- 以下が生成される
foo :: Lens' (Hoge a b) a
foo = lens _foo (\h x -> h { _foo = x })

baz :: Lens' (Hoge a b) b
baz = lens _foo (\h x -> h { _baz = x })

となります。 lensに、getter :: Lens' s a -> asetter :: Lens' s a -> a -> Lens' s aを渡すことで、出来上がるlens getter setterは上手くLensとして振る舞ってくれます。

型クラスとオブジェクト

Lensでオブジェクトを定義しましょう。
例として、ブロック崩しゲームのようなものを考えてみましょう。ブロック崩しには当然、ボールやバーが必要ですのでこれを定義してみます。

data Ball = Ball { _posBall :: (Int, Int), _velBall :: (Int, Int), _r :: Int } deriving (Eq, Show)
makeLenses ''Ball

data Bar = Bar { _posBar :: (Int, Int), _velBar :: (Int, Int), _width :: Int, _height :: Int } deriving (Eq, Show)
makeLenses ''Bar

posHogeはオブジェクトの座標にあたります。わざわざ名前を変えているのは、函数の多重定義になってしまうからです。また、オブジェクトは座標を更新して動かしたいので、このようなメソッドを定義します。
Haskellでは、いわゆるメソッドに当たる部分は型クラスのメソッドとして定義します。メソッドはオブジェクトに関する値を戻り値にとる函数というよりもオブジェクト自体を操作する函数であることが多いのでデータ型とは分けて定義するほうが便利です。また、型クラスのメソッドなら、同じ名前でもデータ型によって異なる振る舞いが定義できます。

class Move c where
  update :: State c ()

instance Move Ball where
  update = do
    (vx,vy) <- use velBall
    posBall %= (\(x,y) -> (x+vx, y+vy))

instance Move Bar where
  -- Barは横にしか動けない
  update = do
    (vx,_) <- use velBall
    posBar %= (\(x,y) -> (x+vx,y))

特に意味はないですが、オブジェクトによって函数の振る舞いを変えることが出来ました。
さて、posBallposBarが同じ座標を表しているのに名前が違うのは何かと面倒なので、これも型クラスを使ってまとめてしまいます。

class HasPos c where
  pos :: Lens' c (Int, Int)

instance HasPos Ball where
  pos = posBall
instance HasPos Bar where
  pos = posBar

はい、これでposBallposBarを区別する必要はありません。これを使えば、posをもつ任意の要素に対するメソッドが定義できます。

reset :: (HasPos c) => State c ()
reset = do
  pos .= (0,0)

resetHasPos型クラスのインスタンスならなんでも適用できます。つまり、BallBarはどちらもresetで操作をすることができるわけです。便利ですね!

Classyとサブクラス

さて、上ではHasPosを定義して名前の衝突を防ぎましたが、これを共通する全ての函数について行わなければならないのは面倒です。そこで、posvelなどの共通するメンバをもつ抽象クラスを作り、BallBarはこれらを内部に含む(ある意味ではサブクラス・継承したクラスのようなもの)クラスとして定義することにしましょう。

data GameObj = GameObj { _pos :: (Int, Int), _vel :: (Int, Int) }
makeClassy ''GameObj

-- 以下が自動生成される
class HasGameObj c where
  gameObj :: Lens' c GameObj

instance HasGameObj GameObj where
  gameObj = id

pos :: (HasGameObj c) => Lens' c (Int, Int)
vel :: (HasGameObj c) => Lens' c (Int, Int)

makeClassyGameObjからHasGameObj型クラスを生成します。これによって、HasGameObjインスタンスになったものは自由にposvelを使えるようになります。
どういうことか見てみましょう。

data Ball = Ball { _ballObj :: GameObj, _r :: Int } deriving (Eq, Show)
makeLenses ''Ball

instance HasGameObj Ball where
  gameObj = ballObj

これでBallHasGameObjインスタンスになったので、b :: Ballに対してb ^. posとかb & vel .~ (1,0)などとかけるようになったわけです。

また、少しデザインパターン的ですが、自分自身を更新する函数を内部に持つオブジェクトの定義も出来ます。
同じ型を持つオブジェクトの実装を変えられるようにしたい -qiita

これは、例えば変な動きをするボールを作りたいときに、ボールの動きをデータの生成時に指定したいみたいな状況で使えると思います。
(上の記事のAutonomieの実装を参照。autoを例えばBall型で、runAutoState Ball ()とすればこのような実装も可能。)

ここまででかなりのことはできるようになったと思います。
今回は記事タイトルの通り、「実践」を意識した解説を行いました。例えば私はChimeraという弾幕シューティングゲームを全てHaskellで実装していますが、Lensはこれくらい本格的なプロジェクトになっても通用するレベルの強力さを秘めています。

Lensは(たぶん)他にも使い方があります。あなたもこの強力なライブラリで快適なHaskellコーディングを楽しみましょう!
さあいますぐインストール! *1

*1:2014/02/02時点でlens-4.0がリリースされています。

2ヶ月くらいでノベルゲームを作った話

発端


で2ヶ月くらいでノベルゲーム(正確にはデジタルノベル、あるいはヴィジュアルノベルと呼ばれるものです)を作りました↓*1

チェイン・コンプレックス

ので、今回のプロジェクトについてまとめます。

製作にあたって

必要になったもの

  • ノベルエンジン: 吉里吉里/KAG
  • 企画・シナリオ
  • ノベルエンジン・スクリプト・フォント
  • キャラクター立ち絵
  • 背景(写真を加工→後述)
  • BGM/SE
  • 宣伝するところ
  • (やる気・根気)

企画・シナリオ・キャラクター立ち絵・スクリプトに関しては自分でなんとかして、あとのものは借りてなんとかしました。 借りた素材やらのリンクはリンクページにリンクを貼っておきました。

製作過程

1. 企画・プロット

今回は一人のプロジェクトだったので企画書のようなものは作ってません。プロットを書きながらあんなことをしたいこんなこともしたいでずっとごにょごにょやってました(後で色々変更したけど)。

モチベーション上げるために好きなノベル作品の思い出に浸ったりもしてました。

今回は作品が作品だっただけに、プロットを書くにあたってグラフエディターのようなものが欲しかったので yEd - Graph Editor を使いました。

2. シナリオ

最終的にシナリオは270KBです(お話に関係のあるシナリオファイルのファイルサイズ)。
シナリオは80%かくのに3週間ほどかかってしまって、なかなか大変でした(主に中だるみ)。書いていてつらい、しんどいなどの症状が出たらそれはシナリオがつまらない可能性があるなと思ってプロットを見直したりもしていました。

今回の作品は前半部分が「恋愛パート」、後半部分が「SFパート」の形になるお話だったので、前半後半で気分も切り替えられて良かったと思います(前半はずっと幼馴染み可愛いしか言ってなくて、後半はずっと頭をひねりながら矛盾が出ないようにプロットをいじってました)。

時間もかかったけど楽しかったです。今もそれなりに満足しています。

アウトラインプロセッサと呼ばれるソフトも導入しました。使ったのはこちら→ Olivine Cafe - OlivineEditor

3. 背景

背景は写真素材を頑張って加工しました。
写真素材を使ったのは、そちらの方が圧倒的に素材の数が多かったからです(「〜のシーン背景が欲しい」などの要望がある場合はイラスト素材だと難しいことがあります)。

加工はそれなりに難しいですが、比較的うまくやると以下のような感じになります(写真はhttp://ruta2.fc2web.com/frame.htmlより)。

f:id:myuon_myon:20131201034227p:plain

加工に際しては 写真を絵のように見せる写真加工技術「PhotoDramatica」トップ - あやえも研究所 を大いに参考にしました。

これだけあればそれなりのことはできます。ただし適度に妥協が必要です。

4. キャラクター立ち絵

リリース3日前に描き直したりと色々ありましたがなにより可愛く描けたと思うのでとても気に入ってます。
チェイン・コンプレックスでサンプルが見れます。

ちなみに枚数は、 幼馴染み表情差分16パターン+クラスメート表情差分16パターン+その他2枚 の立ち絵を用意しました。
ただ「笑い」「泣き」みたいに用意していたんですが、より細かく
「笑い(コミカル)」「笑い(爆笑)」
「泣き(コミカル)」「泣き(大泣き)」
のように、それぞれ喜怒哀楽について2パターンくらい用意しておけばなんとかなったのではないかなと思います。

不思議・困惑などの差分も用意しましたが、シーンによっては合っていないようなところもあったので、分かりやすく「笑いA・B」「泣きA・B」のようにした方が立ち絵の選択にも迷いにくかったかなと思っています。

5. スクリプト

システムボタンプラグインは公式で配布されているものを自分で改造しました(テキストボタンが使えるように)。

さて、YesNoDialogLayerスクリプトはデフォルトだとYes/Noダイアログが開くようになっている部分をレイヤーベースのものに書き換えるプラグインです。これが実は厄介で、ダイアログの場合はYes/Noのどちらを押したかが戻り値として返ってきますがこれはレイヤーベースなので表示する瞬間とYes/Noが確定するタイミングはずれます(ダイアログを表示する瞬間は必ずfalseが返される)。
そしてそこの処理とセーブロードプラグインの「読み込みますか→はい/いいえ」の処理が丁度バッティングするので、「Yesを押した時〜する」という処理をキチンとフックしてあげないといけないわけですが、これに気が付かず、ここに起因するバグフィックスにそれなりに時間を取られました。

よってYesNoDialogLayerスクリプトを入れる際には、既存のプラグインがダイアログボックスを使っていないかどうかしっかり吟味してから導入した方がよいと思います…。

6. BGM/SE

SEは特に言うことないです。ググって良さげなものを探して借りました。

BGMは選定に非常に時間がかかるので、予め片っ端から聴いておき、使えそうな曲には

BGM001.ogg: 主人公が幼馴染みと喧嘩してから一夜明け、なんとなく気まずい雰囲気

みたいに、どういうシチュエーションで使える曲かを細かくメモっておけば時間短縮になります。ただ明るい、暗いだけでは大雑把すぎるので曲に対してシーンを作るとしたらどうなるだろう?と考えてメモを作ると意外と曲の選定で迷いません。

あと、50MB程度あるzipのうち半分はBGMが持っていってるので、調子に乗って色々使いすぎないほうがいい気はします。

7. リリース

リリースは個人サイトの一部に専用ページを作りました。Bootstrap を使ったのでほとんど時間もかかっていません。

zipファイルはSimple File Sharing and Storage.ふりーむ! - フリーゲーム/無料ゲーム 5000本!にアップロードしました。
アップローダーとしてMediaFireを選んだのはうるさい広告がなかったことと、ダウンロードする人への制限があまり厳しくなかったからです。ふりーむ!をはじめとしてフリーゲーム紹介サイトなどには積極的に登録しました。

リリースして少ししてから、レビューを書いていただきました。とても嬉しいです!ありがとうございます。

どちらのレビューにもシステムが不安定と言われていて、実際バグがあったわけなんですが、こういうのをレビュー媒介でしか知れないのは色々アレなので掲示板は作っておいたほうがいいなと思いました(現在は掲示板も設置してあります)。

v2.0でシステムバグはそれなりに解消したつもりですが、v1.0公開から少し間が空いてしまったことは本当に申し訳ないと思っています。

まとめ

2ヶ月という短いスパンでの開発でしたが、考えれば無駄もたくさんあり、この程度の規模のゲームなら慣れれば1ヶ月程度でできるのではないかなと思います。

また、開発にあたっては全てUbuntuとWineを使って行いましたが吉里吉里は全く問題なく動いてくれました。Wineはとても優秀です。
(ただし主に使っていたエディター(KKDE)はWineの上だとそこそこ不安定だったのでWindowsを使ったほうが無難だとは思います。また、テストプレイはWindowsで行なうべきです…当たり前ですが。)

12/1現在でDL数も400を超え、当初予想よりも遥かに色んな人にプレイしてもらえたみたいでとても嬉しかったです(主にレビューのおかげです)。
それなりに色々やらかしたりもしていて、シナリオ修正とかバグフィックスとかあれこれ大変なこともありましたけど何より楽しかったのでとてもいい経験になりました。

思っていたよりも簡単に、それらしいものができたので満足しています。もしも次があれば、今回の経験も踏まえてもっとよいものを作りたいと思います。
このまとめがこれからゲームを作る誰かのお役に立てれば幸いです。

*1:ゲームの内容とチェイン複体は何の関係もありません。なんとなく名前をつけただけです。