Рубрика «dependent type»

в 12:21, , рубрики: c++, dependent type, elm, haskell, idris, Model-Updater-View, scala, зависимые типы, интерфейсы, функциональное программирование

Паттерн Model-Update-View и зависимые типы - 1

Model-Updater-View — функциональный паттерн, успешно применяемый в языке Elm в основном для разработки пользовательских интерфейсов. Что бы им воспользоваться надо создать тип Model, представляющий полное состояние программы, тип Message, описывающий события внешней среды, на которые программа должна реагировать, меняя свое состояние, функцию updater, которая из старого состояния и сообщения создает новое состояние прораммы и функции view, которая вычисляет по состоянию программы требуемые воздействия на внешнюю среду, которые порождают события типа Message. Паттерн очень удобный, но у него есть маленький недостаток — он не позволяет описать какие собятия имеют смысл для конкретных состояний программы.

Схожая проблема возникает (и решается) и при использовании ОО-паттерна State.

Язык Elm простой, но очень строгий — он проверяет, что функция updater хоть как-то обрабатывает все возможные сочетания модели-состояние и сообщения-события. По этому приходится писать лишний, пусть и тривиальный — как правило оставляющий модель без изменений, код. Я хочу продемонстрировать, как этого можно избежать в более сложных языках — Idris, Scala, C++ и Haskell.
Читать полностью »

в 6:15, , рубрики: dependent type, generics, java, jvm, scala, type erasure, Программирование

Простой код на Java: generic интерфейс, класс который его реализует, и метод, принимающий его экземпляр:

//Gen.java:
public interface Gen<A> {
    A value();
}

//GenInt.java:
public class GenInt implements Gen<Integer> {
    private final int i;
    public GenInt(int i) {
        this.i = i;
    }
    @Override
    public Integer value() {
        return i;
    }
}

//GenTest.java:
public class GenTest {
    public static <A extends Gen<T>, T> T test(A a) {
        return a.value();
    }
    public static void main(String[] argv) {
        GenInt g = new GenInt(42);
        Integer i = test(g);
    }
}

Он компилируется и даже запускается. Как вы думаете, что будет, если вам захочется вызывать метод test из Scala?

object TestFail extends App {
  val genInt = new GenInt(42)
  val i = GenTest.test(genInt)
}

Читать полностью »

в 9:11, , рубрики: dependent type, homotopy type theory, scala, type level programming, type theory, зависимые типы, математика, скала, типы данных, функциональное программирование

Всем привет. Хочу поделиться своим опытом использования библиотеки ProvingGround, написанной на Скале с использованием Shapeless. У библиотеки имеется документация, правда, не очень обширная. Автор библиотеки — Сиддхартха Гаджил из Indian Institute of Science. Библиотека экспериментальная. Сам Сиддхартха говорит, что это пока не библиотека, а «work in progress». Глобальная цель библиотеки — брать статью живого математика, парсить текст, переводить естественный язык с формулами в формальные доказательства, которые мог бы чекать компилятор. Понятно, что до этого еще очень далеко. Пока что в библиотеке можно работать с зависимыми типами и основами гомотопической теории типов (HoTT), (полу-) автоматически доказывать теоремы.
Читать полностью »

Главная   |  Архив новостей  |   Android  |   Google  |   Apple  |   Microsoft  |   Информационная безопасность  |   Веб – разработка
Публикации RSS  |  Комментарии RSS
https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js