λ
там энергичное всё
Size: a a a
2020 May 23
DF
А модульность требует лени?
λ
да
DF
Ого
AA
модульность в смысле хьюзность а не макквинность
Oℕ
ну хорошо, вот написал ты
\g f x -> g x (f x) в зависимом языке, и какой тип должен выводиться у этого? {A : Type} -> {F : A -> Type} -> {G: (a :A) -> F a -> Type} ->
( f: (a :A) -> F a ) ->
( (a : A) -> (fa : F a) -> G a fa) ->
a -> G a ( f a)Oℕ
Dollar Føølish
А чо там с модульностью в завтипах?
то же, что и в незавтипах
Oℕ
да
смешно
λ
не очень
Oℕ
почему модульность требует лени?
λ
потому что иначе в модулях нет смысла, если ты будешь руками рекурсию со всей сантехникой через раз описывать
AA
почему модульность требует лени?
я ж говорю, хьюзность требует
AA
по причинам описанным в пейпере "почему фп имеет значение"
Oℕ
потому что иначе в модулях нет смысла, если ты будешь руками рекурсию со всей сантехникой через раз описывать
в идрисе описываешь с сантехникой рекурсию?
AA
(в английской версии названия игры слов нету)
λ
в идрисе описываешь с сантехникой рекурсию?
нет, просто получаешь в 10^5 раз более медленную программу
к
чет я совсем не понимаю про что речь
Oℕ
это похоже на не оч удачную нейросетку, обученную на клапауции, жаль СТЛМ контекст не хранит между репликами
Oℕ
первая про модули, вторая про рекурсию, третья про производительность рантайма
к
в строгом фп языке модули не нужны?