Ну а всякие вариации LINQ2SQL приходится тестами дебажить.

Я вот очень много в C# балуюсь LinqKit (и в F# обожаю всякие композитные запросы), а их только тестами можно отладить нормально.

Реален ли язык, где типы - first-class objects и был бы от этого профит?

Ты про завтипы?

Не знаю)

Почитай про Idris

Представил себе флексибилити, если можно было принимать типы и возвращать типы

Посмотри, может проникнешся, там примерно про это https://youtu.be/X36ye-1x_HQ

А F* не о том же?

Посмотри, может проникнешся, там примерно про это https://youtu.be/X36ye-1x_HQ

Уже понятно, что Идрис как раз про это - есть возможность строить типы на ходу. Обычно все идеи, приходящие в голову, уже кто-то воплотил)

Это да, а вот практичность сего подхода под большим вопросом (для прикладных задач). Плюс народ жалуется, что там ещё всё не стабильно (хотя 1.0 и вышел) и компилятор медленный.

А F* не о том же?

Он точно про "доказательства корректности" на уровне типов, как agda/coq/Idris, но вот есть ли там завтипы ХЗ (да и зачем это юзать если не делаешь ПО для спутников ?)

Он точно про "доказательства корректности" на уровне типов, как agda/coq/Idris, но вот есть ли там завтипы ХЗ (да и зачем это юзать если не делаешь ПО для спутников ?)

Зависимые типы в F* есть.

@mitutee @angmarr Про зависимые типы, кстати, отдельный чат есть. Можно там обсудить. https://t.me/joinchat/AAAAAD9SWO_tLd7rJ9S7Ig

> да и зачем это юзать если не делаешь ПО для спутников кое чего из зав.типов начинает хотеться довольно скоро - стоит лишь пописать достаточно на языках с "предзависимыми типами". И при этом задачи могут быть совсем не космические :)

И всё же в одну корзину Coq и Idris класть не стоит

Idris - язык с зав.типами, язык общего назначения. Coq - доказывалка теорем

На "петухе" том же не пишут программы, на нём доказывают теорему о том, что некая программа - корректна. А потом - вжух и Coq синтезирует код на одном из языков.

И процесс доказывания довольно трудоёмок, поэтому, да, оный имеет смысл далеко не всегда - для особо ответственных кусков, разве что. Но вполне применим и на "небольших" задачах типа верификации кропто-алгоритмов или компиляторов.

А на Idris можно просто писать код - язык просто даёт больше инструментов, чем даёт, например, Haskell

F*, Agda и Idris - одного поля ягоды. Это "просто" "языки покруче" :)

@astynax Спасибо за экскурс.

Много нафлудил?

Много нафлудил?

Довольно познавательно, спасибо.

Создавать типы "на лету" можно и в "обычных" языках, другое дело, что выразительность будет похуже и будет много ручной работы :)

Те же АТД можно конструировать из Tuple + Either.

А как, например, сделать функцию, которая принимает целое число n и возвращает тип ( список ), в который можно положить лишь n элементов?

Представлением n в виде числа Пеано - представлением на типах, конечно же :)

Это как раз таки сравнительно простая задача (её даже я осилю :))

Пойду читать про число Пеано..

Ну числа Пеано, это Zero + Succ

Zero = 0 Succ Zero = 1 Succ (Succ Zero) = 2

"Пеано на типах", это синглтон-тип Zero и Succ<a>

Таким "числом на типах" можно уже параметризовать другие типы, например тип списка - получится "список с длиной"

Нужно писать свой тип списка?

Конечно :)

data List l a = Cons (Succ l) (List l a) | Nil Zero не совсем, но близко (тут GADT нужны, думаю)

Если список представить сразу в виде пар, то он по построению будет иметь известную длину. Но длинные списки будут выглядеть громоздко, конечно.

"Пеано на типах", это синглтон-тип Zero и Succ<a>

Я видел для F# тайп-провайдер с Пеано на типах.

https://github.com/mausch/TypeProviderPlayground/blob/0b8958cf04bf9316754771da894a1f81b42e8fb5/TypeProviderPlayground/PeanoProvider.fs Было непросто, но выкопал ссылку из архива.

Я видел "рогалик" в виде тайп-провайдера с выводом "картинки" в докстринге. Так что числами Пеано меня не напугаешь :)

Ну, рогалик-то как раз понятно как сделать.

Там большого ума не нужно!

(да, на самом деле нужно, но всё равно механизм понятный)

Так это же просто программа, вызываемая из ide в design time

Ну, не совсем.

Это программа, которая должна отдавать набор типов. С этим связана специфика и ряд внутренних ограничений. Например, то, что она не все возможные типы может генерировать.

(надо бы этим вопросом будет как-нибудь заняться и починить?)

А вот провайдер для Пеано, да к тому же такой коротенький, может быть и полезным, и одновременно хорошим пособием при изучении провайдеростроения.

Состояние кодируется в самом типизируемом выражении, а выводить можно тот же тип, что был на входе. Получается рекурсия с состоянием :)

Я видел для F# тайп-провайдер с Пеано на типах.

Пример без провайдеров, но с привлечением литералов. https://github.com/palladin/fsharp-snippets/blob/master/src/FSharpSnippets/Generic%20Numeric%20Literals%20and%20Compile%20time%20Peano%20arithmetic.fsx

Тоже интересно!

Что такое 1G? Как это вообще работает? %)

https://sergeytihon.com/2014/01/11/f-kung-fu-2-custom-numeric-literals/ — ок, нашёл в блоге у Сергея. Я вообще не знал про эту фичу.

