AA
Go
го пока не особо успешен
что реально выехало на гугловом каргокульте - это ПИТОН
что реально выехало на гугловом каргокульте - это ПИТОН
го пока не особо успешен
что реально выехало на гугловом каргокульте - это ПИТОН
Size: a a a
2020 May 24
A
Ну на нем пишут
A
Докеры там всякие
AG
пардон, агдина терминология. Там они лежат в разных из-за отсутствия кумулятивности. То есть в идрисе они норм даже в самый обычный список влезут?
угу
foo : HVect [Type, Type]
foo = [Nat, Type]
bar : List Type
bar = [Nat, Type]
AA
Ну на нем пишут
много на чем пишут, но с топовыми языками типа жаваскрипт, питон, жава не сравнить
AA
для гугла явно результат несоответствующий - где-то через какие-то дыры пар утекает, машина недорабатывает
R
угу
foo : HVect [Type, Type]
foo = [Nat, Type]
bar : List Type
bar = [Nat, Type]
угу, спасибо. Начинаю думать, что я либо что-то неправильно понял когда-то, либо неправильно помню
R
угу, спасибо. Начинаю думать, что я либо что-то неправильно понял когда-то, либо неправильно помню
(это я конкретно про вселенные. На тот момент когда я пробовал идрис, у него не работал инференс для туплов, для constructor-headed functions, и он слишком рано сдавался из-за неразрешенных метапеременных, которые агда успешно решала)
AG
(это я конкретно про вселенные. На тот момент когда я пробовал идрис, у него не работал инференс для туплов, для constructor-headed functions, и он слишком рано сдавался из-за неразрешенных метапеременных, которые агда успешно решала)
инференс туповат да, но щас во втором брэди специально сделал TTImp слой, думаю там будет где развернуться
R
инференс туповат да, но щас во втором брэди специально сделал TTImp слой, думаю там будет где развернуться
да, я слышал, что они вроде как добавили метапеременные в какую-то часть теории, а не просто пытаются резолвить их в surface language
R
так что про идрис 2 я ничего сказать не могу
к
угу
foo : HVect [Type, Type]
foo = [Nat, Type]
bar : List Type
bar = [Nat, Type]
но сдалать
bar : List Type
bar = [Nat]
foo : List Type
foo = Type :: bar
нельзя же, верно?
bar : List Type
bar = [Nat]
foo : List Type
foo = Type :: bar
нельзя же, верно?
AG
почему нельзя
к
ну bar должен вывестись как List Type0
к
а foo уже List Type1
АГ
@A64m_qb0 А сколько среди программистов хороших? И кто они? И на каких языках пишут?
АГ
В топе языков JavaScript, Python, go - что это? Деградация?
DF
У меня в городе есть один хороший программист
DF
Посчастливилось с ним пересечься в работе на американский стартап
DF
Статистика по Казани)