Oℕ
Поетому не весь код, который будет компилится мономорфный останется компилируемым полиморфным
Size: a a a
2020 May 23
R
так я не говорю, что они не могут его делать. я говорю что они могут не делать и не делают
неправильно прочитал. Энивей, я не вижу, зачем его вообще делать, даже если можно было бы это имплементировать просто по щелчку пальцев
R
зато я вижу зачем нужны eta-rules в унификации, зачем нужны эвристики для constructor-headed functions и тд
AA
неправильно прочитал. Энивей, я не вижу, зачем его вообще делать, даже если можно было бы это имплементировать просто по щелчку пальцев
чтоб код писать не только от сигнатуры к реализации, но и в другую сторону удобно было
AA
при чем для многих людей, типа меня, это 90% случаев
Oℕ
ну я так и сказал, что академики просто потеряли интерес к выводу типов и не делают его потому что могут не делать
λ
ну не ноль. Он показывает, что нет каких-то технических ограничений. Просто с зависимыми типами (да и не с зависимыми, как по мне) удобнее не выводить полиморфные типы
ну если фп код не писать, то наверное удобнее
R
при чем для многих людей, типа меня, это 90% случаев
видимо тут я отличаюсь, потому что для меня это 1% случаев
AA
ну. про это я и говорю
Oℕ
если фп код не писать (где завтипные функции передаются в завтипные функции и получаются завтипные функции), то наверное глобальный инференс удобнее
R
чтоб код писать не только от сигнатуры к реализации, но и в другую сторону удобно было
ну хорошо, вот написал ты
\g f x -> g x (f x) в зависимом языке, и какой тип должен выводиться у этого?DF
С глобальным выводом?
AA
ну хорошо, вот написал ты
\g f x -> g x (f x) в зависимом языке, и какой тип должен выводиться у этого?я не собираюсь ниче писать в зависимом языке
DF
По всей программе
Oℕ
я не собираюсь ниче писать в зависимом языке
опять фп хейтишь?
DF
Кек
AA
опять фп хейтишь?
ну как и все остальное
λ
кек, а чо бы фп без вывода типов и базовой модульности не похэйтить
DF
А чо там с модульностью в завтипах?
λ
ну я конкретно об идрисе сейчас говорил