O
какие ещё есть морфизмы такого типа?
Size: a a a
2020 February 12
Oℕ
Если мы берём категорию, где только тотальные функции( что обычно не нравится создателю группы) это определение вообще некорректно
O
> Если мы берём категорию
уже не Hask
уже не Hask
IK
Хаск не категория из-за существования нетотальных функций?
IK
Или почему хаск не категория?
Oℕ
какие ещё есть морфизмы такого типа?
v a = traceShow a undefined
O
с таким же успехом
absurd' a = traceShow a a
spin (Void b) = spin b
absurd' a = traceShow a a
seq spin a wherespin (Void b) = spin b
Oℕ
ну видишь, если позволять писать всё, что заблагорассудится, не терминальный
Oℕ
а если только чистые тотальные - терминальный
O
> если позволять писать всё, что заблагорассудится
это именно то, что делает компилятор
это именно то, что делает компилятор
Oℕ
как раз тайпчеккер - часть компилятора, имеет ровно противоположную задачу
Oℕ
в любом случае, категории частичных функций тоже можно построить, ещё тут регулярно про домены скотта упоминают. Ничего про них не знаю, но кажется, они относятся к теме построения категории для тюринг полных ЯП.
Но в простом случае конечно предполагается, что мы ограничиваем хаскель до тотального сабсета
Но в простом случае конечно предполагается, что мы ограничиваем хаскель до тотального сабсета
O
он ничего не может противопоставить залифченым типам и незавершающимся вычислениям
Oℕ
он ничего не может противопоставить залифченым типам и незавершающимся вычислениям
Это офтоп, я не буду продолжать отвечать на это
Oℕ
в любом случае, категории частичных функций тоже можно построить, ещё тут регулярно про домены скотта упоминают. Ничего про них не знаю, но кажется, они относятся к теме построения категории для тюринг полных ЯП.
Но в простом случае конечно предполагается, что мы ограничиваем хаскель до тотального сабсета
Но в простом случае конечно предполагается, что мы ограничиваем хаскель до тотального сабсета
А то и до system F
O
как с категориями обстоят дела у Идриса?
Oℕ
Поясните вопрос
O
существует ли категория Idr, похожая на Hask здорового человека?
O
категория типов, где морфизмы - функции