特に@PhillipJF、ここで試してみてください。Hask の最も正確でエレガントなモデルを作ろうとしているわけではありません。モデルを作ろうとしているだけです。批評お願いします。
A が Haskell 型の場合、Haskで型 A の値を、型 Aの適切に型指定された Haskell 項 (x :: A
型チェッカーによって受け入れられる文字列 x) の等価クラスとなるように定義します (モジュロ拡張等価性)。つまり、2 つの項が同じ (場合によっては無限の) 標準形に展開される場合、2 つの項は等しいと見なされ、hnf を持たない 2 つの項も等しいと見なされます。これが決定可能ではないという事実は無関係です。これらの条件を理論的に述べるだけでよいのです。
HaskのオブジェクトをHaskell 型 (プリミティブ型とユーザー定義型) とします。ユーザー定義可能な型はすべて存在し、個別の名前を持つと仮定します。ユーザー定義型の定義はソース コードであるため、数えることができますD0
。D1
、...そのカウントによると.)。
射A -> Bを型A -> B の値とする
A上の同一性をの同値類とid :: A -> A
し、同様に合成 とg
をf
の同値類とするg . f
。
すべての値の集合は可算集合です。項は有限のアルファベットの単なる文字列だからです。したがって、 Haskのこのモデルは小さいです。
これは間違っていますか?