Хаскель поддерживает зависимые типы — это уже давно не для кого не секрет. Конечно в нем это не очень родная возможность, но все же успешные опыты существуют. Но долго мне было непонятно как такое (см. ниже код на Агде) сделать на Хаскеле. Проблема в том, что значения n и m — это (внимание) значения, а они присутствуют в типе. В Агде так можно, но в Хаскеле типы и значения строго разделены.
main : IO Unit main = getContents >>= λ stdin → let (n , m) = readℕ×ℕ stdin proof : n ≤ m ⊎ n > m proof = n ≤? m in putStrLn $ show proof
В этом примере считывается со стандартного ввода два натуральных числа, далее строится доказательство, что либо первое меньше или равно второго, либо первое больше второго. В конце доказательство выводится на экран. Так выглядит индуктивный тип, представляющий доказательство неравенства. Его конструкторы следует воспринимать, как аксиомы.
data _≤_ : ℕ → ℕ → Set where z≤n : ∀ {n} → zero ≤ n s≤s : ∀ {m n} → m ≤ n → suc m ≤ suc n
А так оно работает:
dima@hpmini:~/Documents/Agda$ ./Test 1 2 (s≤s z≤n) : n ≤ m dima@hpmini:~/Documents/Agda$ ./Test 2 1 (s≤s (s≤s z≤n)) : n > m
Для значений "1 2" сначала доказываем что 0 ≤ 1 с помощью первой аксиомы, и далее с помощью второй аксиомы увеличиваем каждое значение на единицу. Касательно второго примера, нужно уточнить, что "больше" выражается через меньше равно: n > m = suc m ≤ n.
Haskell
На Хаскеле нужно немножко магии. Сначала заметим, что будем мы использовать синглтон-тип SNat n (не путать с ООП-шним синглтоном):
data SNat n where SZ :: SNat Z SS :: SNat n -> SNat (S n)
Значения синглтона как бы повторяют свой тип, что позволяет матчить по типу. Так же для удобства завернем наш синглтон в мономорфный тип, это разрешит нам передавать его из функций в функции и разворачивать где нужно, доставая значение, которое может иметь разный тип в разных ситуациях.
data HNat = forall n. HNat (SNat n)
Так же нам понадобится функция для конвертации простого значения типа Nat в тип HNat. Вот что получилось:
toHNat :: Nat -> HNat toHNat = to $ HNat SZ where to h Z = h to (HNat n) (S m) = to (HNat $ SS n) m compareNat :: SNat n -> SNat m -> (n `Leq` m) `Either` (n `Ge` m) compareNat SZ m = Left . ZeroLeq $ m compareNat (SS n) SZ = Right . SuccLeqSucc . ZeroLeq $ n compareNat (SS n) (SS m) = bimap SuccLeqSucc SuccLeqSucc $ compareNat n m main = do HNat n <- read <$> getLine HNat m <- read <$> getLine print $ compareNat n m
А вот так оно работает:
*Main> main 1 2 Left (SuccLeqSucc (ZeroLeq (SS SZ))) *Main> main 2 1 Right (SuccLeqSucc (SuccLeqSucc (ZeroLeq SZ)))
Vector
Теперь попробуем что-то более практичное. Суммируем два вектора одной длинны, при этом мы будем иметь гарантию этапа компиляции, что векторы имеют одинаковую длинну, а длинна векторов при этом будет вводится с клавиатуры в runtime.
readVector :: Read a => SNat n -> String -> Maybe (Vector a n) readVector n = Vector.fromList n . map read . words main = do HNat n <- read <$> getLine Just v1 <- readVector n <$> getLine Just v2 <- readVector n <$> getLine print $ Vector.zipWithSame (+) v1 v2
Ну и конечно пример работы:
*Main> main 2 1 2 3 5 4 :- (7 :- Nil)
Вся эта радость разместилась на github.
Прошу, напишите на х-е функцию, которая склеивает Vector a n и Vector a m, получая Vector a (n + m).
ВідповістиВидалити