Comments 55
слишком сложно для пятничной статьи
Трудно не согласиться.
У вас в последнем варианте размер массива так или иначе известен статически, верно?
Совершенно верно, для GenericArray это часть типа. А в чём "читерство"?
Кстати, спасибо, тоже интересная задача: можно ли сгенерировать GenericArray с неизвестной заранее длиной, и если да, то как его можно будет использовать: вернуть из функции, например, заведомо нельзя — точнее, можно, но только в виде trait object, — а вот передать глубже по дереву вызовов, может быть, и получится.
Собственно, это ключевая фича зависимых типов — можно ли выражать терм-левел зависимости в типах, которые могут быть вычислены лишь во время выполнения, или нет.
А вас не затрудник немножко разжевать это для несведующих?
Как это происходит?
Огого! Спасибо большое за подробный ответ!
Не уверен, что все понял, к сожалению, очень уж синтаксис непривычный.
У меня есть ощущение, что что-то частично подобное можно сделать на шаблонах С++, скажем, у std::array размер — шаблонный параметр, довольно легко написать функцию, которая складывает только массивы одной длины.
Но вот кусок, который родит нужный класс в рантайме в зависимости от прочитанной из файла длины — вот тут сходу не получается.
Благодаря twinklede получилось сделать похожее на плюсах и boost::hana. Но в синтаксис языка это не очень вписывается. Если кратко то нам надо на каждую переменную новый тип это будет немного костыльно:
auto x = make<source_loc()>(rand());
auto y = make<source_loc()>(rand());Теперь у икс и игрек разные типы и раные значения. Далее в hana мы можем работать с темплейтами и типами в них как с обычным структурами данных типа set, dict, etc. Например в типе переменной будет хранится ид и множество ид других переменных которым она равна. Т.е. например auto opt_z= x.equal(y) дает нам std::option в котором кроме null (при рантайм значении x!=y) могут быть две новые переменные x1, y1 в типах которых есть отметка о равенстве. После распаковки можно будет делать static_assert(is_equal(x1, y1)).
Попробовал что то подобное реализовать на расте, но без зависимых дженерик типов не получится. приходится пробрасывать все начальные параметры дженериков вручную наверх, и в самой верхней функции уже пяток а то и десяток праметров. Т.е. для серьёзных применений не годится.
В закладки и в планы на будущее, спасибо :)
data Vect: (n: Nat) -> (ty: Type) -> Type where
Nil: Vect 0 ty
(::): ty -> Vect n ty -> Vect (S n) ty
Я правильно понимать, что если мы уберем последнее -> Type то мы сможем объявить тайп конструктор с одной дыркой?
Я не уверен, что понял вопрос. Что значит «с одной дыркой»?
Это значит что конструктору нужно передать один тип чтобы получить тип. Я взял термин из скаловой тусовки, думал он общепринят.
Собственно, просто убрать последнее -> Type у вас не получится, даже если не рассматривать конструкторы, это синтаксическая ошибка:
Я просто думал можно написать метод над тайп конструктором а не обычным типом, а-ля скаловое def Foo[F[_]]
Если вы теперь напишете data Vect: (n: Nat) -> Type, то это вполне легитимная запись, но вопрос в том, что вы будете делать с конструкторами.
Применять где-то позже, логично же :)
Ну я скалу совсем не знаю, она меня своими квадратными скобками пугает.
Это нормально. Нужно пообвыкнуть и чуть-чуть смириться.
А в идрисовской (да и вообще, похоже, в формально-доказательной) тусовке дырка — отсутствующий proof term, как вон вся та ерунда со знаками вопроса в комменте выше.
Под дыркой имеется ввиду незакрепленный генерик. Например, в терминах сишарпа List<> — тайп-конструктор с одной дыркой, HashMap<,> — с двумя, и так далее.
По идее, (n: Nat) -> (ty: Type) -> Type — это тип с двумя дырками, получается. По крайней мере, до тех пор, пока мы не подставим конкретное число n и конкретный тип ty.
не совсем, тут та же разница, как между List<T> и List<>. В одном случае у нас единственный закрепленный тип T, а в другом — дырка.
Типичный пример, когда это может понадобиться:
def eitherMonad[E] = new Monad[Either[E, *]] {
override def unit[A](a: => A): Either[E, A] = Right(a)
override def flatMap[A, B](ma: Either[E, A])(f: A => Either[E, B]): Either[E, B] = ma.flatMap(f)
}Обратите внимание на *. Монада это генерик от одного параметра, а мы используем тип Either с двумя. Таким образом мы делаем монаду от типа с одной дыркой, куда нужно подставить один тип (типа результата) чтобы превратить конструктор в тип.
Синтаксис непривычный, но фишка классная, надо вам писать статью про ФП в примерах.
(тут мне стало интересно, можно ли похожее на плюсах, хехе)
с границами известными в compile-time легко, есть уже всякие библиотеки, может даже как часть буста, например https://www.boost.org/doc/libs/1_69_0/libs/safe_numerics/doc/html/tutorial/6.html.
Весь интерес в том чтобы это работало в рантайм, как Вы написали ниже.
Спасибо за наводку на typenum .
А зачем Option<Box<dyn Trait>>, нельзя просто Option` вернуть?
Число функций, имеющих такую сигнатуру, скорее всего бесконечно.
>Поэтому без теста не обойтись.
Мы пока только убедились, что такая сигнатура не позволяет нам судить о правильности работы функции. Ну то есть правильный вывод — что такой системы типов недостаточно. А уж нужны ли нам тесты (или там формальное доказательство) — это отдельная тема все-таки.
Достаточно рассмотреть все функции вида (n : Nat) -> Fin n (т. е. которые опираются просто на длину вектора), а их уже, похоже, бесконечное число (правда, ещё интересный вопрос в том, сколько из них вычислимы, но то такое).Да, собственно, и вычислимых уже счётное число, по идее: f m n = floor (n / m) для любых целых m >= 2. Любые две такие функции будут различаться как минимум в точке n = max(m1, m2), и их, очевидно, счётное множество.
Не уверен. Например, можно формально показать (но эта алгебра пока за пределами моих навыков), что функций с сигнатурой (a: Type) -> a -> a ровно одна.
Мне кажется тут можно попробовать цепануть что-то из категорий. Там же показывается, что id морфизм единственен.
Tracking issue for const generics (RFC 2000)). Теперь не нужно будет дикое шаманство с typenum и generic_array, которыми я активно пользуюсь.
Пример выше можно переписать как-то так:
fn foo<El: Eq, const Size: usize>(x: [El, {Size}, y: El) -> Option<Box<dyn UnsignedLessThan<{Size}>>>
{
// 10000 строк нечитаемого кода
}
К сожалению, писать реальный код на const generics пока невозможно из-за большого количества ICE (1, 2, 3, ..). Надеюсь скоро исправят.
полезная статья, спасибо
Python — динамически типизированный, информации минимум, какие-то подсказки дают только тесты;
Странное в оригинальной статье утверждение А что мешает использовать Gradual Typing и оставить мета информацию о типах?
Исходная статья была написана в 2016 году, тогда, по идее, это ещё не было реализовано. Сейчас — да, возможно, может быть смысл внести поправку.
Тесты или типы? — Rust version