type theory with variable-free syntax
(追記) 解決した: variable-free type theoryの圏論的な解釈について - Just $ A sandbox
--
文献に突然登場して?ってなったので.
調べても情報がヒットしないのでよくわからないけど, simply typed lambda calculusを変数を使わずに定義するものらしい.
で, STLCかなんかでうまく解釈できるかと思ったけど思いつかなかった.
まず, 代入が変数に関数値を代入しているのかと思ったらそうじゃないっぽい(合成の順番が逆だし).
さらに適用みたいな記号で書いてるM∙s
は何者なんだという感じ.
でも1
はde Bruijn indexに従ってcontextの一番近くの型を取り出しているし, 1[↑] = 2
ともみなせるのでなんか意味はありそう.
圏論的な解釈を考えると自然にでてくるんだろうか. 謎.
参考
Coinductiveのintro rule
Type Theory & Functional Programmingに出てきたCoinductive typeのintro ruleに少し悩んだので.
Coinductiveは最大不動点の形でかけるような型.
例えばStream(無限リスト)はP X = N × X
の時のPの最大不動点である.
テキストにはCoinductiveのintro規則と計算規則が以下のように書かれている*1.
CoinI : (d:D) -> ([y:D,z:D->T] => b:P T) -> xif{y,z} b d : Xif P xif{y,z} b d ~> b[d/y, λw. xif{y,z} b w/z]
ここでd:D
は初期値, y:D
は現在の引数 z:D->T
は現在計算している函数のようにみることができる.
HaskellにはCoListを作るunfoldr :: (b -> Maybe (a, b)) -> b -> [a]
という, リストの畳込みの丁度逆の操作を行う函数があって, 引数の順番は違うがあれと同じ感じ.
例を見よう.
fromN : N -> Xif P fromN := xif{y,z} (y, z (y+1)) fromN 0 ~> xif{y,z} (y, z (y+1)) 0 ~> (y, z (y+1))[0/y, λw. fromN w/z] ~> (0, fromN (0+1)) ~> (0, (1, fromN 2)) ... ~> <0, 1, 2, ..> mapi : (N -> N) -> Xif P -> Xif P mapi f xs := xif{y,z} (f (head y), z (tail y)) xs mapi f <x0,x1..> ~> xif{y,z} (f (head y), z (tail y)) <x0,x1..> ~> (f (head y), z (tail y))[<x0,x1..>/y, λw. mapi f w/z] ~> (f x0, mapi f <x1,x2..>) ... ~> <f x0, f x1, f x2 ..> iterate : (N -> N) -> N -> Xif P iterate f st := xif{y,z} (y, z (f y)) st iterate f st ~> (y, z (f y))[st/y, λw. iterate f w/z] ~> (st, iterate f (f st)) ... ~> <st, f st, f (f st), f (f (f st)) ..>
慣れてくれば簡単.
なおAgdaやIsabelleではcoinductiveな型に対するパターンマッチによる定義が普通に使えるので,
mapi : (N -> N) -> Colist N -> Colist N mapi f (x::xs) = f x :: mapi f xs
のようにかけるため, 上のようなことを考えなくてもいい.
参考
*1:XifがFixをひっくり返したものだということに後になって気がついてなるほどってなった