问Hask在本地是小的吗？

EN

什么是Hask？如果它包含所有haskell可定义的“函数”作为态射，那么肯定不是

data Big = Big (Big -> Big)

Big -> Big的"hom set“包含了整个非类型化的lambda演算！我怀疑它是局部小的，即使你只允许终止函数--我认为system-f没有固定的理论模型。

编辑:七年后，我无法理解我在这里想要说的话。Hask没有集合理论模型，因为模型将函数类型解释为完整的函数集。这是真的，但我不知道这和这个问题有什么关系。不太清楚"Hask“是什么，但在我看来，任何合理的答案都会有小的homsets (也就是说，它是局部小的)。

我多年前回答的奇怪之处让我有点尴尬。我确信我的意思是非常有洞察力的--我只是不知道那是什么，而且从字面上看，它似乎是相当错误的。

Hask对象是Haskell类型，其数量是无限的。Hask箭头是Haskell函数，也是无限的。因此Hask不仅局部小，Hask也小。

card(ob(Hask))=card(hom(Hask))=card(N)

有关Hask的更多详细信息，请单击此处：

http://yannesposito.com/Scratch/en/blog/Category-Theory-Presentation/

尤其是@PhillipJF，这是一个尝试。我并不是想做Hask最精确或最优雅的模型，我只是想做一个模型。请给我评论。

如果A是Haskell类型，则在Hask中将类型A的值定义为类型A的良好类型Haskell术语的等价类(类型检查器将接受x :: A的字符串x)，模扩展相等。也就是说，如果两个项扩展到相同的(可能是无限的)范式，那么它们被认为是相等的，并且两个没有hnf的项也是相等的。事实上，这是不可决定的，这是无关紧要的，我们只需要说明这些条件集-理论上，我几乎怀疑我们可以做到。

假设Haskell Hask的对象是Haskell类型(原始类型和用户定义的类型；我们将假设所有用户定义的类型都存在并具有不同的名称。用户定义的类型定义是源代码，因此它们是可计数的。把它们命名为D0，D1，..。根据该计数。)。

设态射A_ -> _B为A_型-> _B的值

设A上的恒等式是id :: A -> A的等价类，同样地，设g和f的合成是g . f的等价类。

所有值的集合是一个可数集合，因为术语只是有限字母表上的字符串。所以这个Hask的模型很小。

这是错的吗？