Положительный целочисленный тип

Ответ 1

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

В нижеследующем, я не чувствую, что я говорю что-то большее, чем то, что трогатель затронул, упоминая очень классный звуковой инструмент Inch. Надеемся, что дополнительные слова по каждой теме прояснят вам часть пространства решений.

Что означают люди (говоря о статических гарантиях Haskell)

Обычно, когда я слышу, что люди говорят о статических гарантиях, предоставляемых Haskell, они говорят о статическом типе проверки стиля Хиндли Милнера. Это означает, что один тип нельзя смутить для другого - любое такое злоупотребление попадает во время компиляции (ex: let x = "5" in x + 1 недействительно). Очевидно, что это только царапины на поверхности, и мы можем обсудить некоторые аспекты статической проверки в Haskell.

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

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

Это хорошее решение для многих проблем. Я рекомендовал то же самое при обсуждении золотых номеров. Тем не менее, я не думаю, что это то, что вы ловите рыбу.

Точные представления

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

Более распространенным примером использования правильных представлений являются непустые списки. Если вы хотите тип, который никогда не может быть пустым, вы можете просто создать непустой тип списка:

data NonEmptyList a = Single a | Cons a (NonEmptyList a)

Это отличается от традиционного определения списка, используя Nil вместо Single a.

Возвращаясь к положительному примеру, вы можете использовать форму чисел Пеано:

data NonNegative = One | S NonNegative

Или пользовательские GADT для создания двоичных чисел без знака (и вы можете добавить Num и другие экземпляры, разрешая такие функции, как +):

{-# LANGUAGE GADTs #-}

data Zero
data NonZero
data Binary a where
  I :: Binary a -> Binary NonZero
  O :: Binary a -> Binary a
  Z :: Binary Zero
  N :: Binary NonZero

instance Show (Binary a) where
        show (I x) = "1" ++ show x
        show (O x) = "0" ++ show x
        show (Z)   = "0" 
        show (N)   = "1"

Внешние доказательства

Пока он не является частью вселенной Haskell, можно генерировать Haskell с использованием альтернативных систем (таких как Coq), которые позволяют утверждать и доказывать более богатые свойства. Таким образом, код Haskell может просто опускать такие проверки, как x > 0, но тот факт, что x всегда будет больше 0, будет статической гарантией (опять же: безопасность не из-за Haskell).

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

Исследование более описательных статических свойств

Исследовательское сообщество, которое работает с Haskell, замечательно. В то время как слишком незрелые для общего использования, люди разработали инструменты, чтобы делать такие вещи, как статическая проверка пристрастие функций и контракты. Если вы посмотрите вокруг, вы найдете это богатое поле.

Ответ 2

module Positive (toPositive, Positive(unPositive)) where

newtype Positive = Positive { unPositive :: Int }

toPositive :: Int -> Maybe Positive
toPositive n = if (n < 0) then Nothing else Just (Positive n)

Вышеприведенный модуль не экспортирует конструктор, поэтому единственный способ построить значение типа Positive - предоставить toPositive положительное целое число, которое затем можно развернуть, используя unPositive чтобы получить доступ к фактическому значению.

Затем вы можете написать функцию, которая принимает только натуральные числа, используя:

positiveInputsOnly :: Positive -> ...

Ответ 3

Я бы не выполнил свой долг как своего руководителя, если бы я не смог подключить препроцессор Adam Gundry Inch, который управляет целыми ограничениями для Haskell.

Смарт-конструкторы и барьеры абстракции - все очень хорошо, но они слишком много тестируют для запуска и не позволяют возможности узнать, что вы делаете, таким образом, чтобы проверить статически, без требуется для отладки Maybe. (Педант пишет. Автор другого ответа, по-видимому, предполагает, что 0 является положительным, что некоторые могут считать спорным. Конечно, правда состоит в том, что мы используем множество нижних границ, 0 и 1, которые происходят часто. имеют некоторое применение для верхних границ.)

В традиции Xi DML препроцессор Адама добавляет дополнительный уровень точности поверх того, что предлагает Haskell, но полученный в результате код стирает Haskell как есть. Было бы здорово, если бы то, что он сделал, можно было бы лучше интегрировать с GHC, в координации с работой над натуральными числами уровня, которые Iavor Diatchki делает. Мы стремимся выяснить, что возможно.

Чтобы вернуться к общей точке, Haskell в настоящее время недостаточно зависимо от типа ввода, чтобы разрешить построение подтипов по понятию (например, элементы Integer больше 0), но вы часто можете реорганизовать типы на более индексированную версию, которая допускает статическое ограничение. В настоящее время конструкция одноэлементного типа является самым чистым из доступных неприятных способов достижения этого. Вам понадобятся некие "статические" целые числа, а затем жители вида Integer -> * захватывают свойства определенных целых чисел, такие как "имеющие динамическое представление" (что одноэлементная конструкция, придающая каждой статической вещи уникальный динамический аналог), но и более конкретные вещи, такие как "быть положительными".

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

Ответ 4

Я знаю, что на это был дан ответ давным-давно, и я уже предоставил свой ответ, но я хотел обратить внимание на новое решение, которое стало доступно в промежуточный период: Liquid Haskell, в котором вы можете прочитать введение в здесь.

В этом случае вы можете указать, что данное значение должно быть положительным, написав:

{[email protected] myValue :: {v: Int | v > 0} #-}
myValue = 5

Аналогично, вы можете указать, что для функции f требуются только такие положительные аргументы:

{[email protected] f :: {v: Int | v > 0 } -> Int @-}

Liquid Haskell проверит во время компиляции, что заданные ограничения будут выполнены.

Ответ 5

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

Почему? Посмотрите на определение Num:

class (Eq a, Show a) => Num a where
    (+) :: a -> a -> a
    (*) :: a -> a -> a
    (-) :: a -> a -> a
    negate :: a -> a
    abs :: a -> a
    signum :: a -> a
    fromInteger :: Integer -> a

Если вы не вернетесь к использованию error (что является плохой практикой), вы не можете предоставить определения для (-), negate и fromInteger.

Ответ 6

Для GHC 7.6.1 запланированы натуральные числа на уровне типа: https://ghc.haskell.org/trac/ghc/ticket/4385

Используя эту функцию, написать тип "натуральное число" тривиально и дает производительность, которую вы никогда не сможете достичь (например, с типом числа Пеано, написанным вручную).