Проверка времени компиляции на Haskell умных конструкторов - PullRequest
Новая
       48

Проверка времени компиляции на Haskell умных конструкторов

0 голосов
/ 12 сентября 2018

Я изучаю Хаскель, бегаю по лекциям: http://www.cis.upenn.edu/~cis194/spring13/

У меня есть: 

module HanoiDisk(HanoiDisk, hanoiDisk) where
import Control.Exception
data HanoiDisk = HanoiDisk' Integer deriving (Show)
hanoiDisk :: Integer -> HanoiDisk 
hanoiDisk n = assert (n >= 1) $ HanoiDisk' n

Это работает, но если у меня есть: 

main = do 
  print(show (hanoiDisk (-3))

Я получаю ошибку только во время выполнения, а не во время компиляции.

Я очень хочу понять, как полностью исключить исключения во время выполнения.

Может ли кто-нибудь предложить альтернативный подход?

Спасибо

Ответы [ 2 ]

0 голосов
/ 13 сентября 2018

Haskell проверяет типы при компиляции кода, а не значений.Заставить типы зависеть от значений - задача «зависимых типов».Это сложная тема.

Другой способ добиться этого - заставить hanoiDisk работать не с Integer с, но с некоторым типом "PositiveInteger", который не может быть отрицательным (или0 как хорошо ..?).Это более простой подход.

Там будет нечего утверждать - вы не сможете даже записать отрицательное значение с этим типом.Вы должны будете сделать этот тип экземпляром Num, Eq, Ord и Show (возможно, также Enum).

Обычный способ - определить 

data Nat = Z | S Nat 
           deriving (Eq, Show)
0 голосов
/ 13 сентября 2018

Насколько я понимаю, вам нужен способ "красиво провалиться", когда кто-то применяет функцию hanoiDisk к аргументу, который меньше 1.

Как заявил комментатор, выполнение этого во время компиляциивыходит за рамки базового языка Haskell, и он вам не нужен в вашем повседневном коде!

Определенно, вы можете "красиво провалиться", используя тип данных Either a b.

Идея состоит в том, что если у вас есть функция hanoiDisk :: Integer -> HanoiDisk, которая принимает Integer и должна возвращать значение HanoiDisk, если вход «хороший», и какое-то значение ошибки, когдавход «плохой», вы можете закодировать его, используя альтернативные конструкторы.

Конструкторы для типа данных Either a b: Left a и Right b, где вывод ошибки будет иметь форму Left a ихороший результат будет иметь вид Right b.Давайте перепишем вашу функцию, используя это. 

hanoiDisk :: Integer -> Either String HanoiDisk 
hanoiDisk n = if n >= 1 
              then Right (HanoiDisk' n)
              else Left "a hanoi disk must be least 1"

(Возможно) Более подходящий ответ

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

Я думаю, что проблема связана с тем, как компилятор анализирует числа.Каждый раз, когда вы используете символы «0», «1», «2», «3», «4», ..., «9» для представления цифр в вашей программе, синтаксический анализатор языка ожидает, что конечный результат будет соответствоватьвведите Int, Double и т. д. и поэтому, когда вы используете эти символы, вы открываете себе возможность того, что кто-то может добавить «-» к последовательности цифр и превратить ваше неотрицательное число в отрицательное..

Давайте создадим новый модуль с именем Natural , который позволит нам создавать положительные числа.В нем мы определяем «псевдонимы» для символов «0», ..., «1», используя первые две буквы имени каждого символа (например, tw для «2»).Поскольку люди пишут натуральные числа, используя десятичную систему, мы создаем тип данных с именем Natural, который принимает два аргумента - первую цифру числа, которое мы представляем, а затем список последующих цифр.Наконец, мы выборочно экспортируем функции из модуля, чтобы запретить «злоупотребление» пользователями. 

module Natural (ze,on,tw,th,fo,fi,si,se,ei,ni,Natural(..)) where

newtype Digit = Digit Int

ze = Digit 0
on = Digit 1
tw = Digit 2
th = Digit 3
fo = Digit 4
fi = Digit 5
si = Digit 6
se = Digit 7
ei = Digit 8
ni = Digit 9

data Natural = Nat Digit [Digit]

В качестве примера, натуральное число 312 будет представлено как Nat th [on,tw].

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

Я опускаю определения экземпляров для Num,Integral, Eq, Ord и т. Д., Потому что я не думаю, что они добавят больше моего объяснения.

...