я не знал что impl может быть для любой функции с N аргументов

да impl может быть для любого типа

а причем тут импл?

там ничего не написано про impl для сигнатур функций. Ничего такого не помню.

а какая разница?

а какая разница?

потому что это неочевидно нифига.

чем тип функций отличается от типа числового?

а причем тут импл?

притом что он участвует в коде

потому что это неочевидно нифига.

очевидно

чем тип функций отличается от типа числового?

это нифига неочевидно

завтра будем impl для констант?

после завтра для макросов?

аааа, я понял

типа макрос с такими аргументами ловит impl

ты просто не шаришь что сейчас везде функции — обычные значения

теперь я понял твою проблему

ты просто не шаришь что сейчас везде функции — обычные значения

в книге ничего такого не описано, да.

в книге ничего такого не описано, да.

ну, вообще, написано

ну, вообще, написано

я не видел, можешь дать ссылку?

я вроде второе издание полностью прочел

в какой-нибудь главе о closures должно быть, иначе эту главу нельзя понять

а вы тут просите hkf лел

а вы тут просите hkf лел

как же хочется hkp в rust :c

хм

а можно таким образом написать трейт который определяет, predicate ли функция?

я не видел, можешь дать ссылку?

https://doc.rust-lang.org/book/first-edition/functions.html

> first-edition

> first-edition

и?

но во втором поинтеры на функции тоже были

на что надо обратить внимание?

бля

= function_name

это как воще

а, понял

на что надо обратить внимание?

да на то что это обычное значение

которое можно присваивать там

да на то что это обычное значение

так то что это значение на которое можно например поинтер получить это понятно

а на let тоже можно impl сделать?

а можно таким образом написать трейт который определяет, predicate ли функция?

походу нет, нужны negative trait bounds :(

а на let тоже можно impl сделать?

у let есть тип? let — значение? ты шо, не врубаешься реально?

impl можно навесить на любой ТИП

let stuff impl trait for stuff

а можно impl на impl сделать?

let stuff impl trait for stuff

после for должен стоят ТИП

лололо

а можно impl на impl сделать?

наследование, еретик.

let stuff impl trait for stuff

а ты ставишь значение

то у тебя функция это значение

то на значение внезапно нельзя impl

то у тебя функция это значение

сука

да я не пойму тебя

функция — значенин

а её тип — ЭТО ВНЕЗАПНО ТИП

ОХУЕТЬ, ПРАВДА?

ну я не знал что у функции есть тип, лол

да я не пойму тебя

конкретный объект и тип объекта это непересекаемые пространства

для меня Trait это тип

а стоп

структура это тип

короч я запутался.

и структура и трейт находятся в "пространстве" типов

но почему у функции вдруг есть тип?

но почему у функции вдруг есть тип?

ДА ПОТОМУ ЧТО ФУНКЦИЯ — ЗНАЧЕНИЕ

но почему у функции вдруг есть тип?

потому что функции одного типа отличаются от функций другого типа

ты сказал что на значение нельзя impl

а почему нет? есть тип вида Int => String и экземпляр этого типа какаято функция

если ты берешь поинтер на функцию, у него же должен быть какой-то тип

но почему у функции вдруг есть тип?

Так договорились

а, ну да, вспомнил. Т.к мы можем кложурку получить, то там все эти Fn, FnMut и т.д

но почему у функции вдруг есть тип?

class FunctionIntToInt; FunctionIntToInt f;

которые соответственно типы.

возможно тебе поможет почитать про изоморфизм карри-ховарда

Соответствие Карри-Говарда / Изоморфизм Карри-Ховарда - эквивалентность между математическим доказательством и программой. Тип терма является высказыванием, а сам терм - доказательством верности высказывания (конструктивное доказательство, когда для доказательства утвреждения нужно доказать существование объекта доказательства). Тип - логическое высказывание. Логическое высказывание считается верным, если его тип населен, т.е. есть хотя бы одно значение, имеющее данный тип. Например, тип Void - 0 - значений не имеет, поэтому Void эквивалентен ложному высказыванию. Импликации A ⇒ B (если A, то B ) соотвеетствует функция a → b. И действительно, если a населен и b населен, то и тип a → b населен (есть хотя бы одна такая функция), значит и утверждение верно. И наоборот - для типа a → Void нельзя привести термы, так как не существует функции, которая вернет ничего. Конъюнкции A ∧ B (и A, и B ) соответствует произведение типов a × b, она же пара (a, a) (или любой другой конструтор). Если хотя бы один из типов не населен, то и составить пару невозможно, ведь для одного из компонента пары просто нет возможных значений (да и логично, что a × 0 = 0 ). Дизъюнкции A ∨ B ( A или B ) - размеченная сумма типов a + b, например Either a b. Если хотя бы один тип населен (например a`), то всегда можно составить терм `Left x, где x : a. И только если оба типа не населены, то и сумма не населена. А теперь вещи поинтереснее - кванторы всеобщности и существования. Квантор всеобщности, ∀(x ∈ A) P(x), утверждает, что для каждого x из A верно утверждение (предикат) P(x). Например ∀(x ∈ ℕ). x² ≥ 0 - для каждого натурально числа x верно то, что x² больше либо равен нулю. Нам как бы нужно выполнить конънкцию всех утверждений P(x) для каждого x. А конъюнкция - произведение типов ⇒ нам нужно найти произведение всех зависимых от x типов P(x) для каждого значения x типа a. А это Π-тип (пи-тип). То есть каждая функия (a :: A) → P a является квантором всеобщности, ведь этот пи-тип населен только тогда, когда населены все P(a) для каждого a. Аналогично и с квантором существования ∃(x ∈ A) P(x), который утверждает, что утверждение P(x) верно хотя бы для одного x. Его изоморфизмом является Σ-тип (сигма-тип), так как именно сигма-тип является суммой всех P(x) для каждого x, на Idris тип квантора всеобщности будет выглядеть так - (x : A ** P x). Отрицанию ¬A соответствует тип a → Void, тут все понятно. Один важный момент, тип Void → Void населен ( 0^0 = 1 ), это частный случай id. Функцию вызвать конечно нельзя, но тем не менее, функция существует и возвращает элемент типа Void для каждого входного элемента типа Void (коих 0). Если вы помните, как я представлял функцию как таблицу значений, то тут у нас получится пустая таблица - (). Все эти изоморфизмы между логикой и типами позволяеют нам строить утверждения на типах и доказывать их. Именно этим я буду сейчас заниматься, потому и прикупил книжку по Idris)

вот про изоморфизм Карри-Ховарда

ну такое, не для людей далеких от компьютер сайенс и не совсем точно с другой стороны

хотя не, точно с точностью до изоморфизма))

https://play.rust-lang.org/?gist=1e50a802ac74b1511981da800dc256e0&version=nightly

интересная ошибка...

никто не знает можно ли заставить это работать?

пытаюсь собрать redox-os, посмотрим чем кончится

есть же образы