haskell - Hask 局部小吗？

Question

haskell 对象的类别 Hask 是本地小类别的示例吗？

http://ncatlab.org/nlab/show/locally+small+category

也许不是.. hask as cpo http://www.cs.gunma-u.ac.jp/~hamana/Papers/cpo.pdf

haskellwiki，http://www.haskell.org/haskellwiki/Hask有很好的信息，表明 Haskell 不是笛卡尔封闭的。

Answer 1

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

data Big = Big (Big -> Big)

的“hom 集”Big -> Big包含整个无类型的 lambda 演算！即使您只允许终止函数，我也怀疑它在局部很小——我认为 system-f 没有固定的理论模型。

编辑：七年后，我无法对我在这里想说的话做出正面或反面。在将函数类型解释为完整函数集的模型意义上，Hask 没有集合理论模型。这是真的，但我不知道这与这个问题有什么关系。目前还不清楚“Hask”是什么，但在我看来，任何合理的答案都会有小的 homsets（也就是说，它在本地很小）。

多年前我的回答很奇怪，这让我有点尴尬。我确定我的意思是非常有见地的——我只是不知道那是什么，而且措辞似乎相当错误。

Answer 2

特别是@PhillipJF，这是一个尝试。我不是想制作最准确或最优雅的 Hask 模型，我只是想制作一个模型。批评，请。

如果 A 是 Haskell 类型，则在 Hask 中将A 类型的值定义为 A 类型的良类型 Haskell 项的等价类（x :: A类型检查器将接受的字符串 x），模外延相等。也就是说，如果两个项扩展为相同的（可能是无限的）范式，则认为它们相等，并且没有 hnf 的两个项也相等。这是不可判定的事实是无关紧要的，我们只需要在理论上陈述这些条件，我毫不怀疑我们可以做到。

让Hask的对象是 Haskell 类型（原始类型和用户定义类型；我们将假设所有用户可定义类型都存在并且具有不同的名称。用户定义类型定义是源代码，因此它们是可数的。只需命名它们D0，D1, ...根据那个计数。）。

让态射A -> B是A -> B类型的值

令A上的恒等式为 的等价类id :: A -> A，同样令 的合成 为g的f等价类g . f。

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

这是错的吗？

Answer 3

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

卡片(ob(Hask))=卡片(hom(Hask))=卡片(N)

有关 Hask 的更多详细信息：

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