В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

Теория категорий

559 membersпожаловаться на группу
2019 September 23

NI

Nick Ivanych in Теория категорий
Ну то есть, тут неявно скрывается, что мы одинаковым образом конструируем стрелку.
Хотя и понятно, что это не одна и так же стрелка получается для разных a.
источник
22:27пожаловаться#1

AZ

Alex Zhukovsky in Теория категорий
Мне это неочевидно. По ссылке говорят как раз ту вещь, которая мне кажется интуитивно верной:

For example, a function of type

f :: ∀a. a -> a
can only be the identity function: since it must return something of type a, for any type a, the only thing it can do is return the argument of type a that it was given
источник
22:29пожаловаться#2

NI

Nick Ivanych in Теория категорий
Она верная. Только для каждого a, это будет своя id-стрелка.
источник
22:31пожаловаться#3

NI

Nick Ivanych in Теория категорий
Выражение ∀a. a -> a задаёт не одну функцию, а семейство их.
источник
22:31пожаловаться#4

AZ

Alex Zhukovsky in Теория категорий
Nick Ivanych
Она верная. Только для каждого a, это будет своя id-стрелка.
значит я неверно сформулировал. Я имел ввиду именно то, что f такого вида сущесвтует в единственном виде для разных а
источник
22:32пожаловаться#5

AZ

Alex Zhukovsky in Теория категорий
f :: ∀a. a -> a
g :: ∀a. a -> a

как простым образом доказать, что эти функции совпадают и являются id для своих типов?
источник
22:33пожаловаться#6

H

Hmm in Теория категорий
Что нужно знать при изучение теор ката? достаточно ли мат анализа  и лин ала?
источник
22:33пожаловаться#7

AG

Alex Gryzlov in Теория категорий
Alex Zhukovsky
f :: ∀a. a -> a
g :: ∀a. a -> a

как простым образом доказать, что эти функции совпадают и являются id для своих типов?
ну по хорошему нужна теория типов с отрефлексированной параметричностью
источник
22:34пожаловаться#8

NI

Nick Ivanych in Теория категорий
Hmm
Что нужно знать при изучение теор ката? достаточно ли мат анализа  и лин ала?
В принципе, можно не знать ни того, ни другого.
Но чем больше областей знаешь, тем бОльшая часть примеров будет понята.
В принципе, не так уж мало можно изучить, знаючи только за функциональное программирование.
источник
22:34пожаловаться#9

AG

Alex Gryzlov in Теория категорий
Бернарди кажется таким занимался
источник
22:35пожаловаться#10

NI

Nick Ivanych in Теория категорий
Alex Zhukovsky
f :: ∀a. a -> a
g :: ∀a. a -> a

как простым образом доказать, что эти функции совпадают и являются id для своих типов?
Вадлер это как-то относительно несложно показывал.
А если правильно категорно, то надо категорную модель SystemF строить.
источник
22:35пожаловаться#11

AG

Alex Gryzlov in Теория категорий
проще всего конечно показать что у этого типа один житель
источник
22:36пожаловаться#12

NI

Nick Ivanych in Теория категорий
Alex Gryzlov
проще всего конечно показать что у этого типа один житель
для каждого a
источник
22:36пожаловаться#13

NI

Nick Ivanych in Теория категорий
Тут вот, как раз, и загвоздка.
Что в хаскеле я пишу id x = x
Это какбе одна функция, но на самом-то деле, это куча таких id для разных типов.
источник
22:37пожаловаться#14

NI

Nick Ivanych in Теория категорий
Alex Gryzlov
проще всего конечно показать что у этого типа один житель
На самом деле, правильно сказано относительно теории типов.
Я просто с категорными вещами увязать пытаюсь, но так просто это сделать не выйдет.
источник
22:38пожаловаться#15

AZ

Alex Zhukovsky in Теория категорий
я видимо потому изначально криво сформулировал, потому что в голове генерики автоматически, и я думаю об этом как об одной функции. Но вопрос про семейство, да.
источник
22:38пожаловаться#16

NI

Nick Ivanych in Теория категорий
В общем, без категорной модели индексирования по типам ничего не получится близкого.
источник
22:39пожаловаться#17

AT

Anton Trunov in Теория категорий
Alex Gryzlov
Бернарди кажется таким занимался
Это же его color type theory?
источник
22:40пожаловаться#18

NI

Nick Ivanych in Теория категорий
Alex Zhukovsky
я видимо потому изначально криво сформулировал, потому что в голове генерики автоматически, и я думаю об этом как об одной функции. Но вопрос про семейство, да.
Внутри соответствующих теорий типов, это ж таки один терм.
Но задающий сразу семейство функций.
Можно ещё сказать, что у него неявным параметром тип, как оно во всех типазависимых языках делается.
источник
22:41пожаловаться#19

АТ

Алексей Троицкий in Теория категорий
Alex Zhukovsky
f :: ∀a. a -> a
g :: ∀a. a -> a

как простым образом доказать, что эти функции совпадают и являются id для своих типов?
на OPLSS 2014 Derek Dreyer это показывал на второй лекции
https://www.cs.uoregon.edu/research/summerschool/summer14/curriculum.html
источник
22:42пожаловаться#20