2020年04月27日

Agdaのデータ型宣言により定義される要素の型

研究室の輪講がらみだが、Agdaのデータ型宣言とコンストラクタの暗黙的パラメータについてごちゃごちゃになったのでここにメモ。

以下のようなデータ型宣言があったとする。

data T {a : A} (b : B) : X -> Set where
C1 : {c1 : C1} (d1 : D1) : T b x1
C2 : {c2 : C2} (d2 : D2) : T b x2

x1(またはx2)はaやbやc1やd1(c2やd2)からXの項が作られているものとする。

このとき、生成される要素は以下の3つである。

T : {a : A} -> (b : B) -> X -> Set
C1 : {a : A} -> {b : B} -> {c1 : C1} -> (d1 : D1) -> T {a} b x1
C1 : {a : A} -> {b : B} -> {c2 : C2} -> (d2 : D2) -> T {a} b x2


簡単に説明。

  • Tは比較的そのまま。あえて言えばコロンが矢印になっているくらい。

  • C1とC2は引数に「Tのパラメータだったもの」が先頭の暗黙的パラメータとしてくっついている。ただしコロンより後ろに書かれていたXはない。


つまるところ、影響があるのはTの宣言でコロンの前に書かれたaやbである。

  • Tにとっては、コロンの前後にかかわらず「この型が取るパラメータ」であるため、基本的に宣言そのままの引数になる。

  • Tのコロンの前にあるパラメータaとbはこの型宣言全体で可視なパラメータである。各コンストラクタはaやbを使える。一方残りの型Xのパラメータについては(今回は無名であるのもあるがそうでなくても)型宣言全体では見えず、あくまでSetまで書かれた範囲でしか見えない。


このようにaやbは可視範囲が広いので、コンストラクタが独立して存在するにあたり相当する値をどこかから拝借しなければならない。結果としてaやbは暗黙的パラメータとして追加される。
もちろんよほどのことがない限りこのパラメータを明示的に渡すことはない(必要とされる型から自動で推論される)が、c1やc2を渡そうとする際に若干ややこしいことになるので注意。({c1 = ...}のような書き方をすると問題を回避しやすい)

なお、このパラメータは便利なのだが、コンストラクタ記述時に制約がつく。
定義時、全てのコンストラクタの型はTに(aや)bを適用した型で終わることが要求される。今回の例で言えば、必ず結果が T {a} b ... の形の型でなければならない。一方、型Xのパラメータについてはそのような制限はなく、コンストラクタ毎に異なってよい(x1とx2は異なってよい)。
あと、この制約は「結果の部分」にのみかかり、コンストラクタのパラメータにTが出現しても(aや)bを使う必要性は無い。

_≡_ の定義が複雑な考えと思うかもしれないが落ち着いて読めば読める。
xが型パラメータにあるのはコンストラクタで第一引数が固定されても特に影響ないため。
第二引数が第一引数と同じという制約はあくまでコンストラクタで行う。
posted by chiguri at 20:22| Comment(0) | Agda

2013年12月06日

よしひろさんの問いにAgdaで答えよう

これはTheorem Prover Advent Calendarとはまったく関係のない記事である。
いや、来週くらいに書くけど。

昨日(世界のどこかの時間では)の担当だったよしひろさんが書いた記事
依存関係のある値のうちの一部をrewriteしようとしたときの問題
に最後にこんな一言があった。
> また、依存型に定評のあるAgdaではどうなるかなども興味深い。

なるほど、この問いには答えねば。
そう思いAgdaを起動してまねた記述を作る。
ファイル名はYIquestion.agdaとする。

module YIquestion where

open import Data.Nat
open import Relation.Binary.Core

postulate
f : (n : ℕ) → n > 0 → ℕ
h : (n : ℕ) (H : 2 * n > 0) → f (2 * n) H ≡ n

postulate
x : ℕ
H : x > 0

goal : (x ≡ 2 * 1) → f x H ≡ 1
goal eq = ?

同じ流れならここでeqを展開(rewrite相当)、Coqではエラーの出る展開である。
だが、エラーメッセージがなんか違うぞ・・・

Cannot decide whether there should be a case for the constructor
refl, since the unification gets stuck on unifying the inferred
indices [x] with the expected indices [2 * 1]
when checking that the expression ? has type f x H ≡ 1

(●△●)??
Hが問題とかそれ以前の問題のようだ。
え、なに?xと2*1をunifyしようとして詰まった・・・??
何を言ってるのだろう。

というヒントを元に作った正解はこちら。

goal' : (x : ℕ) → (x ≡ 2 * 1) → (H : x > 0) → f x H ≡ 1
goal' .2 refl H = h 1 H

goal : (x ≡ 2 * 1) → f x H ≡ 1
goal eq = goal' x eq H

最初のgoal'の記述は

goal' x eq H = ?

からeqを展開して作成した。
これを見ると何となく見えてくるのは、
どうもAgdaは引数が実際になんだったかしかreflで書き換えないらしい
ということである。
つまり、Coqの場合同様にHが依存していることももちろん問題だったのだが、それ以前に
xが適当に置かれた変数であるせいで、展開できない
ということの方がよっぽど問題だったという。

やっぱりAgdaのエラーメッセージはわかりにくい・・・

ちなみにCoqでは上のやり方に相当するパターンマッチではなくeq_indなどで書き換えているので注意。
posted by chiguri at 21:39| Comment(0) | Agda

2013年11月05日

Windows用Agdaのインストーラで詰まったこと

講義で一斉にインストールを試したのだが、一応注意とメモとして。
10人ちょっとだが、ネットワークが死ぬのが怖いので、極力インストーラがネットワークを見に行かないようにインストーラを改変(注:この決断が正しかったことを後に知る)。
起こったエラーは次の二つ。

1)インストール時、関連するパスに日本語があるとエラーを起こす。
2)F-SecureのDeepGuardがcabalでインストールしたcpphsやなんだったか忘れたがHaskell用のmakeっぽいプログラムをトロイの木馬として認識する。

1は一応Known issueだったらしいことを後に知った。
なお、インストールパスのみならず、tempフォルダが配置されるユーザ名が日本語でもアウト。
(cabalでのAgdaインストール時に文句を言う)
もちろん後でユーザ名を変えてもユーザディレクトリ(C:\Users\ほげ の「ほげ」の部分)が日本語である限りアウトなのを付記しておく。
こんなの講義中にやられたら死ぬわ。
(ちなみに講義では新しくアカウントを作らせた)

2は困った。
幸い、cpphsの方は尋ねるだけなので、その時点で許可を出しつつF-Secureの設定から一時的にDeepGuardを停止することで回避。
Agda自体にはこれらの実行ファイルは必要ないので、後に引っかかっても特に問題なし。

こんなの一度も出たことないんだけどなあ・・・
もう21世紀も13年目なのに、また日本語ユーザ名に苦しむとか勘弁してほしい。
というかこの学科そんなアカウント作らせるの勘弁して。
いやまじめに。


ちなみにネットワークについて。
割り当ての教室に学内ネットワークが届かないという抱腹絶倒な環境だった。
cabalだけじゃなかったらどんなネットワーク環境作っても死にましたって。
(基本的にネットワークを見に行かないのだが、cabal updateだけは避けられなかったため、インストール時にネットワーク必須)
posted by chiguri at 18:39| Comment(0) | Agda