p
Думаю всё-таки попробовать хаскель и туда переписать яп, пушто Раст заебал говно моча
Size: a a a
2020 June 06
G
Думаю всё-таки попробовать хаскель и туда переписать яп, пушто Раст заебал говно моча
Правильно
AZ
При чем почти любая программа в идрисе работала раньше моего понимания🤔
Хз как вас, меня это напрягает
Хз как вас, меня это напрягает
так это наоборот круто
AZ
VarArgs : Type -> (numargs : Nat) -> Type
VarArgs t Z = t
VarArgs t (S k) = (next : t) -> VarArgs t kAZ
охуенно же
AZ
варарги можно самому реализовать
AZ
а не ныть "позязя дайте в язык такую возможность"
G
+++
AZ
реализовал за 3 наносек знакомства с языком
VS
Хм - прочитал что в Германии на законодательном уровне запретили лечить Гомосексуализм. Ну вообще давно надо было такой закон принять и вообще да - мое уважение.
p
только эти варарги тебе в идрисе туеву хучу оверхеда в рантайм перенесут, держу в курсе. у меня правда есть мысли как от этого избавиться, но в идрисе уже всегда будет лишний оверхед
DF
Не могу понять чем эти варарги отличаются от джавовских :)
DF
Там тоже все в список покуется
G
Dollar Føølish
Не могу понять чем эти варарги отличаются от джавовских :)
В Idris разных типов могут быть
G
В Java это массив по-факту)
DF
А, тогда норм
G
Dollar Føølish
А, тогда норм
Я ещё поразился, когда оно в рантайме генерировалось
DF
Што генерировалось
G
Т.е. сигнатура функции в рантайме определяется, и при этом всё безопасно
DF
А, ну так завтипы