Was ist Hask? Wenn es alle Haskell definierbaren "Funktionen" als Morphismus enthält, dann definitiv nicht
%Vor% Der "hom set" von Big -> Big enthält den gesamten untypisierten Lambda-Kalkül! Ich bezweifle, dass es lokal klein ist, selbst wenn Sie nur abschließende Funktionen zulassen - ich denke, es gibt keine mengentheoretischen Modelle von System-f.
Hask-Objekte sind Haskell-Typen, die abzählbar unendlich sind. Hask-Pfeile sind Haskell-Funktionen, die auch abzählbar unendlich sind. Deshalb ist Hask nicht nur lokal klein, sondern auch klein.
Karte (ob (Hask)) = Karte (hom (Hask)) = Karte (N)
Weitere Details über Hask hier:
Besonders @PhillipJF, hier ist ein Versuch. Ich versuche nicht, das genaueste oder eleganteste Modell von Hask zu machen, ich versuche nur ein ein Modell zu machen. Kritik, bitte.
Wenn A ein Haskell-Typ ist, definieren Sie einen -Wert vom Typ A in Hask als eine Äquivalenzklasse gut typisierter Haskell-Terme vom Typ A (Strings x, für die x :: A akzeptiert würde) vom Typ Checker), modulo extensional equality. Das heißt, zwei Terme gelten als gleich, wenn sie sich auf die gleiche (möglicherweise unendliche) Normalform ausdehnen, und zwei Terme, die kein Hnf haben, sind ebenfalls gleich. Die Tatsache, dass dies nicht entscheidbar ist, ist irrelevant, wir müssen diese Bedingungen nur theoretisch festlegen, was ich kaum bezweifeln kann.
Lassen Sie die Objekte von Hask Haskell-Typen sein (primitive Typen und amp; benutzerdefinierte Typen; wir nehmen an, dass alle benutzerdefinierten Typen existieren und unterschiedliche Namen haben. Benutzerdefinierte Typdefinitionen sind Quelle Code, so dass sie zählbar sind. Benennen Sie sie einfach mit D0 , D1 , ... entsprechend dieser Zählung.).
Lassen Sie die Morphismen A - & gt; B sind Werte vom Typ A - & gt; B
Lassen Sie die Identität auf A die Äquivalenzklasse von id :: A -> A sein und lassen Sie die Zusammensetzung von g und f ebenfalls die Äquivalenzklasse von g . f sein.
Die Menge aller Werte ist eine zählbare Menge, da die Begriffe nur Strings über ein endliches Alphabet sind. Dieses Modell von Hask ist also klein.
Ist das falsch?
Tags und Links haskell