Не могу понять

В смысле, почему в Hask произведения не настоящие? А хрен его знает, если честно. Я тоже удивляюсь.

Это завело меня в тупик, и я начал пить.

Действительно, хрень какая-то получается, коллега.

Из типизированного лямбда-исчисления получается как раз CCC / LCCC. Что касается Hask - хаскель вообще противоречив under CH и в нём есть всякие non termination, undefined, error, throw и т.п. Они как раз и ломают непротиворечивую структуру категории. Например, в агде найти fixpoint для любого эндоморфизма (CCC отличается тем, что в ней не может быть сумм и fixpoint для всех эндоморфизмов) нельзя никак иначе кроме как поломкой набора аксиом или отменой termination:

postulate
  universal-duck : ∀ {A : Set} → A

all-fixpoints : ∀ {A : Set} → (endo : A → A) → ∃ λ x → endo x ≡ x
all-fixpoints = universal-duck

all-fixpoints′ : ∀ {A : Set} → (endo : A → A) → ∃ λ x → endo x ≡ x
all-fixpoints′ = all-fixpoints′

тогда как в хаскеле «универсальная утка» и non termination в порядке вещей:

data Z = Z
data S x = S x

data (:=) x :: * -> * where
  Refl :: x := x

plusOneFixpoint :: S x := x             -- forall x. x + 1 = x
plusOneFixpoint = error "plusOneFixpoint"

plusOneFixpoint' :: S x := x            -- forall x. x + 1 = x
plusOneFixpoint' = plusOneFixpoint'

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.8232

Ну, настоящих сумм в Hask тоже нет.

кто здесь?

Это конечно менее очевидно, чем то, что рецессивная аллель влияет на фенотип, только если генотип гомозиготен.

Мне вот интересно, почему для описания не таких что бы уж очень сложных вещей необходимо использовать так много непонятных слов?;-)

настоящих сумм в Hask тоже нет

__ :: t
__ = __

f, g :: () -> ()
f = __
g = \_ -> __

f1, g1, f2, g2 :: ()
f1 = f ()
g1 = g ()               -- f1 == g1 == _|_
f2 = f `seq` ()
g2 = g `seq` ()         -- f2 == _|_ /= g2 == ()

                        -- f /= g

c1, c2 :: ()
c1 = (f . id) ()        -- == g1 == _|_
c2 = (f . id) `seq` ()  -- == g2 == ()

                        -- f . id == g

^ разные функции попали в один класс эквивалентности, так что настоящих морфизмов тоже нет.

Ты сам понял, что написал? )

Не понял, кто попал в один класс эквивалентности.

можно взять произвольное произведение и попытаться показать, что проекции в общем случае построить невозможно

Хватит ботать - НГ же.

Разные функции f и g неразличимы в Hask. Хотя там должны быть неразличимы только одинаковые функции (морфизмы - классы эквивалентности функций).

Разные функции f и g неразличимы в Hask.

Э-э-э... почему это?

То есть, тут всё зависит от того, как ты определяешь морфизмы в Hask. Если просто как лямбда-термы — то f и g становятся двумя разными морфизмами и всё хорошо. Если как теоретико-множественные отображения — то g вообще не задаёт морфизма, и тоже всё хорошо.

То есть, тут всё зависит от того, как ты определяешь морфизмы в Hask.

Не знаю как нужно строить Hask (видимо, так чтобы описать как можно больший кусок хаскеля). Но обычно модель LC в виде CCC использует классы эквивалентности (modulo alpha/beta/eta reductions) термов со свободными переменными в качестве морфизмов (http://arxiv.org/abs/1102.1313 - Definition 101 & 102). Для того чтобы различать термы (и не различать редукции в рамках уже их классов) нужны более сложные модели (2-категории - http://golem.ph.utexas.edu/category/2006/08/cartesian_closed_categories_an.html, http://math.ucr.edu/home/baez/qg-winter2007/hilken_2lambda_calculus.ps).

Но обычно модель LC в виде CCC использует классы эквивалентности (modulo alpha/beta/eta reductions) термов со свободными переменными в качестве морфизмов

Ну дык Hask — в любом случае не декартово замкнута, в ней, опять-таки, даже произведений нет.

Я не знаю, насколько это общепринято, но я бы пошёл, опять-таки, от семантики Скотта, это будет проще. Просто определить морфизмы как непрерывные отображения соответствующих посетов.

Гомоморфный образ группы изоморфен ее фактор-группе по ядру гомоморфизма (Первая теорема о гомоморфизме)

Из учебника Д.К. Фадеева: > Формулировка этой теоремы является пугалом для непосвященных так как состоит практически из одних терминов.

Так и здесь )

http://www.stihi.ru/2009/01/17/2570

Ну дык Hask — в любом случае не декартово замкнута, в ней, опять-таки, даже произведений нет.

