Haskに関連する値は何ですか?

カテゴリ理論とhaskellに関するncatlabのページによると、 ”
Haskellのサブセットを識別することができます.Haskellは、基本的なカテゴリ理論で使われている概念を識別するためによく使われるものです。

だから型はオブジェクトであり、関数はモプラズムです。リスト[1,2,3]やブール値「true」などの値は、どのようにしてHaskellのカテゴリ理論的定義に適合しますか?
(私は、モナドのようなリストはおそらく、ブーリアンよりも、どのようなカテゴリの理論表現でも違っていることを実感しています。どちらも実際の値がHaskの定義にどのように関係しているのか分かりません)。

ベストアンサー

nlabページで使用される精度レベルでは、値は グローバル要素 – すなわち、$ A $型の値は、$ 1 からA
$への変形に対応します。

これについて真剣に考えたければ、いくつかの技術的な問題点があります:

  1. First, actual Haskell does not actually form a category in the
    sense that we would hope — the seq operator breaks a
    lot of the program equivalences we need. However, if it were
    removed, then the pure fragment of Haskell would form a category
    (basically corresponding to the category of domains and continuous
    functions).

  2. However, global elements in “Hask” (how I hate this
    terminology!) are not precisely values, since the nonterminating
    computation is an inhabitant of every type, and so for every type
    $A$ there is a map $mathsf{loop}_A : 1 to A$ which just runs
    forever.

    If you want to distinguish between values and nonterminating
    computations, then you need a somewhat more complicated setup,
    corresponding to the models of Paul Blain Levy’s call-by-push-value.

    There, you work with two categories — one, a category of
    values, and the other, a category of computations, with an
    adjunction which gives you two functors, one embedding values into
    computations and the other embedding computations into values.

返信を残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です