Крылатый
Всё, что нужно знать.
Andrey
🦥Alex Fails
babysitter
ну сори, я слабак в этом всем. flat strings - это я выдумываю?
🦥Alex Fails
ну сори, я слабак в этом всем. flat strings - это я выдумываю?
Да я тож не знаю, могу только предположить. Ща погуглю, короч
babysitter
обычно flat говорят про ассоциативные контейнеры
babysitter
но типа мол память плоская - значит доступ быстрый
babysitter
а со строками хз
🦥Alex Fails
Дык на x86/amd64 плоская
Denis
обычно flat говорят про ассоциативные контейнеры
flat говорят про контейнеры, где память не сегментированна, резве нет?
babysitter
да, вот я про это. как это относится к строкам, щас посмотрю
Denis
Я думаю никак, потому что если строка это последовательный кусок памяти, то она и так плоский контейнер :)
Denis
А мапка вот не flat, хоть это ассоциативный контейнер
Denis
Если я конечно не путаю
babysitter
ты не путаешь, по этому в контексте мапки часто и слышно мол flat - такой особый вид мапки, которая реализуется внутри плоско
babysitter
сейчас попробую обосновать про строки
babysitter
babysitter
похоже к строкам никак не относится
Anonymous
эт.. господа.. работал кто с жерналом событий?
Anonymous
*журналом событий
🦥Alex Fails
Untitled Document.md
www.open-std.org
Flat Containers. P0038R0.
Vladislav
Почему смайл? Сейчас насоветуете...
idris - экспериментальная и глубоко теоретическая штука
Vladislav
и в продакшн она вряд ли когда-либо пойдет
Vladislav
😊
не пойми неправильно, это очень классная вещь, но нужно угорать по математике чтобы ей пользоваться
🦥Alex Fails
idris - экспериментальная и глубоко теоретическая штука
Idris (язык программирования) — Википедия
ru.wikipedia.org
Idris это чисто-функциональный язык программирования общего назначения с haskell-подобным синтаксисом и поддержкой зависимых типов. Система типов подобна системе типов языка Agda.
Борис
не пойми неправильно, это очень классная вещь, но нужно угорать по математике чтобы ей пользоваться
А haskell для нематиматика как?
Крылатый
Idris и Agda годны тем, что там есть зависимая типизация.
🦥Alex Fails
А haskell для нематиматика как?
Haskell | зеркало лурк Lurkmore
lurklurk.com
Зеркало Луркоморье. 1 История. 2 Хаскель, чаны и все-все-все. 3 Востребованность. 4 Примеры кода на Haskell.
Крылатый
В плюсах, кстати, её тоже можно запилить.
Крылатый
Но оч сложна.
Vladislav
А haskell для нематиматика как?
тоже хорошего мало, но если особо не вдаваться в детали монад/фукторов/etc. то можно
Крылатый
Да, полноценную не выйдет.
Крылатый
А хотелось бы(
🦥Alex Fails
Idris и Agda годны тем, что там есть зависимая типизация.
А что значит "зависимая"?
Крылатый
Т.е. считай делаешь под-тип для типа, навешивая предикат.
Крылатый
Например, функция деления
Vladislav
https://ru.wikipedia.org/wiki/%D0%97%D0%B0%D0%B2%D0%B8%D1%81%D0%B8%D0%BC%D1%8B%D0%B9_%D1%82%D0%B8%D0%BF
Крылатый
div a b : return a / b
Крылатый
Сюда, очевидно, нельзя вместо b сувать ноль)
Крылатый
Знач int тут будет за исключением, собсна, нуля.
Vladislav
самое клевое в них - типы эквивалентны свойствам, а программы - доказательствам
Крылатый
С, чсх, всё это делается в компил-тйаме.
Vladislav
и можно формально доказывать корректность программы прямо в коде
🦥Alex Fails
и можно формально доказывать корректность программы прямо в коде
в плюсы хотели аксиомы добавить
Крылатый
{v/
Крылатый
Хм.
Крылатый
Как?
🦥Alex Fails
axiom {
int a + b == b + a
};
🦥Alex Fails
Не помню точно, надо пропосалы копнуть
Anonymous
😁😁
🦥Alex Fails
What are “axioms”? | Axioms: Semantics Aspects of C++ Concepts
www.open-std.org
This paper claries the semantics of “axioms” in the C++ concept proposal and provides standard wording, following the C++ commit-tee vote and resolution at the Spring 2009 meeting at Summit, NJ.
Vladislav
писал когда-то бинарное дерево поиска на agda, с доказательством корректности: https://github.com/winger/agda-stuff/blob/master/Splay.agda
Крылатый
Ахринеть большая штука.
Vladislav
Ахринеть большая штука.
она еще и не дописана, на доказательтво корректности удаления меня не хватило)
Dumitru
она еще и не дописана, на доказательтво корректности удаления меня не хватило)
откуда такие знания во всем?
Vladislav
откуда такие знания во всем?
в данном случае, как ни странно, из универа - у нас был курс по фп (haskell) и спецкурс по agda
Dumitru
в данном случае, как ни странно, из универа - у нас был курс по фп (haskell) и спецкурс по agda
круто, в моем вузе сейчас одкокурсники учат парадигмы, сейчас на скале пишут
я вот как раз пропускаю
Anonymous
Учитывая, что строка известна на этапе компиляции, то почему не юзать её как параметр шаблона? Ну, шобы нативно.
оказ-ся можно писать template<std::string *str> или std::string &str;
Крылатый
И оно работает?
Anonymous
da
Anonymous
http://stackoverflow.com/questions/30604686/template-tricks-with-const-char-as-a-non-type-parameter
Anonymous
Здесь работает, у меня - нет
Vladislav
только внутрь строки не заглянуть, опять же (в compile time)
Anonymous
видимо мой компайлер не поддерживает новый стандарт
Anonymous
http://stackoverflow.com/questions/5687540/non-type-template-parameters
Anonymous
а вот
Anonymous
Vladislav