KLabGames Tech Blog

KLabは、多くのスマートフォン向けゲームを開発・提供しています。 スマートフォン向けゲームの開発と運用は、Webソーシャルゲームと比べて格段に複雑で、またコンシューマゲーム開発とも異なったノウハウが求められる領域もあります。 このブログでは、KLabのゲーム開発・運用の中で培われた様々な技術や挑戦とそのノウハウについて、広く紹介していきます。

(本稿はKLab Advent Calendar 2017 の1日目の記事になります)

2017年のKLabのアドベントカレンダーです。最初はoho-sです。よろしくお願いします。

自分が作ったVRコンテンツをどんなのか説明したい!

VRコンテンツを作っていて、自分が作ったVRコンテンツをどんなものか説明したり共有したい時ってありませんか? ハイスペックPCやVR用HMDを持っていない人にも、雰囲気だけでも伝えたい。そんな時に便利なのが、いわゆる360°動画でのキャプチャです。 今回は、Facebookが公開している、360-Capture-SDKを使ってキャプチャしてみます。日本語での使い方の情報が探してもあまりなかったので、参考になれば幸いです。

Facebookの360-Capture-SDKを使ってみる

360-Capture-SDKの動作環境は、こちらを参考にしてください。 Windows(64bitのみ)の8以降で、NVIDIAもしくは、AMDのGPUが必要になります。各ドライバのバージョン指定があるので確認してください。 対応しているUnityのバージョンは、README.mdに記載がありませんが、今回Unity 5.5.3p3 (64-bit)で動きました。一方、Unity 2017.2.0p2 (64-bit)では、動画のキャプチャはできましたが、画面の表示がされないなどの不具合が見られました。

さて、では使ってみましょう。まず、キャプチャしたいUnityプロジェクトにSDKを組み込みます。 360-Capture-SDKが公開されているリポジトリは、こちらです。 このリポジトリをcloneしてきて、 Samples/Unity/Assets 以下のEncodePackageフォルダとPluginsフォルダをそのまま組み込みたいプロジェクトのAssets以下にコピーします。

次に、EncodePackage内の、EncoderObjectプレファブをシーンに置きます。

組み込み

そして、EncoderObjectのインスペクターからいくつかの録画用パラメータなどを修正などします。 負荷とクオリティを考えて、ピクセル数などを選びましょう。 EncoderObjectの位置がキャプチャの中心位置になるので、適切にPositionを設定します。少し離れた位置にすると、観客視点とかもできると思います。

最後にキャプチャをします。 プロジェクトを実行して、キャプチャしたいポイントでF2キー(デフォルトでは。インスペクターで変更可能)を押すとキャプチャ開始、F3キーで停止です。キャプチャした動画は、プロジェクトフォルダのGallery内に保存されます。

動画のメタデータの調整

ここまでの手順で作成した動画を、そのままYouTubeやFacebookに投稿しても360°動画再生の専用プレイヤーになりません。 動画に360°動画であることのメタデータを付けてやります。

そのためのツールが、こちらになります。

展開して実行すると下図のようなダイアログが出てくるので、「Open」からキャプチャした動画ファイルを選び、「Spherical」 のチェックボックスをオンにして「Inject metadata」します。以上で新しい動画ファイルができたと思います。

ダイアログ

アップロードしてみる

通常の手段でアップロードします。FacebookやYouTubeであれば、自動的に先ほどの手順でつけたメタデータに基づいて処理してくれて、360°動画として扱われるはずです。

サンプル動画ファイルリンク

まとめ

以上のように、比較的容易に360°動画でのキャプチャができてしまいました。 VRコンテンツのプロモーションなどに使えるのではないかと思います。 是非試してみてください。

最後に余談ですが、EncoderObjectのインスペクターを見ていると、どうもキャプチャーした動画のストリーミングができるようですが、試してみたところうまく動きませんでした。 この辺りも面白そうなので、今後調査を進めてみたいと思います。

KLab Advent Calendar 2017 の2日目は、haltさんです。よろしくお願いします。

Webでとにかく高速に計算したい

やまだです。Webでとにかく高速な計算を行うために人生の何%かを使っています。
前回はJavaScriptから直接SIMD.jsを呼びましたが今回はEmscriptenを使用し、C言語からSIMD命令を呼び出してみます。

題材としては定番ですがマンデルブロ集合を使用します。

