C
Size: a a a
2021 April 14
C
Кот када отказался от ифов
SK
или кто там про него вспомнил
S
димаход
AT
@skucherenko блин, про элиминаторы заговорили, вспомнил, как сегодня прикольное решение нашёл для функции уполовинивания натуральных чисел в форме Пеано через рекурсор
Через паттерн-матчинг это будет как-то так
Definition halve : nat -> nat :=
nat_rect (fun _ => nat) 0 (fun n rec => n - rec).
Через паттерн-матчинг это будет как-то так
Definition halve : nat -> nat :=
fix halve (n : nat) :=
match n with
| 0 => 0
| 1 => 0
| S (S n) => S (halve n)
end.
w
а можно рисунок фотографии скриншота?
EK
Прикиньте, Джон выкидывает ифы, заменяет это адт или черчем, твиттер ему апплодирует, конференции мутятся.
Потом прагматично возвращает if, называя это constructor rotation
Потом прагматично возвращает if, называя это constructor rotation
AT
выкидывание ифов и замена чёрчем ещё и с налогами поможет (всякие поблажки религиозным организациям)
SK
с фиксом сразу понятно, на нат_рект пришлось идти у Адама в цпдт смотретт
AT
нат_рект просто рекурсию абстрагирует
nat_rect =
fun (P : nat -> Type) (f : P 0) (f0 : forall n : nat, P n -> P (S n)) =>
fix F (n : nat) : P n :=
match n as n0 return (P n0) with
| 0 => f
| S n0 => f0 n0 (F n0)
end
AT
вот кстати у хаскеллистов было понимание слепоты в стилея де гуза
но это не оно)
булева слепота же про то, что если матчишь по типу-сумме, то в ветках матча должен какую-то доп инфу получать, а не просто ветвление
data Case = CaseInsensitive | CaseSensitive
data Predicate = Contains | Equalsно это не оно)
булева слепота же про то, что если матчишь по типу-сумме, то в ветках матча должен какую-то доп инфу получать, а не просто ветвление
AT
а у дегуза просто синонимы була, что при вызове функции не спутать аргументы
SK
просто на уровне человека расслепливание, без механизации ;)
AT
я бы сказал, что просто тёмные очки с разными оттенками чёрного
EK
Ну булеан блайнднес - это ситуация, когда есть ответ, но ты забыл, какой был вопрос. Синонимы була эту проблему частично решают же.