Что такое 1G? Как это вообще работает? %)

Нужны руки. https://github.com/fsharp/fslang-suggestions/issues/445

(надо бы этим вопросом будет как-нибудь заняться и починить?)

Да, я могу уже целый список написать, что нужно починить в провайдерах. :)

Да, я могу уже целый список написать, что нужно починить в провайдерах. :)

Напиши.

Это полезно.

Это полезно.

Ок, позже соберу с ссылками.

А делал кто-нибудь cqrs с read и write базами?

Напиши.

1. Support generic provided type definitions Нет положительного решения. Текущее состояние описано в спецификации F#: Provided type and method definitions may not be generic. https://github.com/fsharp/fslang-suggestions/issues/274 2. Support provided union and record types Approved in principle. Нет ни RFC, ни прототипа. https://github.com/fsharp/fslang-suggestions/issues/154 3. Allow intrinsic type extensions for provided types Approved in principle. Есть прототип, но нужен RFC. https://github.com/fsharp/fslang-suggestions/issues/509 4. Allow type providers to generate types from types Approved in principle. Есть RFC и прототип. https://github.com/fsharp/fslang-design/blob/master/RFCs/FS-1023-type-providers-generate-types-from-types.md 5. Allow quotation expressions as type provider arguments Нет положительного решения. In UserVoice, Don Syme noted that this will "almost certainly require #212 (Allow type providers to generate types from types) to be fully implemented". https://github.com/fsharp/fslang-suggestions/issues/450

Это самое важное, на мой взгляд.

Есть еще пара интересных вещей, которые могут быть полезны для провайдеров. Improve support for staging in F# quotations https://github.com/fsharp/fslang-suggestions/issues/584 Немного раздражает руками собирать некоторые деревья выражений.

Type Provider Combinator Experiments Старый незаконченный, но интересный проект. С последними изменениями в TP SDK, наверное, нужно очень много обновлять. https://github.com/fsprojects/TPCombinators

@nevoroman Может быть тоже будет интересно. ^

@nevoroman Может быть тоже будет интересно. ^

Привет! Спасибо, я видел уже, действительно интересная штука :)

Привет! Спасибо, я видел уже, действительно интересная штука :)

Я про всю серию сообщений целиком.

Я про всю серию сообщений целиком.

А, окей!

Возможно, расскажу в докладе и постараюсь привлечь комьюнити реализовывать это все :)

Ну или после доклада

Лучше после доклада, наверное. Не думаю, что стоит подсвечивать недоделки на самом докладе. Это может оставить смешанное впечатление :)

Скрывать недоделки тоже не всегда хорошо. А озвучить можно как "а вот еще что будет реализовано". Я скорее за тайминг переживаю, фатально не хватает времени на то, чтобы рассказать про все интересное

Скрывать недоделки однозначно нельзя, но и как-то особенно выделять их тоже не стоит. А все, о чём говорится в докладе, по определению «особенно выделяется».

Allocations are not always your enemy. https://github.com/vasily-kirichenko/CoreApp33

> CoreApp33

Vladimir @fvnever Что скажете по этому бенчмарку?

Вариант с аллокациями работает быстрее, чем с пулом.

Вариант с аллокациями работает быстрее, чем с пулом.

А как этот пул работает? Есть что-нибудь почитать на примете?

ArrayPool.Shared.Rent — о, а это уже в стандартной либе чтоли?

А как этот пул работает? Есть что-нибудь почитать на примете?

Код можешь почитать :)

https://github.com/dotnet/corefx/blob/master/src/System.Buffers/src/System/Buffers/ArrayPool.cs

Ок, я нашел бенчмарки. http://adamsitnik.com/Array-Pool/

Да, действительно, для небольших массивов ArrayPool работает медленее аллокаций.

Аллокации всегда быстро работают, малину портит только GC. Не очень понятно в этом бенчмарке где GC

Т.е. у Адама Ситника понятно) У Василия не понятно.

Т.е. у Адама Ситника понятно) У Василия не понятно.

Да, выяснили.

Ну и с точки зрения сервера тут тоже неясно даже про маленькие массивы. Там нулевое поколение можеть быть до 4GB и когда его чистишь у юзеров таймауты.

Как обычно, надо бенчмаркать.

В каждом конкретном случае.

было бы интересно на max-min и моду посмотреть, по идее с аллокациями должен быть гораздо сильней разброс на вызовы которые попадают на GC

если так и есть, то это выбор между лучшей стабильностью и суммарной лучшей производительностью

я вот например когда тестил wcf vs asp.net core это как раз и видел, wcf работает в 2 раза быстрей в целом, но запросы которые приходятся на GC в 2 раза медленней в итоге обрабатываются

Кто-нибудь, кроме меня, работал с Freya? У меня чёт не получается сделать редирект. Написал такое: freyaMachine { movedPermanently true handleMovedPermanently (freya { do! Freya.Lens.setPartial Response.Headers.Location_ (Location(UriReference.parse "/")) return Representation.empty }) } Но этот мой хендлер в handleMovedPermanently почему-то вообще не вызывается. Я долго смотрел на диаграммы состояний в документации https://docs.freya.io/en/latest/_static/specifications.responses.html, но по ним так и не понял, почему у меня не работает :(

Ага, в гиттере подсказали: для того, чтобы работали редиректы, нужно добавить к определению машины exists false.

Привет.

https://twitter.com/oss_fsharp/status/927529742215077888