mandelbrot_glsl

マンデルブロ集合は以下の漸化式で計算が可能でしばしば並列演算の課題としてとりあげられます。

mandelbrot0

z は複素数なので実部と虚部をXY平面に表すと以下のようになります。

mandelbrot1

mandelbrot2

Emscriptenを使う

今回はWebでということでC言語のコードをJavaScriptコードにコンパイルするEmscriptenを使用します。
Emscriptenを使用するとasm.jsを利用した最適化をかけることができるため単純にJavaScriptで実装した時よりも高速になることがあります。
Emscriptenでは -O1 以降を指定するとasm.jsが有効となります。今回は -O3 を使用して計測しました。

Emscriptenでコンパイルすることを前提としてCでマンデルブロ集合を実装すると以下のようになります。

#define N (500)

void compute(int bufferLength)
{
  for (int i = 0; i < N; i++)
  {
    for (int j = 0; j < bufferLength; j++)
    {
      float zx = zxBuffer[j];
      float zy = zyBuffer[j];

      zxBuffer[j] = zx * zx - zy * zy + cxBuffer[j];
      zyBuffer[j] = 2.0 * zx * zy + cyBuffer[j];
    }
  }
}

全ピクセルに対してN回ループする必要があるため非常に重い処理であることがひと目でわかります。
実行時間はマンデルブロ集合のループ計算を開始してからテクスチャ用のRGBバッファに変換するまでの時間を計測しています。

SSE: disabled
Thread: 1
Width: 1024
Height: 1024
PixelRatio: 2.0
Step: 500
Time : 3414ms

スレッドを使う

compute関数の内側のループはスレッドを使用して分割できそうですのでこちらに挑戦してみます。

Emscriptenはマルチスレッドライブラリであるpthreadを実験的にサポートしています
コンパイル引数に-s USE_PTHREADS=1を加えることによりpthreadを有効にできます。
ただし、ECMAScriptのドラフト仕様であるSharedArrayBufferに依存しているため、2017年6月現在Firefox Nightlyでのみ動作します。

#define N (500)
#define NUM_THREADS (2)

// マンデルブロ集合を計算する
static void *compute(void *args)
{
  THREAD_ARGS *threadArgs = (THREAD_ARGS *)args;
  int min = threadArgs->min;
  int max = threadArgs->max;

  for (int i = 0; i < N; i++)
  {
    for (int j = min; j < max; j++)
    {
      float zx = zxBuffer[j];
      float zy = zyBuffer[j];

      zxBuffer[j] = zx * zx - zy * zy + cxBuffer[j];
      zyBuffer[j] = 2.0 * zx * zy + cyBuffer[j];
    }
  }

  return NULL;
}

// スレッドを作成する
static void create_threads(int bufferLength, pthread_t **threads)
{
  for(int i = 0; i < NUM_THREADS; i++) {
    // 分割する
    int min = i * bufferLength / NUM_THREADS;
    int max = (i + 1) * bufferLength / NUM_THREADS;

    // スレッドを作成
    pthread_create(threads[i], NULL, compute, (void *)get_thread_args(min, max));
  }
}

結果は以下のようになりました。
単一スレッドで実行した時に比べて1.7倍程度高速化できています。
計測環境はCPUコア数が2であったこともあり、4スレッドにしたとしてもパフォーマンス向上は体感できませんでした。
ですが、コア数がもっと多いCPUですと演算器の数の制限などはあるでしょうが、スレッド数を増やすことによりパフォーマンスが向上することが期待できます。

SSE: disabled
Thread: 2
Width: 1024
Height: 1024
PixelRatio: 2.0
Step: 500
Time : 1952ms

SIMDを使う

さて、もう一つの高速化の方法として1命令で複数の計算処理が可能なSIMD命令を使用してみます。
SIMD命令に対応しているブラウザでのみ動作します。

SIMDを使用するにはいくつか方法があります。

  • LLVMの自動ベクトル化機能を使用する
  • GCC/Clang固有のSIMD拡張を使用する
  • IntelのSIMD拡張であるSSEを使用する

今回はSSEを使用します。
IntelのSIMD拡張はMMXやAVDなどがありますがEmscriptenはSSE1, SSE2, SSE3, SSSE3のみ対応しています。
SSEを使用するにはコンパイル時に-msseオプションを指定します。

