Из значений в типы...

Хаскель поддерживает зависимые типы — это уже давно не для кого не секрет. Конечно в нем это не очень родная возможность, но все же успешные опыты существуют. Но долго мне было непонятно как такое (см. ниже код на Агде) сделать на Хаскеле. Проблема в том, что значения 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.