#nがシンボルとして宣言されていないという話ですがそんなに違和感ありますか？
#型シグネチャに登場するシンボルは全て宣言が必要？（Setを除いて）
#data Vec (A : Set) : (n : Nat) where
[] : Vec A zero
_::_ : A -> Vec A n -> Vec A (suc n)
#でnが何かわかってもよさそうな気がするというだけで
#仮にこれをagdaが飲んでしまうとしたら別の問題が（何か曖昧になるケースがあるとか表現できないタイプの型があるとか）あるのかな？と
#もしかしたらdataでparameterはコンストラクタのスコープのところでAとして参照できるけどindicesは参照できないという規則に由来するだけ？
#これも規則なのか本質的にそうならざるを得ないものなのか自分では整理できてないですが。
#パラメータとインデックスの違いがどうも分からない。
#というわけでちょっと試してみました。
#まずVecの例でnをインデックスではなくパラメータにするとどうなるのか？
#data Vec2 (A : Set) (n : Nat) : Set where
[] : Vec2 A zero
_::_ : A -> Vec2 A n -> Vec2 A (suc n)
#などとnもパラメータにしてみたら
#zero != n of type Nat
when checking the constructor [] in the declaration of Vec2
#とでる。そこで
#data Vec2 (A : Set) (n : Nat) : Set where
[] : Vec2 A n -- ここ修正
_::_ : A -> Vec2 A n -> Vec2 A (suc n)
#すると、
#suc n != n of the type Nat
when checking the constructor_::_ in the declaration of Vec2
#となる。パラメータはコンストラクタで登場する時に固定なのね。
#逆にインデックスにすると動くのか
#今度は逆にAもインデックスにしてみる
#data Vec3 : (A : Set) -> (n : Nat) -> Set where
[] : {A : Set} -> Vec3 A zero
_::_ : {A : Set}{n : Nat} -> A -> Vec3 A n -> Vec3 A (suc n)#という風にすると
#The type of the constructor does not fit in the sort of the
datatype, since Set1 is not less or equal than Set
when checking the constructor [] in the declaration of Vec3
#これの意味するところが良く分かりません。sortってナニ？
#とりあえずSet1 is not less or equal than Setってあるから。。。
#data Vec3 : (A : Set) -> (n : Nat) -> Set1 where
[] : {A : Set} -> Vec3 A zero
_::_ : {A : Set}{n : Nat} -> A -> Vec3 A n -> Vec3 A (suc n)#分からないなりにこうするとコンパイル通るみたいだ
#これの意味するところが何なのか。
#A : SetということはAは命題なので、仮に述語論理だとすれば、{n : Nat}という個体を含むならVecは一階述語論理だけど、{A : Set}を含んでしまうとVec3は二階述語論理にしないといけないということか？
#なのでVec3はSet1だよ、と。
#(A : Set)がパラメータに現れる分にはVecはSetで良いのは…why?
#それがパラメータだってことなのか。
#Aga
#パラメータの部分は全てのコンストラクタで同じものでないとダメなのか
#Vec2 (A : Set) (n : Nat)なので[]も_::_も返す型はVec2 A nになってないとダメ。
#data Vec2' (A : Set) (n : Nat) where
[] : Vec2 A n
_::_ : A -> Vec2 A (suc n) -> Vec2 A n
#これの_::_は意味分からんけど型的にはVec2 A nを返してて正しいと
#Vec A zeroを構成したり Vec A (suc n)を返したりコンストラクタによって返す型が変わる部分はインデックスにしないといけないよと。
#で、インデックスで使われるSetのレベルの最大のものより上のものを返さないとダメよと。これはパラドックスを避けるため。
#あ、プライム忘れてる。。。
#論理の方から見るとパラメータとインデックスってどういう扱いになるのだろう？
#なんとなく少しだけ見えてきたけども
#ダメだ。
#data Foo : (A : Set) -> Set where
#これOK
#data Bar (A : Set) : Set where
#これもOK
#なんでSet1が要求されるのだらう
#コンストラクタか
#data Foo : (A : Set) -> Set where
foo : {A : Set} -> Foo A#ha
#はエラー
#data Foo : (A : Set) -> Set1 where
foo : {A : Set} -> Foo A#ならOK
#data Bar (A : Set) : Set where
bar : Bar A
#これOK
#data Bar (A : Set) : Set where
bar : A -> Bar A
#コンストラクタが引数としてAを取るからかとも思ったけどこれもOK
#とりあえずFoo : (A : Set) -> Setの問題ではなくfooの問題だとすると、命題は書いていいけど証明はできないという不都合があるのか。
#集合の集合が集合であったら、ラッセルのパラドックスを引き起こすのでは
#僕的には、Agdaは現在のコンテキストはすべて明示するという素直な思想がある気がするので、data宣言のインデックスに書いた変数がコンストラクタに書けないのは、まぁそうかなと思ってました
#あとeven nのような証明は、人間が与えてAgdaはそれを単に確認するのが基本であって、Agdaが勝手に計算するというのはないんじゃないかな…
#もちろん型推論からコンストラクタが唯ひとつしかありえない、という場合は、Agdaが勝手に埋めてくれるので、それは暗黙にすると便利らしい…
#でもAgdaは何かほどよく勝手に関数展開したりするのは、そういう実装なんだろうなーと勝手に思ってるけど、実際どういう基準なんだろうか…
#ラッセルのパラドックスについてはそうなんだろうと思いますが、そうするとインデックスはそういう扱いだけどパラメーターはなぜそういう扱いになら無いのか？というのが疑問です。
#で、その何故？という疑問は私がパラメータとインデックスの違いを正確に理解してないからだと思いますが、この場合、命題と証明として見たときにインデックスに現れるA : Setは命題で、これを仮に「xは自身を述語付けない述語である」とすると、全体が「「～は自身を述語付けない述語である」は自身を述語付けない述語である」となってパラドックスに落ちるのでダメってことで納得できるとして、パラメータのA : Setは何に当たるんだ？ということです。
#「～は自身を述語付けない述語である」の例はあくまでとりうる様々なSetのうちの一例でそういうのを含んでしまう可能性があるがゆえに高階の述語論理を扱うならSet nなヒエラルキーを考えないといけないというのが根拠なんだという理解で話してますが。
haskell-ja > Archives > 2013/05/16