SSEを使用する場合は128ビット幅の__m128を使用します。__m128には32ビットfloatが4つパックされています。
_mm_add_ps_mm_mul_psがSSE用の関数ですので演算にはこちらを使用します。
見ての通り_mm_add_psが加算、_mm_mul_psが乗算APIとなります。
公式リファレンスにアラインメントの指定なども書かれているので、こちらの指示に従った形でメモリ確保をする必要があります。
SSEは16ビットにアラインされたバッファが必要となるため、専用のaligned_allocでメモリを確保します。
ですがaligned_allocはEmscriptenでビルドすると関数が見つからずにエラーとなってしまったため、Emscriptenのbenchmark_sseで使用されているマクロを使用することにしました。

#define aligned_alloc(align, size) (void*)(((uintptr_t)malloc((size) + ((align)-1)) + ((align)-1)) & (~((align)-1)))

// 項zと定数cのバッファを確保する
static float *zxBuffer = NULL;
static float *zyBuffer = NULL;
static float *cxBuffer = NULL;
static float *cyBuffer = NULL;

static void alloc_bufers(int bufferLength)
{
  zxBuffer = (float *)aligned_alloc(16, bufferLength);
  zyBuffer = (float *)aligned_alloc(16, bufferLength);
  cxBuffer = (float *)aligned_alloc(16, bufferLength);
  cyBuffer = (float *)aligned_alloc(16, bufferLength);
}

static void compute(int bufferLength)
{
  const __m128 two128 = _mm_set1_ps(2.0);

  // floatを4つ同時に計算するため4で割る
  // 即ちバッファの長さは4の倍数である必要がある
  int bufferLength128 = bufferLength / 4;

  // SIMD型にキャストする
  __m128* zxBuffer128 = (__m128 *)zxBuffer;
  __m128* zyBuffer128 = (__m128 *)zyBuffer;
  __m128* cxBuffer128 = (__m128 *)cxBuffer;
  __m128* cyBuffer128 = (__m128 *)cyBuffer;

  for (int i = 0; i < N; i++)
  {
    for (int j = 0; j < bufferLength128; j++)
    {
      __m128 zx = zxBuffer128[j];
      __m128 zy = zyBuffer128[j];

      __m128 cx = cxBuffer128[j];
      __m128 cy = cyBuffer128[j];

      // SSEを使用して4つまとめて計算する
      __m128 tx = _mm_mul_ps(zx, zx);
      __m128 ty = _mm_mul_ps(zy, zy);

      zxBuffer128[j] = _mm_add_ps(_mm_sub_ps(tx, ty), cx);
      zyBuffer128[j] = _mm_add_ps(_mm_mul_ps(two128, _mm_mul_ps(zx, zy)), cy);
    }
  }
}

実行結果は以下の通り3414msから1659msに約2倍程度高速化しています。
理想を言えば4倍程度になって欲しいのですが複素数をRGBに変換する処理などいくらかオーバーヘッドが発生しています。

SSE: enabled
Thread: 1
Width: 1024
Height: 1024
PixelRatio: 2.0
Step: 500
Time : 1659ms

SSEとpthreadの併用

browser

さて、ではSSEとpthreadは同時に使えないものかと思い併用してみました。
ソースコードは省略しますがあっさりうまくいってしまい、3倍程度の高速化に成功しました。

SSE: enabled
Thread: 2
Width: 1024
Height: 1024
PixelRatio: 2.0
Step: 500
Time : 1083ms

Chromeでは?

Google Chromeは残念ながらSSEもpthreadも対応していません。
ですがasm.jsには対応しているのでSSEやpthreadを無効にして実行してみたところ、
同じコンパイルオプションでFirefox Nightlyよりも良好なパフォーマンスを得ることができました。
JavaScript実行エンジンの違いでの差ということになります。

SSE: disabled
Thread: 1
Width: 1024
Height: 1024
PixelRatio: 2.0
Step: 500
Time : 2065ms

WebAssembly

本当はWebAssemblyでコンパイルしたかったのですが、以下のようなエラーがでていました。

Traceback (most recent call last):
  File "/Users/yamada/emsdk-portable/emscripten/1.37.9/emcc", line 13, in <module>
    emcc.run()
  File "/Users/yamada/emsdk-portable/emscripten/1.37.9/emcc.py", line 1278, in run
    assert not shared.Settings.USE_PTHREADS, 'WebAssembly does not support pthreads'
