Всем привет. Хочу поделиться своим опытом использования библиотеки ProvingGround, написанной на Скале с использованием Shapeless. У библиотеки имеется документация, правда, не очень обширная. Автор библиотеки — Сиддхартха Гаджил из Indian Institute of Science. Библиотека экспериментальная. Сам Сиддхартха говорит, что это пока не библиотека, а «work in progress». Глобальная цель библиотеки — брать статью живого математика, парсить текст, переводить естественный язык с формулами в формальные доказательства, которые мог бы чекать компилятор. Понятно, что до этого еще очень далеко. Пока что в библиотеке можно работать с зависимыми типами и основами гомотопической теории типов (HoTT), (полу-) автоматически доказывать теоремы.
Читать полностью »
Рубрика «типы данных» - 2
От зависимых типов к гомотопической теории типов на Scala + Shapeless + ProvingGround
2017-05-22 в 9:11, admin, рубрики: dependent type, homotopy type theory, scala, type level programming, type theory, зависимые типы, математика, скала, типы данных, функциональное программированиеАналог std::vector из C++11 на чистом C89 и как я его писал
2017-03-17 в 11:36, admin, рубрики: C, вектор, Занимательные задачки, макросы, массив, меня отчислят, ненормальное программирование, обобщённое программирование, пиши компилятор, пиши курсовую, Си, типы данных, шаблоны, метки: си
Жилой массив людей. Нет, серьёзно.
Холивары между ценителями Си и приверженцами его "сына" в лице C++ начались ещё до моего рождения и прекратятся разве что после смерти обоих этих языков и меня заодно. Адепты великого творения Кернигана-Ритчи до последней секунды рабочего дня готовы доказывать аксиомы приспешникам Страуструпа про вечность Си и его невероятную гибкость. Те в ответ им по-свойски советуют лучше порадоваться рабочему дню, ведь он вот-вот окажется последним – двадцать первому веку кроссплатформенный ассемблер не нужен. Распаляясь, сторонники Си приводят давно прошедшие через голову навылет миллионы тезисов "почему Си лучше C++", при этом каждый раз подчёркивая, что второй все достоинства первого растерял ещё будучи в отцовской утробе, попутно утратив лик человеческий. Обвиняемая сторона в обиде не остаётся и… а хотя постойте, о чём это я.
Я люблю Си, уважаю C++ и не переношу холивары (честно). При этом я осознаю, что в Си действительно не хватает многого, и яркий тому пример – отсутствие удобной работы с данными. В C++ эту проблему во многом решает STL и свойства самого языка. На мой студенческий взгляд, здесь особо отличается всем знакомый std::vector. Если стало интересно, как я реализовал его аналог средствами C89 – прошу под кат.
Подмостки для Вавилонской башни, или О собственных типах данных для многоязычных приложений
2016-12-05 в 7:29, admin, рубрики: .net, i18n, localization, абстрактные типы данных, Анализ и проектирование систем, Блог компании CUSTIS, интернационализация, локализация, многоязычность, Программирование, Проектирование и рефакторинг, строки, типы данных
Гравюра М. Эшера «Вавилонская башня», 1928
Введение
Возможно, вы готовы к тому, что ваше приложение будет многоязычным уже на старте проекта. Но скорее всего, новость о необходимости интернационализации, как это однажды уже случилось с человечеством, застанет вас в разгаре строительства Вавилонской башни. В любом случае полезно иметь при себе джентльменский набор средств, дающих шанс завершить стройку века успешно.
Спустя четыре тысячи лет после Вавилонского столпотворения технологии предлагают нам несколько замечательных инструментов. Что же у нас есть?
Во-первых, сборная солянка — абстракция локали (locale). Локаль включает не только язык, но еще и письменность, календарь, правила форматирования чисел, денежных единиц, дат и пр.
Во-вторых, Юникод. Юникод — это не просто таблица кодирования символов. Это еще и различные формы одних и тех же букв, диакритические знаки, порядок сортировки символов, правила изменения регистра, алгоритмы нормализации строк, семейство кодировок UTF и многое другое.
Все это большое подспорье. Такие возможности, как правило, уже встроены в операционные системы и доступны в стандартных библиотеках. Программисты и пользователи во всех уголках планеты благополучно применяют одни и те же операционные системы, средства разработки, базы данных. Читать полностью »
Perl6 — Работа с типами данных
2013-08-16 в 16:57, admin, рубрики: perl, perl6, typeof, Программирование, типы данных, метки: perl6, typeof, типы данных До сих пор в статьях было лишь поверхностное упоминание о типах данных — объявление переменной определенного типа, либо указание результата операции, но все что мы могли, это лишь терпеть выходки компилятора — «хочу умру (die), захочу варнинг кину, или просто поменяю тип».
Собственно, для тех кто хочет почувствовать себя богом хоть как-то важным в управлении типами в своем же скрипте, добро пожаловать под кат.
Читать полностью »
Как устроен namedtuple или динамическое создание типов
2013-08-13 в 5:33, admin, рубрики: namedtuple, python, Блог компании Буруки, коллекции, разработка, структуры данных, типы данных Мы в Буруках любим не только людей и цифры. Мы также без устали совершенствуемся во владении нашим основным инструментом, языком Python. Ссылка для тех, кто хочет совершенствоваться с нами. В этой статье-переводе автор разбирает устройство namedtuple и по ходу рассказывает об одной из основных концепций языка.
Пару дней назад я был на пути в Сан-Франциско. Интернета в самолёте не было, поэтому я читал исходники стандартной библиотеки Python 2.7. Реализация namedtuple показалась мне особенно интересной, наверное, потому, что на деле всё гораздо проще, чем я думал раньше.
Вот здесь лежат исходники. Если вы никогда раньше не знали о namedtuple, то рекомендую ознакомиться с этой функцией.
Читать полностью »
Что сложного может быть в вычислении гипотенузы?
2013-01-08 в 12:11, admin, рубрики: Алгоритмы, гипотенуза, математика, переполнение, Программирование, типы данныхВ библиотеках различных языков программирования часто может быть включена функция для вычисления гипотенузы прямоугольного треугольника (или вы сами можете написать такую функцию для решения той или иной задачи).
На первый взгляд это может показаться тривиальной задачей, не так ли? Если сторонами треугольника являются x и y, то, формально, формулой для вычисления гипотенузы будет:
sqrt(x*x + y*y)
Это работает теоретически, но на практике данный подход может приводить к ошибке. Если значение x достаточно велико, то вычисление x*x может привести к переполнению типа данных (ни один тип данных от этого не застрахован, если не рассматривать длинную арифметику), и результатом вычислений будет бесконечность.
Читать полностью »
Особенности работы с переменными и литералами в Perl6
2012-09-26 в 18:19, admin, рубрики: perl, perl6, контексты, Песочница, типы данных, метки: perl6, контексты, типы данных Не так давно я решил начать изучать Perl6, даже не смотря на то, что фактически полностью работающего компилятора ещё нету. Подумал что можно смотреть Synopsis'ы, смотреть что из написанного в них уже работает, и изучать как именно это работает на различных примерах. Этим я и начал заниматься, попутно записывая себе в блокнот результаты различных манипуляций с переменными.
И вот в качестве своего первого поста я решил поделиться своими познаниями: тем, что обычно авторы материала оставляют на самостоятельную «проработку» — ответы на вопросы по типу «а что будет если ...» или «а что из себя это представляет в языке».
В этой статье Я опишу какие основные типы данных есть в этом языке и частично затрону вопрос о контекстах — одной из основных особенностей языка Perl.
Читать полностью »