cathand
「勝たす異論」じゃねーよ。型推論とかいうとつっこまれそうだから、型解析にする。問題はパイプ結合だけ。 型ユニフィケーションをして、SIL命題のセットを出力する SIL命題セットを整理、計算（簡約）する。 SIL命題セットから代入を取り出して、再帰的に…
式Eの計算が、すべての部分式の計算も含めて安全に行われる（と予測できる）とき、《E》 と書く。式Eのすべての部分式とパイプ記号には、番号（一意的ならなんでもいい）が振ってあるとする。異なる番号が同じ場所を指す可能性がある。（[追記]そんなにイッ…
これは、あくまで構文的であり、決して意味的ではないことに注意。意味的な議論は解釈を決めないとできないし、解釈は色々あり、解釈ごとに定義は変わる。基底：コマンド呼び出しと定数 Dom(f::S -> T) = S Dom(c) = null Cod(f::S -> T) = T Cod(c) = sing(…
「文字列（名前）の集合と非負整数値」の組をシグニチャと呼ぶ。次の形で書く； {"foo", "bar"; 2}, {; 3}, {"baz"; 0}, {;0}。シグニチャパターンはオプションシグニチャパターンと引数シグニチャパターンの組である。オプションシグニチャパターンは： 文…
モノ（値）かコト（事態、動作）か モノとコトの相互変換 soft-nothing と hard-nothing ⊥の追加、厳密射、リフト 結局は、バンドルと層を使うことになるな。 集合圏の始対象／終対象の非対称性 関数と関数型（べき、指数） 特異値と非特異台 外延的記法によ…
http://d.hatena.ne.jp/m-hiyama/20061115/1163573135
戻り値Bでエラー（丸括弧で囲む）がEの関数は、A→B+(E)。Eをcatchすると、A→B+E。となると、もともと A→B+E である例外しない関数を A→B+(E) とするのが、場合分けthrowってことになる。when { y∈B => return y, y∈E => throw y}。ある範囲内の射を全部に場…
メモ編にも書くべき事も山盛りあるんだけどなあ、、、 あー手が間に合わない。しかし、記録しないとドンドン忘却するし、、、うーむ。とりあえず、モノイド圏上に、3項または4項のhomを定義して、それで圏の集まり（indexed family of categories）みたいな…
たしか、Subject-Property-Value図とか、そんなんがあったな。 Subject 丸印 Property 名札が付いた矢印 Value 四角とか、あるいは再帰的にSPV スカラー（基本データ）は四角か楕円とか。細長い四角形で配列を表せばJSONの図示となる。[1, 2] は次の図。 +--…
本編に書くべきなんだが、面倒でなー。 {ただのHTMLファイル} ⊆ {HTMLテンプレートファイル} （一般には {静的コンテンツ} ⊆ {動的コンテンツ}） {JSONデータリテラル} ⊆ {Catyスクリプト} {HTTPリクエスト} ⊆ {Catyコマンドライン} これの左側だけを取ると…
dirname, basename, ext, trunk の定義 ノード概念、ノードの種別 パス名の接頭辞順序 ツリー領域、またはツリー形状の定義 ツリー形状の上で定義された関数としてツリー ノード属性と関数値 パスの存在確認 パスの実体の生成 パスの属性を読む パスの属性を…
when {number => "this is number", string => "this is string"} function output(x) { alert("output: " + x); }if (typeof input === 'number') { output("this is number") } else if (typeof input === 'string') { output ("this is string") }
集合の直積を考えたモノイド圏では、右自明（左自明）モノイドを作れる。集合の直和について同じことをしようと思うとうまくいかない。射を部分写像にすると、右自明積の類似を定義できる。A+A→A を左成分では未定義、右成分では恒等とすればいい。ところが…
Catyのモデルとなる圏って、分配圏をイッパイ含んだ分配圏か？ スタンピングでモナド、コモナドを作るときに使う演算と、JSONデータを細工するときの演算は明らかにレベルが違うのだけど、どっちも分配代数の構造を持つ。なんか、やっぱりマトリョーシカつう…
意味じゃなくて、もっぱら記号の話。 定数とarity 0の関数 関数と演算子 fooとfoo()の区別 関数の引数渡しのバリエーション：可変引数、省略とデフォルト値、名前付き引数 関数記号と関係記号の区別 ソートを入れるか、特に真偽値のソート 真偽値のソートが…
JSONの意味論を展開するときの外の圏＝背景圏（background category）は、次のような圏がよかろう。 対象はセットイドである。 射は部分的セットイド写像。 直和、直積は集合ベースで考える。圏論的な直和・直積にならなくてもいい。 直和と直積で分配圏、で…
u = undefined として、記号の乱用で u = {u}。ブラケット内の数値はランクが減少する量。 ●opt-right A ⊆ B+u [u!∈A] -----------[-1] A ⊆ B●opt-both A+u ⊆ B+u [u!∈A, u!∈B] -----------[-2] A ⊆ B●object object {pi: Ai} ⊆ object {pi: Bi} -----------…
Catyの型推論のために、分解還元法というのを考えた。シーケント計算とタブローの中間のような感じのもの。推論は逆向きに（結論から仮定へと）行われるので、次の用語を導入する。 分解図 -- 推論図（1ステップ）の逆 還元図 -- 証明図（nステップ）の逆 シ…
A?? → A? (A?|B) → (A|B)? など A? & B → A & B など A? & B? → (A & B)? bag [A?] → bag [A] (ハテナ定理には不要) @name A? → @name A (ハテナ定理には不要) ハテナ定理に必要なのは、演算子?, |, & に関する正規化だけ。
制限の追加ではなくて、領域（型の意味）の構成となっている演算は7種。 配列構成 オブジェクト構成 バッグ構成 （追加） ?演算 オプショナル構成 |演算 ユニオン構成 @演算 タギング構成 （追加） &演算 インターセクション構成 （追加） 配列、オブジェク…
たいした内容ではないけど、名前を付けておこう。 タグ排他性の原理：α≠β ⇒ (@α A)∩(@β B) = 0 単調性の原理：S ⊆T ⇒ tags(S)⊆tags(T) ハテナ定理：正規形の式なら、一番外側の'?'で確定型か不確定型か判断できる。 ν（nu）定理：ν(T) ≧ 1、ν(T) = n なら、T…
タグの基本はラベル（マーカー）。型情報としての利用は付随的／二次的であり、ラベルをインスタンス型情報として流用しているに過ぎない。利用可能な範囲も限定的である。バリデータをvalidateとすると： 基本は、validate(x, T) Tは型表現 validate(x) → v…
module public provides [person]; // personは公開型名となるtype person = @person object { "name" : string, "age" : integer(minimum=0), * : any } & // インターセクション演算子 personExt // 拡張ポイント ;// 拡張ポイントの実体を外部参照にする …
partialの訳語に「偏」を使う。「部分」だとsubと区別がつかないので。集合Aとその上の二項演算 +, * の組(A, +, *)が次を満たすなら分配代数。 (a + b) + c = a + (b + c) a + b = b + a (a*b)*c = a*(b*c) a*(b + c) = a*b + a*c (a + b)*c = a*c + b*c 0…
∩の定義は、XとYの共通アンビエント領域への埋め込みを使って定義する。 そりゃそうなんだが、共通アンビエント領域を探すのが難しい。∩という絶対的な演算はどうも無理で、∩Zのような演算しか有効じゃない気がする。
Tが型表現のとき T? はオプショナル型だが、この意味がわからない。モナドはもとより関手にさえならない。値空間が表現空間の外にあるときに、T? が何をすることなのか、サッパリわからない。embedded objectsの圏EO(C, A)の中なら解釈できるのか？CとEO(C, …
背景圏としては、Posetoidを使うが、次のような組 (X, p)を考える。 Xはposetoid pはXからΩ={true, false, ⊥}への射 スライス圏を考えるわけではない。射はPosetoidと同じ。ただし、次のような演算を考えることができる。 (X, p) | (Y, q) = (X+Y, [p, q]) (…
JcentricTSのような簡単な型システムでも、型の意味はけっこう複雑で、Uをアンビエント対象＝JSON領域だとして： 台型の表現空間R、これはposetoid 台型の表現空間上で定義された3値述語p、⊥付きbooleanへのposetoid射 台型の値空間V Q(R)と同型だが同じとは…
Setoid, Posetoidもトポスにはならない。部分対象に関して： 充満である -- 埋め込みを関手とみなして充満 推移的である -- x∈D, x〜y ⇒ y∈D 完全である -- 充満かつ推移的 計算可能な述語で定義される部分対象を定義可能と呼べば、定義可能なら完全である。…
provide/require方式だから、requireがあるか・ないかで分類できる。開いたモジュール、閉じたモジュールとでも言えばいいのか。 Mが閉じたモジュール ⇔ モジュールを射とする圏で dom(M) = 1