AssertionError: WebAssembly does not support pthreads

まだ、pthreadは対応していないようです。

まとめ

処理時間をまとめてみました。かなり効果的に高速化されています。
今後はSSEやpthreadを使った高速化に積極的に挑戦していきたいです。

Firefox Nightly SIMD及びマルチスレッド化なし 3414ms
Chrome SIMD及びマルチスレッド化なし 2065ms
Firefox Nightly マルチスレッド化 1952ms
Firefox Nightly SIMD化 1659ms
Firefox マルチスレッド化 + SIMD化 1083ms

Firefox Nightlyは他の環境で試してみたところ処理するスレッドは1スレッドだったとしても、
pthread_createを使用してメインスレッドで処理せずに一つのサブスレッドで処理した場合のほうが高速だったこともありNightly Buildということもあり結果が安定していない印象を受けました。

と、ここまでSIMD推しできましたが直近ちょっとした事件が発生しました。
ECMAScriptの新仕様としてSIMDは議論が続けられてきましたがInactive Proposalに移動しました

今後はWebAssemblyの一部としてSIMDの実装は続けられていくようです。

マルチスレッドやSIMDは従来はWebになかったチューニング手段です。
ゲームを始めとしてWebがプラットフォームとして育っていくのを見るとわくわくしますね。

参考

こんにちは、@trigottです。この記事では、社内で行っている Agda ハンズオンの紹介をします。

はじめに

Agda とは、依存型の使える関数型プログラミング言語、あるいは定理証明支援系です。Coq などとは違いタクティックは使わず証明項を直接記述するスタイルですが、Emacs 上で対話的に証明を進めるためのインタフェースが用意されているため、効率的に証明を進めることができます。Agda で n * 2n + n が等しいことを証明する動画を撮影してみました。雰囲気がつかめれば幸いです。

KLab では月に1回 ALM(All Layers Meeting)という社内勉強会を開催しています。学生のころから Agda が好きで触っていたこともあって、Agda に関する発表をしたところ、先輩からハンズオンを開いてほしいということを言われました。ハンズオンとかやったことないし、Agda も人に教えられるほどではないし・・・と最初は不安だったのですが、まあ全3回くらいでやってみよう、という軽い気持ちで開催することにしました。社内から参加者を募り、集まるか不安でしたが5人の方が参加してくれることになりました。この勉強会は昨年の10月から始まり、現在も継続中です。

ハンズオンということで、一人で進められるような資料を作成しました。具体的には、資料は Agda のプログラムとして実行可能なファイルで、コメントとして説明を記載し、さらに演習として、埋めるべき箇所を指定したプログラムを所々に配置しています(Software Foundations の真似をしました)。演習の問題は以下のように作成しました。

-- ==================================================================
-- Exercise: (2 star) app-assoc
-- _++_ の結合法則を証明してください。_++_ は右結合なので、xs ++ ys ++ zs
-- は xs ++ (ys ++ zs) と解釈されます。
-- ==================================================================

app-assoc : ∀ {A : Set} (xs ys zs : List A)
            → xs ++ ys ++ zs ≡ (xs ++ ys) ++ zs
app-assoc = ?

2 star は問題の難易度を示しています。特に基準を設けず難易度付をしてしまったせいで、あてになりません。コメントに問題の解説を書いています。問題の本文は実際の Agda のプログラムです。基本的にどれも証明すべき命題=プログラムの型だけを記述し、値は ? だけの未完成なものになっています。Agda ではプログラムの代わりに ? を書くことができ、プログラムとしては不完全ですがコンパイルを通すことができます。なので、まだ解けていない問題がある状態でプログラムをコンパイルしてもエラーにはなりません。また、Emacs でファイルをロードすると埋めるべき ? の一覧が表示されるので、現在の進捗が分かります。

資料は https://github.com/krtx/agda-handson にあります。最初は全3回くらいで終わる予定でしたが、資料を作成しているうちに内容が膨らみ、気づいたらDay1からDay6までの全6部構成になっていました。以下、各ファイルについて解説と作成時の苦労について書きます。

Day1

