Ограничить число в диапазоне (Haskell)

Question

Я выставляю функцию, которая принимает два параметра, один - минимальная граница, а другой - максимальная граница. Как я могу гарантировать, используя типы, что, например, минимальная граница не больше максимальной границы?

Я хочу избежать создания умного конструктора и возврата значения Maybe, потому что это сделает все использование более громоздким.

Спасибо

Answer 1

Это не совсем отвечает на ваш вопрос, но иногда работает один подход - изменить вашу интерпретацию вашего типа. Например, вместо

data Range = {lo :: Integer, hi :: Integer}

вы могли бы использовать

data Range = {lo :: Integer, size :: Natural}

Таким образом, нет способа представить недопустимый диапазон.

Answer 2

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

Решение использует GHC.TypeLits модуль из базы, а также из пакета typelits-свидетелей.

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

{-# language TypeFamilies #-}
{-# language TypeOperators #-}
{-# language DataKinds #-}
{-# language ScopedTypeVariables #-}

import GHC.TypeLits
import GHC.TypeLits.Compare
import Data.Type.Equality
import Data.Proxy
import Control.Applicative

difference :: forall n m. (KnownNat n,KnownNat m,n <= m) 
           => Proxy n 
           -> Proxy m 
           -> Integer
difference pn pm = natVal pm - natVal pn

Мы можем проверить это из GHCi:

ghci> import Data.Proxy
ghci> :set -XTypeApplications
ghci> :set -XDataKinds
ghci> difference (Proxy @2) (Proxy @7)
5
ghci> difference (Proxy @7) (Proxy @2)
** TYPE ERROR **

Но что, если мы хотим использовать функцию со значениями, определенными во время выполнения? Скажем, значения, которые мы читаем из консоли или из файла?

main :: IO ()
main = do
   case (,) <$> someNatVal 2 <*> someNatVal 7 of
       Just (SomeNat proxyn,SomeNat proxym) ->
            case isLE proxyn proxym of
                Just Refl -> print $ difference proxyn proxym 
                Nothing   -> error "first number not less or equal"
       Nothing ->     
            error "could not bring KnownNat into scope"

В этом случае мы используем такие функции, как someNatVal а также isLE, Эти функции могут не работать с Nothing, Однако, если они преуспевают, они возвращают значение, которое "свидетельствует" о некотором ограничении. И путем сопоставления с образцом свидетеля мы вводим это ограничение в область действия (это работает, потому что свидетель является GADT).

В примере Just (SomeNat proxyn,SomeNat proxym) образец соответствия приносит KnownNat ограничения для двух аргументов в область. И Just Refl образец соответствия приносит n <= mограничение в сферу. Только тогда мы можем позвонить нашим difference функция.

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

Answer 3

То, что вы просите, это зависимые типы. Есть хороший учебник на https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell

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

Answer 4

Вам не нужно вызывать Maybe тип, чтобы воспользоваться "умными конструкторами". Если вам нравится, вы можете принять конструкторы любой формы (min,max) или же (max,min) и до сих пор создать data тип, который правильно интерпретирует, какой есть какой.

Например, вы можете сделать небольшой модуль:

module RangeMinMax (
               Range,
               makeRange
              )
where

data Range = Range (Integer,Integer)
  deriving Show
makeRange a b = Range (min a b, max a b)

И теперь, когда вы создаете Range с помощью makeRange, 2-кортеж будет автоматически упорядочен так, чтобы он был в форме (min,max), Обратите внимание, что конструктор для Range не экспортируется, поэтому пользователь модуля не может создать недействительный Range- вам просто нужно убедиться, что вы создаете действительные в этом модуле.