Есть ли язык с ограниченными возможностями?

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

A Вероятность - это число с плавающей запятой, минимальное значение 0.0 и максимальное значение 1.0.
```
type Probability subtype of float
where
    max_value = 0.0
    min_value = 1.0
```
Распределение дискретной вероятности - это карта, где: ключи должны быть одного типа, значения - это все вероятности и сумма значений = 1.0.
```
type DPD<K> subtype of map<K, Probability>
where
    sum(values) = 1.0
```

Насколько я понимаю, это невозможно с Haskell или Agda.

Ответ 1

То, что вы хотите, называется типами уточнения.

В Agda можно определить Probability: Prob.agda

Тип функции массы вероятности, с условием суммы определяется в строке 264.

Существуют языки с более точными типами уточнения, чем в Agda, например ATS

Ответ 2

Вы можете сделать это в Haskell с Liquid Haskell, который расширяет Haskell с помощью типы уточнения. Предикаты управляются решателем SMT во время компиляции, что означает, что доказательства полностью автоматические, но логика, которую вы можете использовать, ограничена тем, что обрабатывает решатель SMT. (К счастью, современные решатели SMT достаточно универсальны!)

Одна из проблем заключается в том, что я не думаю, что Liquid Haskell в настоящее время поддерживает float. Если это не так, это должно быть возможно исправить, потому что существуют теории чисел с плавающей точкой для решателей SMT. Вы могли бы также притворяться, что числа с плавающей запятой были фактически рациональными (или даже использовать Rational в Haskell!). Имея это в виду, ваш первый тип может выглядеть следующим образом:

{p : Float | p >= 0 && p <= 1}

Второй тип будет сложнее кодировать, особенно потому, что карты являются абстрактным типом, о котором трудно рассуждать. Если вы использовали список пар вместо карты, вы можете написать "меру" следующим образом:

measure total :: [(a, Float)] -> Float
total []          = 0 
total ((_, p):ps) = p + probDist ps

(Возможно, вы захотите обернуть [] в newtype).

Теперь вы можете использовать total в уточнении, чтобы ограничить список:

{dist: [(a, Float)] | total dist == 1}

Чистый трюк с Liquid Haskell заключается в том, что все рассуждения автоматизированы для вас во время компиляции, в обмен на использование несколько ограниченной логики. (Меры, подобные total, также очень ограничены в том, как они могут быть написаны, - это небольшое подмножество Haskell с такими правилами, как "ровно один случай для каждого конструктора".) Это означает, что типы уточнения в этом стиле менее эффективны, но намного проще чем полные зависимые типы, что делает их более практичными.

Ответ 3

Perl6 имеет понятие "подмножества типов", которое может добавлять произвольные условия для создания "подтипа".

Для конкретного вопроса:

subset Probability of Real where 0 .. 1;

role DPD[::T] {
  has Map[T, Probability] $.map
    where [+](.values) == 1; # calls `.values` on Map
}

(обратите внимание: в текущих реализациях часть "where" проверяется во время выполнения, но поскольку "реальные типы" проверяются во время компиляции (включая ваши классы), а так как существуют чистые аннотации (is pure) внутри std (что в основном perl6) (это также относится к операторам, таким как * и т.д.), это только вопрос усилий, прилагаемых к нему (и это не должно быть намного больше).

В более общем плане:

# (%% is the "divisible by", which we can negate, becoming "!%%")
subset Even of Int where * %% 2; # * creates a closure around its expression
subset Odd of Int where -> $n { $n !%% 2 } # using a real "closure" ("pointy block")

Затем вы можете проверить, совпадает ли число с оператором Smart Matching ~~:

say 4 ~~ Even; # True
say 4 ~~ Odd; # False
say 5 ~~ Odd; # True

И, благодаря multi sub (или нескольким любым, действительно - мульти-методам или другим), мы можем отправить на основе этого:

multi say-parity(Odd $n) { say "Number $n is odd" }
multi say-parity(Even) { say "This number is even" } # we don't name the argument, we just put its type
#Also, the last semicolon in a block is optional

Ответ 4

Nimrod - это новый язык, поддерживающий эту концепцию. Они называются поддиапазонами. Вот пример. Вы можете узнать больше о языке здесь ссылка

type
  TSubrange = range[0..5]

Ответ 5

Для первой части да, это будет Pascal, который имеет целочисленные поддиапазоны.

Ответ 6

Язык в режиме "Входящий" поддерживает что-то очень похожее на то, что вы говорите. Например:

type natural is (int x) where x >= 0
type probability is (real x) where 0.0 <= x && x <= 1.0

Эти типы также могут быть реализованы как предварительные или пост-условия:

function abs(int x) => (int r)
ensures r >= 0:
    //
    if x >= 0:
        return x
    else:
        return -x

Язык очень выразителен. Эти инварианты и пред-/пост-условия проверяются статически с использованием решателя SMT. Это очень хорошо справляется с примерами, описанными выше, но в настоящее время борется с более сложными примерами, включающими массивы и инварианты цикла.

Ответ 7

Modula 3 имеет типы поддиапазонов. (Поддиапазоны ординалов.) Итак, для вашего примера 1, если вы готовы сопоставить вероятность с целым диапазоном некоторой точности, вы можете использовать это:

TYPE PROBABILITY = [0..100]

При необходимости добавьте важные цифры.

Ссылка: больше о ординалах поддиапазона здесь.