一番最初に作ったので、一番気合が入っていて、一番長いです。真偽値と自然数を題材にして Agda での基本的な定理証明の仕方を解説しています。≡などの文字の入力の仕方や、Emacs でのコマンドを使った対話的な証明のやり方などです(そう、このハンズオンは Emacs が前提です)。Day1 の最後は、自然数の大小関係を定める2つのデータ型が互いに等価であることを証明する問題になっています。Day1 と言いつつ、1日ではまったく終わりませんでした。

Day2

等しいことの証明をする際によく使われる Rewrite パターンと equational reasoning combinator というものについて(あとおまけで自動で証明してくれる SemiringSolver について)解説しています。Day2 の演習の最後は (a + b) * (c + d)(a * c + b * c) + (a * d + b * d) が等しいことを証明する問題です。Rewrite パターンか equational reasoning combinator を使ってこの問題が証明できれば、初等的なものに限れば等しいことの証明は大体できるのではないでしょうか。

Day3

新しい構造としてリストの解説を、またリストに関する証明を題材として With abstraction の解説をしています。真偽値→自然数→リストという順番でデータ構造を紹介するのは、構造が徐々に複雑になっていくという点で自然に難易度を上げることができているのではないかと思います。rev-involutiverev-injective は Software Foundations のものを真似しています。with abstraction が説明できたので with abstraction を使うことで実現できる inspect パターンというものも説明しようと思ったのですが、例が思い浮かばず断念しました。

Day4

レコード型及び依存型を伴うレコード型について解説しています。レコード型の例として二次元平面上の点を定義し、それを使ったマンハッタン距離に関する性質の証明を演習としています。マンハッタン距離が三角不等式を満たすことの証明はやってみると意外と面倒なのですが、面白かったのでそのまま演習に残しています。ただレコード型の理解に貢献する問題ではないので、余力がある人向けとなっています。この辺から例を考えるのがかなりしんどくなっています。

Day5

偽及び Absurd パターンの解説をしています。偽についての説明は、自分の力量不足で怪しいかもしれません。演習には古典論理にまつわる命題をいくつか与えており、そのために必要なので「かつ」と「または」についても解説しています。

Day6

最後は新しいことはなしで、これまでの知識を使って正しいソートアルゴリズムを定義するという演習です。どこまでヒントを出すかは悩みましたが、ソート済みであることなどの定義はすべて与えて、ソートするプログラムだけを書いてもらう形にしました。insert-sort は単にソートするだけでなく、命題を見ると結果のリストがソート済みであることも要求しています。想定解法では、ソートをしつつ証明も同時に行うようにしています。このように、証明とプログラムが一緒になった証明のスタイルを intrinsic な証明と呼び、一方プログラムを単体で書き、それに対する証明を別で与えるスタイルを extrinsic な証明と呼びます。Agda では intrinsic な証明が多いようなので、insert-sort の型もそれを推奨するように作ってみました(ただ説明がないので、ちょっと中途半端...)。

やってみての感想

実際にハンズオンをしていく中で出てきた感想です。

refl が分からん

Day1 である2つの項が等しいとはどういうことか、またそれはどのようにして証明できるか、について説明したのですが、これが分からないという意見が非常に多かったです。Agda では等しいという関係 _≡_ は以下のように定義できます。

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {x} → x ≡ x

以下のような点から、_≡_ を理解するのは非常に難しかったようです。

  • 関係をデータ型として定義するというのは、普通のプログラミングでは出てこない考え方であること
  • _≡_ という型自体が値を受け取っていること(依存型)
  • refl の引数が implicit になっていること
  • Agda が値を比較する際には正規形に計算してから比較するため、プログラムの字面とは違う値が比較されていること

等しいというのはとても馴染み深い関係のように思えるにもかかわらず、初心者にとっては超えるべきハードルがいくつもあります。自分でも説明に窮する場面が何度もあり、まだまだ十分に理解できていないなと感じました。もう少し簡単な関係から始めるべきだったかもしれません。

Agda がどこまで計算してくれるのか分からん

Day1 では足し算を以下のように定義しています。

_+_ : ℕ → ℕ → ℕ
zero    + m = m
(suc n) + m = suc (n + m)

このため、以下の命題中に現れる (suc x) + y という項は suc (x + y) に計算されます。

prop : ∀ x y → (suc x) + y ≡ suc (x + y)
prop = refl