Если взять Hask как полную (почему полную - непрерывные функции вычислимы, а на хаскеле можно написать любую вычислимую функцию) подкатегорию DCPO⊥, то она будет иметь произведения, то есть денотационно и семантически всяким типам-dcpo будет соответствовать тип-кортеж-dcpo со смыслом произведения в категории. Другое дело, что эти типы-произведения будут недостижимы операционно и синтаксически, то есть на уровне самого языка Haskell. Например, если тип A это dcpo X, тип B - dcpo Y, то в модели будет нормальное произведение X × Y, тогда как в языке (A, B) это на самом деле не X × Y, а (X × Y)⊥, то есть помимо (⊥, ⊥) и т.п. содержит и просто ⊥.

Ещё особенность в том, что есть две стратегии вычисления, так что должны быть две модели (DCPO⊥ и DCPO⊥!, например), при этом смешиваемые (?). То есть примерно так:

Cat       MCC       CCC       sums      fixpoints complete  cocomplete  Hask?

DCPO      ✓         ✓         ✗         ✓         ✓         ✓

DCPO⊥     ✓         ✓         ✗         ✓         ✗         ✗           Lazy (non-strict) Hask (full subcategory)

DCPO⊥!    ✓         ✗         ✓         ✓         ✓         ✓           Strict Hask (full subcategory)

Другая особенность в том, что в хаскеле помимо ⊥-зависаний (безинформационных) есть ещё ⊥-исключения (хоть какая-то информация в них есть) - их нужно отдельно упорядочивать.

Просто определить морфизмы как непрерывные отображения соответствующих посетов.

Ну то есть это будет модель в смысле теории доменов, а не категорных логик. Ndulu, как я понял, спрашивал про то какое отношение имеет то о чём говорят Баез & Co к Hask, а Баез & Co говорят в основном про модели в смысле категорных логик, так что никакого отношения - у логически противоречивого языка не может быть модели в логическом смысле (теорема о полноте). При этом просто модель теории языка в которой непротиворечивость понимается как существование неравных вещей может существовать. То есть также как в истории с нетипизированным лямбда-исчислением - как логика оно противоречиво, но существуют теории (как наборы равенств над термами) которые непротиворечивы (не все термы равны) и имеют модели (в виде рефлексивных доменов).

Не знаю как связаны модели категорных логик и теории доменов, но с декартовой замкнутостью, суммами и универсальными неподвижными точками ситуация «выберите любые два из трёх»:

CCC       sums      fixpoints Cat                           consistency (possibility)

✓         ✓         ✓         ≅ degenerative category (1)   universally inconsistent

✓         ✓         ✗         biCCC                         logically consistent (e.g. BHK)

✓         ✗         ✓         e.g. DCPO, DCPO⊥            | logically inconsistent (e.g. UTLC)
                                                          | consistent in the sense of equational theory (e.g. UTLC, again)
✗         ✓         ✓         e.g. DCPO⊥!                 |

✓         ✗         ✗         CCC                           logically consistent (e.g. STLC)

Можно забыть о CH и строить чисто денотационную модель, либо ограничивать (как в «Fast and Loose Reasoning is Morally Correct») хаскель до тотального подмножества, для которого уже можно строить модель в смысле категорных логик с оглядкой на «типы = логические утверждения, программы = их доказательства».

Другое дело, что эти типы-произведения будут недостижимы операционно и синтаксически, то есть на уровне самого языка Haskell.

То есть, их не будет в Hask.

Кстати, насчёт «непрерывные функции вычислимы» — это ты тоже загнул, на самом деле: возьми любую функцию Integer->Integer, загоняющую (_|_) в себя; она непрерывна.

есть две стратегии вычисления, так что должны быть две модели

Э... зачем? seq — функция непрерывная, так что всё в DCPO укладывается.

с декартовой замкнутостью, суммами и универсальными неподвижными точками ситуация «выберите любые два из трёх»

«Выберите не более чем два из трёх».

Я бы, кстати, отказался от неподвижных точек. Пусть жопы будут не везде, а только у некоторых типов. А добавление жопы — вообще монада.

То есть, их не будет в Hask.

Ну да, если хочется чтобы в Hask были только достижимые синтаксически вещи, то это будет неполная подкатегория DCPO⊥ в которой настоящим произведениям и т.п. из (полной подкатегории) DCPO⊥ будут соответствовать их «эффективные расширения» которые на уровне языка ведут себя несколько иначе (поэтому получается curry . uncurry /= id и т.п. несоответствия).

«непрерывные функции вычислимы»

Ага, то есть наоборот - вычислимые функции монотонны, монотонные функции не всегда вычислимы, вычислимые функции непрерывны, непрерывные функции не всегда (но уже лучшая аппроксимация) вычислимы.

Но тогда вопрос - почему всякий хаскельный тип - (d)cpo, а всякая функция - непрерывна?

так что всё в DCPO укладывается

Только DCPO⊥ - от того, что всякий тип в хаскеле населён никак не избавиться. Если же нужно рассуждать исключительно про строгую семантику, тогда нужно брать моноидально, не декартово, замкнутую DCPO⊥!.

Я бы, кстати, отказался от неподвижных точек

Тогда должно получиться примерно то что сейчас в агде - логически чистое ядро из тотальных функций и функториально строго позитивных данных, возможность отключить его чистоту (отключением соответствующих проверок на уровне флагов компиляции), FFI (постулаты), смешиваемая с индукцией коиндукция и IO monad, partiality monad (как раз «добавление жопы») и т.п. на их основе.