Определение натуральных чисел в функциональных языках, как Ada подтипы

Question

В Ada для определения натуральных чисел можно написать следующий образом:

subtype Natural is Integer range 0 .. Integer'Last; 

Это типобезопасное и проверяются во время компиляции. Это просто (однострочный код) и эффективный (он не использует рекурсию для определения натуральных чисел, как это делает многие функциональные языки). Есть ли какой-либо функциональный язык, который может обеспечить аналогичную функциональность?

Благодаря

Answer 1

Это типобезопасный и проверяется во время компиляции.

Как вы уже указали в комментариях к своему вопросу, он не проверяется во время компиляции. Также нет эквивалентной функциональности в модуле-2 или любом другом готовом к выпуску универсальном языке программирования.

Возможность проверки ограничений, подобных этому во время компиляции, - это то, что требует зависимых типов, типов уточнения или подобных конструкций. Вы можете найти такие функции в теоретических теоремах, как Coq или Agda или в экспериментальных/академических языках, например ATS или Liquid Haskell.

Теперь из тех языков, которые я упомянул, Coq и Agda определяют рекурсивно их типы Nat, так что это не то, что вы хотите, и ATS является обязательным языком. Так что листья Liquid Haskell (плюс языки, о которых я не упоминал, конечно). Liquid Haskell - это Haskell с аннотациями дополнительного типа, поэтому он определенно является функциональным языком. В Liquid Haskell можно определить MyNat (тип с именем Nat уже определен в стандартной библиотеке) типа как это:

{-@ type MyNat = {n:Integer | n >= 0} @-} 

, а затем использовать его как это:

{-@ fac :: MyNat -> MyNat @-} 
fac :: Integer -> Integer 
fac 0 = 1 
fac n = n * fac (n-1) 

Если вы попробуете для вызова fac с отрицательным числом в качестве аргумента вы получите ошибку компиляции. Вы также получите ошибку компиляции, если вы вызываете ее с пользовательским вводом в качестве аргумента, если вы специально не убедитесь, что вход был неотрицательным. Вы также получите ошибку компиляции, если вы удалили строку fac 0 = 1, потому что теперь n на следующей строке может быть 0, что делает n-1 отрицательным при вызове fac (n-1), поэтому компилятор отвергнет это.

Следует отметить, что даже при использовании современных методов вывода типов нетривиальные программы на таких языках будут иметь довольно сложные сигнатуры типов, и вы потратите много времени и усилий на гонку ошибки через все более сложные джунгли типов подписей, имеющих только непонятные ошибки типа, которые помогут вам. Таким образом, есть цена на безопасность, которая предлагает вам такие функции, как эти. Следует также отметить, что на полном языке Тьюринга вам иногда придется записывать проверки времени выполнения для случаев, которые, как вы знаете, не могут произойти, поскольку компилятор не может доказать все, даже если вы думаете, что это должно произойти.

Answer 2

Типичная ракета, типизированный диалект Racket, имеет богатый набор числовых подтипов и знает о множестве свойств закрытия (например, сумма двух неотрицательных чисел неотрицательна, сумма двух точных целых чисел равна точное целое число и т. д.).Вот простой пример:

#lang typed/racket 
(: f : (Nonnegative-Integer Nonnegative-Integer -> Positive-Integer)) 
(define (f x y) 
    (+ x y 1)) 

проверка типов выполняется статически, но, конечно, не программа проверки в состоянии доказать каждый истинный факт о числовых подтипов. Например, следующая функция фактически возвращает только значения типа Nonnegative-Integer, но правила типа для вычитания допускают только TR для завершения типа результата Integer.

> (lambda: ([x : Nonnegative-Integer] [y : Nonnegative-Integer]) 
    (- x (- x y))) 
- : (Nonnegative-Integer Nonnegative-Integer -> Integer) 
#<procedure> 

типизированного Ракетка подход к номерам описан в Typing Цифровую башня по Санкт-Amour и др (появился в PADL 2012). Обычно есть ссылка на бумагу here, но ссылка, похоже, сейчас нарушена. Google имеет кэшированный рендеринг PDF как HTML, если вы ищете название.