Есть ли язык с ограниченными типами?
Есть ли типизированный язык программирования, где я могу ограничить типы, как в следующих двух примерах?
Вероятность - это число с плавающей запятой с минимальным значением 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.
7 ответов
То, что вы хотите, называется типами уточнения.
Можно определить Probability в Агде: Проб.агда
Тип массовой функции вероятности с условием суммирования определяется в строке 264.
Есть языки с более прямым типом уточнения, чем в Agda, например, ATS
Вы можете сделать это в Haskell с помощью Liquid Haskell, который расширяет Haskell типами уточнения. Предикаты управляются решателем SMT во время компиляции, что означает, что доказательства являются полностью автоматическими, но логика, которую вы можете использовать, ограничена тем, что обрабатывает решатель SMT. (К счастью, современные SMT решатели достаточно универсальны!)
Одна проблема заключается в том, что я не думаю, что Liquid Haskell в настоящее время поддерживает поплавки. Если этого не произойдет, то можно будет исправить, потому что существуют теории чисел с плавающей запятой для решателей SMT. Вы также можете притвориться, что числа с плавающей точкой на самом деле рациональны (или даже использовать Rational в Хаскеле!). Имея это в виду, ваш первый тип может выглядеть так:
{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 с правилами типа "ровно один случай на конструктор".) Это означает, что типы уточнения в этом стиле менее мощные, но гораздо проще в использовании, чем полностью зависимые типы, делая их более практичными.
В Perl6 есть понятие "подмножества типов", которые могут добавлять произвольные условия для создания "подтипа".
Для вашего вопроса конкретно:
subset Probability of Real where 0 .. 1;
а также
role DPD[::T] {
has Map[T, Probability] $.map
where [+](.values) == 1; # calls `.values` on Map
}
(примечание: в текущих реализациях часть "где" проверяется во время выполнения, но поскольку "реальные типы" проверяются во время компиляции (включая ваши классы), и поскольку существуют чистые аннотации (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 subs (или несколько, на самом деле - несколько методов или другие), мы можем отправить на основе этого:
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
Nimrod - это новый язык, поддерживающий эту концепцию. Они называются поддиапазонами. Вот пример. Вы можете узнать больше о языке здесь ссылка
type
TSubrange = range[0..5]
Язык whiley поддерживает нечто очень похожее на то, что вы говорите. Например:
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. Это очень хорошо обрабатывает примеры, подобные приведенным выше, но в настоящее время борется с более сложными примерами, включающими массивы и циклические инварианты.
Для первой части, да, это был бы Паскаль, который имеет целочисленные поддиапазоны.
Для всех, кого это интересует, я подумал, что добавлю пример того, как вы можете решить эту проблему в Nim с 2019 года.
Первая часть вопросов проста, поскольку в промежутке времени, прошедшем с момента, когда был задан этот вопрос, Nim получил возможность генерировать типы поддиапазонов на float (а также порядковые типы и типы перечислений). В приведенном ниже коде определены два новых типа поддиапазонов с плавающей запятой:Probability а также ProbOne.
Вторая часть вопроса более сложная - определение типа с ограничениями на функцию его полей. Предлагаемое мной решение напрямую не определяет такой тип, а вместо этого использует макрос (makePmf) связать создание константы Table[T,Probability] возражать против возможности создать действительный ProbOneобъект (таким образом гарантируя, что PMF действителен). ВmakePmf макрос оценивается во время компиляции, гарантируя, что вы не сможете создать недопустимую таблицу PMF.
Обратите внимание, что я относительный новичок в Nim, поэтому это может быть не самый идиоматический способ написать этот макрос:
import macros, tables
type
Probability = range[0.0 .. 1.0]
ProbOne = range[1.0..1.0]
macro makePmf(name: untyped, tbl: untyped): untyped =
## Construct a Table[T, Probability] ensuring
## Sum(Probabilities) == 1.0
# helper templates
template asTable(tc: untyped): untyped =
tc.toTable
template asProb(f: float): untyped =
Probability(f)
# ensure that passed value is already is already
# a table constructor
tbl.expectKind nnkTableConstr
var
totprob: Probability = 0.0
fval: float
newtbl = newTree(nnkTableConstr)
# create Table[T, Probability]
for child in tbl:
child.expectKind nnkExprColonExpr
child[1].expectKind nnkFloatLit
fval = floatVal(child[1])
totprob += Probability(fval)
newtbl.add(newColonExpr(child[0], getAst(asProb(fval))))
# this serves as the check that probs sum to 1.0
discard ProbOne(totprob)
result = newStmtList(newConstStmt(name, getAst(asTable(newtbl))))
makePmf(uniformpmf, {"A": 0.25, "B": 0.25, "C": 0.25, "D": 0.25})
# this static block will show that the macro was evaluated at compile time
static:
echo uniformpmf
# the following invalid PMF won't compile
# makePmf(invalidpmf, {"A": 0.25, "B": 0.25, "C": 0.25, "D": 0.15})
Примечание. Хорошим преимуществом использования макроса является то, что nimsuggest (как интегрировано в VS Code) будет даже выделять попытки создать недопустимую таблицу Pmf.
Модула 3 имеет поддиапазонные типы. (Поддиапазоны ординалов.) Так что для вашего Примера 1, если вы хотите отобразить вероятность на целочисленный диапазон некоторой точности, вы можете использовать это:
TYPE PROBABILITY = [0..100]
При необходимости добавьте значащие цифры.
Ссылка: Подробнее о порядковых поддиапазонах здесь.