refl は対応する命題の左辺と右辺が同一の項であることを要求します。(suc x) + y という項と suc (x + y) という項は構文解析をした時点では違う形ですが、Agda によって (suc x) + ysuc (x + y) に計算されるため、refl を使うことができるようになります。このように、Agda が自動で計算を行うということを知っていないと、なぜ証明が通るのかが理解できません。また、足し算の定義を覚えていないと、どこまで計算が進むかも分かりません。自分もこの辺りの理解が甘く、テキストには解説を書けていませんでした。

名前が読めない

Agda の標準ライブラリを見ていると、n ≤ m → n ≤ suc m という命題に n≤m⇒n≤sm という名前をつけるなど、空白だけ詰めた名前を採用していることが多いです。Agda では : など一部の例外を除いて基本的に空白で区切られるため、n≤m⇒n≤sm のような名前でもひと続きの識別子として認識されます。このハンズオンでも同様の命名法を採用したのですが、やはり n≤m⇒n≤sm はひと続きの名前としては認識しづらいとのことでした。

rewrite はロードが必要

rewrite は 文脈中のある項を別の項で置き換えるパターンです。以下の例のように使います。

posulate
  A : Set
  a : A
  b : A
  eq : a ≡ b

lem : suc a ≡ suc b
lem rewrite eq = {! ここの命題は suc b = suc b となる !}

ただし、rewrite を書いただけでは反映されません。rewrite を書いてからロードして初めて文脈に反映されます。テキストのなかでも注意がなかったため、ここで戸惑う参加者の方が多かったです。

reasoning combinator はよしなに推論してくれない

Day2 ではある2つの項が等しいという命題について、rewrite と reasoning combinator それぞれを使った証明法を解説しています。上述の例と同じ命題を reasoning combinator を使って証明すると以下のようになります。

lem′ : suc a ≡ suc b
lem′ = begin
  suc a
    ≡⟨ cong suc eq ⟩
  suc b
    ∎

rewrite の場合は eq だけを指定すればよかったのですが、reasoning combinator を使う場合は suc がついていることを明示してあげる必要があります。

reasoning combinator は対象となる項を書く必要があり、また完全な証明を与えなければならないため、冗長な記述になります。ですが、冗長になっている分、説明が多いためこちらのほうが分かりやすくなっています。実際参加者の間では rewrite による証明よりも reasoning combinator を使ったほうがわかりやすいと評判でした。

標準ライブラリに何があるか把握するのが難しそう

演習を進めていく上で補題が必要になったとき、それが標準ライブラリにあるかどうかが分からない、という声がありました(このハンズオンでは標準ライブラリの解説は対象外にしていたのでそのあたりの話は特にテキストには書きませんでした)。これは実際もっともで、自分もいまだにどのように探せばいいのか分かりません。補題を探すときはファイルを標準ライブラリから直接目で見ることが多いし、モジュールの構成も完全には頭に入っていません。どうすればいいんでしょうか。

1週間空くと何をやっていたか忘れる

普通のプログラミングではないし、週に1時間しかやっていないため、どうしても前回やっていたことを忘れてしまうという声が多かったです(1時間の最初は前回やっていたことを思い出すところから始まる)。しょうがないところもあるとは思いますが、この問題に対しては対策を思いつきませんでした...。

おわりに

初めにも書いたとおり、当初は3回完結の想定(本気で3回でソートまでできると思っていた)だったし、やる内容からしても(そして最初の依頼に沿う形としても)ハンズオン形式が相応しいと考えて、ハンズオン用の資料を作成しました。ところが、蓋を空けてみるともう半年以上も続いています。ハンズオンという自分で進める形式の勉強会が長期に渡ると、参加者の間で進度に差が出てしまうという問題が発生します。途中から参加者が少ない場合は開催を中止するようにして、なるべく差が出ないよう配慮をしました。

ハンズオンをやることになったときに思ったことの1つとして、Agda が非常に入門難易度の高い言語であり苦労した経験から、自分が教えることでその障壁を少しでも和らげることができたらいいな、ということがありました。同じ証明支援系である Coq などと比較すると、決定版と言えるような教科書はなく(教科書は最近出版された1冊だけあり、入門にはよさそう)、日本語の情報もそこまで多くはありません。一体、世間の人はどのようにして Agda を学んでいるのでしょうか? 標準ライブラリを使いこなしている人間がどれだけいるのか、気になります。

↑このページのトップヘ