Исходное сообщение
"Опубликован стандарт параллельного программирования OpenMP 5..." Отправлено Siborgium, 15-Ноя-20 05:14
>[оверквотинг удален] > дотягивают) на то, что в остальном мире лет 30 известно как > "refinement type". И для проверки которых не помешает не самый плохой > SMT вычислитель, тот же z3 для F* или alt-ergo для Frama-C > запросто тянут на пару сотен мб. Концепты это не refinement types, хотя и позволяют реализовать их. Концепты являются более мощным инструментом, так как, в отличие от refinement types, которые (в Idris и Liquid Haskell, во всяком случае) способны оперировать лишь валидными с точки зрения языка конструкциями, концепты еще и отвечают на вопрос "скомпилируется ли это выражение". >> Только Idris подбирается близко, но и он тащит метаинформацию в рантайм. > Вообще-то, в Idris, емнип, зависимые типы (dependent type). Они способны отобразить в > _типе_ такие вещи как: > Vect n -> Vect m -> Vect (n + m) > "длина результата объединения двух векторов равна сумме длин объединяемых" -- и правда, > куда там до концептов 🙄 ... Молодой человек, dependent types в плюсах существуют с появления темплейтов. Ваш пример выражается не так красиво, но с сохранением всех свойств: ``` template <size_t N> struct Vect {     template <size_t M>     Vect<N + M> operator+ (Vect<M>) { ... } } ```

Ваше сообщение
Имя*:
EMail:	Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email). Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:	>>[оверквотинг удален] >> дотягивают) на то, что в остальном мире лет 30 известно как >> "refinement type". И для проверки которых не помешает не самый плохой >> SMT вычислитель, тот же z3 для F* или alt-ergo для Frama-C >> запросто тянут на пару сотен мб. > Концепты это не refinement types, хотя и позволяют реализовать их. Концепты являются > более мощным инструментом, так как, в отличие от refinement types, которые > (в Idris и Liquid Haskell, во всяком случае) способны оперировать лишь > валидными с точки зрения языка конструкциями, концепты еще и отвечают на > вопрос "скомпилируется ли это выражение". >>> Только Idris подбирается близко, но и он тащит метаинформацию в рантайм. >> Вообще-то, в Idris, емнип, зависимые типы (dependent type). Они способны отобразить в >> _типе_ такие вещи как: >> Vect n -> Vect m -> Vect (n + m) >> "длина результата объединения двух векторов равна сумме длин объединяемых" -- и правда, >> куда там до концептов 🙄 ... > Молодой человек, dependent types в плюсах существуют с появления темплейтов. Ваш пример > выражается не так красиво, но с сохранением всех свойств: > ``` > template <size_t N> > struct Vect { > template <size_t M> > Vect<N + M> operator+ (Vect<M>) { ... } > } > ```
	Введите код, изображенный на картинке: