и меня такая возможность писать одинаковые вещи двумя способами немного настораживает
эти GADT и семья данных не эквивалентны
Vladislav
кана
ну семья открытая еще
Vladislav
Попробуй принять SBool a на вход, по GADT-у сможешь паттерн-матчить, по семье данных не сможешь.
Сергей
а астрономия как применяет?
а так и применяет: понаблюдали за звёздами, построили графики, стаявят эксперимент по проверке гипотезы о расстоянии до звезды, что исходя из предположения, через полгода, с учётом параллакса, она будет на таком-то месте на небосклоне. Ждут, смотрят - да, точно там. Такой эксперимент
A64m
А зачем истории обязательно быть наукой в строгом смысле понятия "наука" и всяких критериев Поппера?
постановка вопроса неправильная, тут скорее нужны какие-то дополнительные ухищрения, чтоб история оказалась не наукой с точки зрения попперистов-лакатошистов
Vladislav
Это не избыточность, а другая абстракция.
Yurij
Ну я это и имел ввиду
Yurij
постановка вопроса неправильная, тут скорее нужны какие-то дополнительные ухищрения, чтоб история оказалась не наукой с точки зрения попперистов-лакатошистов
Alexander
/me перепроверил календарь
A64m
а так и применяет: понаблюдали за звёздами, построили графики, стаявят эксперимент по проверке гипотезы о расстоянии до звезды, что исходя из предположения, через полгода, с учётом параллакса, она будет на таком-то месте на небосклоне. Ждут, смотрят - да, точно там. Такой эксперимент
ну т.е. эксперимент и наблюдение это одно и то же, о чем и речь, но вопрос чем это от истории отличается ответа так и нет
Vladislav
Какие предсказания делает история?
Сергей
Причины астрономических явлений регулярны, и могут быть объяснены теорией, математической моделью, например.
А причины исторических событий никто никогда не знает. В хрониках остаются только разрозненные факты и последствия.
A64m
Ну я это и имел ввиду
я вообще не понял что вы имели в виду. Ваш вопрос звучал как "какая выгода арбузу быть ягодой?"
Vladislav
Астрономические теории имеют предсказательную силу, исторические гипотезы имеют силу порассуждать на диване
Алексей
В астрономии есть много почти идентичных объектов. История таким похвастаться не может
Yurij
Так арбуз и не ягода:)
Denis
и меня такая возможность писать одинаковые вещи двумя способами немного настораживает
ни разу не эквивалентно
Yurij
"А причины исторических событий никто никогда не знает" — сильно!
A64m
Так арбуз и не ягода:)
ну так и история может не наука, но точно есть мнение что арбуз - ягода, и есть мнение, что история - наука
кана
Это не избыточность, а другая абстракция.
хм, а почему нельзя?
Я так понимаю, в случае с GADTs мы имплиситно (в компайлтайме) храним в значении пруф, что для STrue :: SBool a a ~ True.
В случае с датасемьями есть только один способ построить конструктор, значит по идее все значения в паттерне инстанса датасемьи тоже можно было бы спокойно использовать как пруф, так почему это не работает?
f :: SBool True -> Bool
f STrue = True
f' :: SBool' True -> Bool
f' STrue = True
-- • Couldn't match expected type ‘SBool' 'True’
-- with actual type ‘SBool t0’
A64m
A64m
Астрономические теории имеют предсказательную силу, исторические гипотезы имеют силу порассуждать на диване
т.е. с экспериментами разобрались?
Vladislav
хм, а почему нельзя?
Я так понимаю, в случае с GADTs мы имплиситно (в компайлтайме) храним в значении пруф, что для STrue :: SBool a a ~ True.
В случае с датасемьями есть только один способ построить конструктор, значит по идее все значения в паттерне инстанса датасемьи тоже можно было бы спокойно использовать как пруф, так почему это не работает?
f :: SBool True -> Bool
f STrue = True
f' :: SBool' True -> Bool
f' STrue = True
-- • Couldn't match expected type ‘SBool' 'True’
-- with actual type ‘SBool t0’
Другая семантика
в GADT у тебя в рантайме будет храниться 0 (False) или 1 (True), в зависимости от конструктора
в data family конструктор на каждый тип один, то есть 0 (False instance) и 1 (True instance)
Yurij
Я вопросом своим мел ввиду, что зачем попперисты требует от истории соответствия своим критериям?
Yurij
ну так и история может не наука, но точно есть мнение что арбуз - ягода, и есть мнение, что история - наука
Алексей
Уж очень много всего в космосе. Одних звездов сколько! Потому обобщения делать проще. Но разница чисто количественная
Vladislav
@kana_sama У тебя могут быть даже инстаны data family представлены GADT-ами
A64m
Я вопросом своим мел ввиду, что зачем попперисты требует от истории соответствия своим критериям?
так ведь не требуют. Емнип у попперист есть критерий демаркации между наукой и ненаукой, он ничего не требует, он классифицирует историю как науку, а истмат не как науку
Vladislav
data family F a b
data instance F Int a where
FII :: F Int Int
FIB :: F Int Bool
data instance F Bool a where
FBI :: F Bool Int
FBB :: F Bool Bool
Yurij
Так я ведь и не спорю, это вы другим расскажите :)
Yurij
так ведь не требуют. Емнип у попперист есть критерий демаркации между наукой и ненаукой, он ничего не требует, он классифицирует историю как науку, а истмат не как науку
кана
хм
кана
я понял разницу в семантике
Vladislav
в рантайме
FII = 0
FIB = 1
FBI = 0
FBB = 1
кана
в датасемьях каждый инстанс это вообще отдельный тип
Alexander
+
Vladislav
Да
кана
а в gadt это один тип, но индексированный
A64m
лакатошист и так далеко не идет, он указывает что у истмата слишком большой "защитный пояс", особого толка от такой науки нету уже, другие подходы более успешно с ним конкурируют
Yurij
Просто странно слышать от человека, который заявляет, что он за научный подход к истории, чисто истамтовские термины
Yurij
Это я про Евгения Омельченко
Yurij
истматовские*
Yurij
Тут прямое противоречие
Vladislav
т.е. с экспериментами разобрались?
Не совсем
Вот в астрономии если наблюдение сделали и гипотезу построили, то эксперимент — это какое-то конкретное наблюдение следующее, которое надо провести.
В истории нельзя найти документ, сделать гипотезу, а потом поставить эксперимент "найти еще документов", потому что может и не найдешь
A64m
Не совсем
Вот в астрономии если наблюдение сделали и гипотезу построили, то эксперимент — это какое-то конкретное наблюдение следующее, которое надо провести.
В истории нельзя найти документ, сделать гипотезу, а потом поставить эксперимент "найти еще документов", потому что может и не найдешь
это странный какой-то довод, можно ведь и наблюдение не сделать
Vladislav
Эксперимент это запланированные действия, для которых реальные результаты сверяются с ожидаемыми
Vladislav
В астрономии наблюдение может быть таким, в истории нет
Alexander
пятничный чятик весел
A64m
почему не может-то?
Alexander
но не в чятике
A64m
этот процесс может быть даже идентичным от начала и до конца, когда астроном поднимает спектрограммы 1905го года из архива чтоб экзопланету подтвердить
Vladislav
Это один вариант, а второй вариант (сделать новую спектрограмму) историку не доступен
A64m
астроном тоже для много чего не сможет сделать новое наблюдение, это вопрос не принципиальный а чисто технический
Yurij
История и астрономия изначально совершенно разные науки, с разными объектами исследования — вы упоролись оба их всерьез сравнивать сейчас?
Vladislav
ну ок, с машиной времени объявим историю наукой (раз это вопрос "технический")
Yurij
Естественно, там и методы будут иными
A64m
ну ок, с машиной времени объявим историю наукой (раз это вопрос "технический")
при такой логике и астрономию без машины времени наукой считать нельзя
Vladislav
Можно, потому что в астрономии есть периодичность, и если пропустить наблюдение из прошлого, можно делать эквивалентное
A64m
периодичность в астрономии есть мало где, мы можем опыты наблюдениями в астрономии заменить не из-за периодичности, а из-за того что мы наблюдаем множество похожих процессов на разных стадиях
Сергей
второй раз сегодня вспоминаю Азимова и Foundation. Психоистория Хэри Сэлдона была наукой, потому что он с её помощью мог участвовать в построении будущего, реальности
Сергей
На самом деле всё рассчитывылось
Leonid 🦇
Сергей
что тут 31 будет..
A64m
"предсказательная способность" это отдельная история, с этим во многих науках не все радужно
Alexander
в общем будет тихий и спокойный чятик
кана
в хаскель вики семейства часто проводят параллели с тайпклассами
Это полезная аналогия или просто простой способ понимания?
Alexander
неинъективно и то и другое
кана
Потому что я тупо не могу увидеть нормальной параллели между этими двумя вещами, но вроде как понимаю и то, и то, лишь немного общих свойств типа открытости
Vladislav
> Это полезная аналогия или просто простой способ понимания?
Не полезная
Kirill
в общем будет тихий и спокойный чятик
судя потому с какой скоростью тут появляются сообщения даже в будние дни - местные хаскелисты с удовольствием будут затирать про научные подходы во всех/любых областях не связанных с хаскелом даже в 00:00
Vladislav
Классы надо сравнивать с обычными data
Alexander
Alexander
но там семьи, друзья, поспать наконец
Kirill
или кто-нибудь не вбросит очередное "хаскель медленный, я на питоне сделал быстрее"
Vladislav
data Monoid a = MkMonoid
{ mempty :: a,
mappend :: a -> a -> a
}
monoidSum :: Monoid Int
monoidSum = MkMonoid 0 (+)
class Monoid a where
mempty :: a
mappend :: a -> a -> a
instance Monoid Int where
mempty = 0
mappend = (+)
Kirill
или кто-нибудь не вбросит очередное "хаскель медленный, я на питоне сделал быстрее"
и тогда хаскель чятик превратится в С/С++ чатик истинных извращений :)