понимание функций уровня типов в haskell - PullRequest
Новая
       50

понимание функций уровня типов в haskell

0 голосов
/ 05 августа 2020

Я пытаюсь понять, как работают функции Plus и Times в приведенном ниже коде. Я не понимаю:

  1. Как вы вызываете эти функции в ghci для работы с вектором?
  2. Почему они должны работать на уровне типа? С каким типом они работают?
  3. Как они оценивают результат?

Для plus у нас есть Plus (S m) n = S (Plus m n), но как оценивается (Plus m n). Аналогично, как оценивается (Times n m)? 

{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, GADTs #-}
{-# LANGUAGE UndecidableInstances, StandaloneDeriving #-}

module Vector where

-- Natural numbers, values will be promoted to types
data Nat
  = Z     -- Zero
  | S Nat -- Successor (+1)

data Vec (a :: *) :: Nat -> * where
  -- Nil has zero length
  Nil :: Vec a Z
  -- Cons has length of the tail + 1
  Cons :: a -> Vec a n -> Vec a (S n)

deriving instance Show a => Show (Vec a n)

-- head :: [a] -> a
hd :: Vec a (S n) -> a
hd (Cons x xs) = x

-- tail :: [a] -> [a]
tl :: Vec a (S n) -> Vec a n
tl (Cons x xs) = xs

-- map :: (a -> b) -> [a] -> [b]
vMap :: (a -> b) -> Vec a n -> Vec b n
vMap f Nil = Nil
vMap f (Cons x xs) = Cons (f x) (vMap f xs)

-- (++) :: [a] -> [a] -> [a]
vAppend :: Vec a n -> Vec a m -> Vec a (Plus n m)
vAppend Nil         xs = xs
vAppend (Cons y ys) xs = Cons y (vAppend ys xs)

-- Type-level addition
type family Plus (x :: Nat) (y :: Nat) :: Nat where
  Plus Z     n = n
  Plus (S m) n = S (Plus m n)


-- concat :: [[a]] -> [a]
vConcat :: Vec (Vec a n) m -> Vec a (Times m n)
vConcat Nil = Nil
vConcat (Cons xs xss) = xs `vAppend` vConcat xss

-- Type-level multiplication
type family Times (x :: Nat) (y :: Nat) :: Nat where
  Times Z     m = Z
  Times (S n) m = Plus m (Times n m)

vFilter :: (a -> Bool) -> Vec a n -> [a]
vFilter p Nil = []
vFilter p (Cons x xs)
  | p x = x : vFilter p xs
  | otherwise = vFilter p xs

1 Ответ

1 голос
/ 05 августа 2020

Позвольте мне сначала определить более удобный синоним для Cons: 

infixr 5 #:
(#:) :: a -> Vec a n -> Vec a (S n)
(#:) = Cons

Как вы вызываете эти функции в ghci для работы с вектором?

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

*Vector> :set -XDataKinds
*Vector> let v = 4 #: 9 #: 13 #:Nil

*Vector> :t v
v :: Num a => Vec a ('S ('S ('S 'Z)))
*Vector> v
Cons 4 (Cons 9 (Cons 13 Nil))

*Vector> let w = 7 #: 8 #: 6 #:Nil

*Vector> :t vAppend v w
vAppend v w :: Num a => Vec a ('S ('S ('S ('S ('S ('S 'Z))))))
*Vector> vAppend v w
Cons 4 (Cons 9 (Cons 13 (Cons 7 (Cons 8 (Cons 6 Nil)))))

Для оценки семейств типов как функций уровня типа сами по себе, используйте команду GHCi :kind!: 

*Vector> :kind! Plus ('S 'Z) ('S ('S ('S 'Z)))
Plus ('S 'Z) ('S ('S ('S 'Z))) :: Nat
= 'S ('S ('S ('S 'Z)))

Почему они должны работать на уровне типа? С каким типом они работают?

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

foo :: [a] -> [a] -> String

, но это точно означает, что длины должны быть идентичными: 

foo' :: Vec a n -> Vec a n -> String

Конкретным примером является zip. Prelude.zip допускает списки разной длины, но это означает, что более длинный список в основном обрезается до длины более короткого, что может привести к неожиданному поведению. В версии Vector 

vZip :: Vec a n -> Vec b n -> Vec (a,b) n
vZip Nil Nil = Nil
vZip (Cons x xs) (Cons y ys) = Cons (x,y) $ vZip xs ys

этого не может произойти: 

*Vector> vZip v w
Cons (4,7) (Cons (9,8) (Cons (13,6) Nil))

*Vector> vZip (vAppend v v) w
<interactive>:22:7: error:
    • Couldn't match type ‘'S ('S ('S 'Z))’ with ‘'Z’
      Expected type: Vec a ('S ('S ('S 'Z)))
        Actual type: Vec a (Plus ('S ('S ('S 'Z))) ('S ('S ('S 'Z))))
    • In the first argument of ‘vZip’, namely ‘(vAppend v v)’
      In the expression: vZip (vAppend v v) w
      In an equation for ‘it’: it = vZip (vAppend v v) w

Обратите внимание, что даже если бы это выражение было записано где-то глубоко в большой программе, вы бы сразу получили ошибка во время компиляции, вместо проблем во время выполнения, когда-нибудь позже.

Как они оценивают результат?

Это зависит, а вы не На самом деле нужно проявлять осторожность, но важно то, что компилятор отсеивает все, что могло go неправильно † , и немедленно выдает сообщение об ошибке. Если все вычисления типов доказуемо верны, то компилятор жестко встраивает код, соответствующий этим типам, в вашу программу, стирает сами типы, и среда выполнения работает, по сути, как в программе Haskell с простыми старыми списками.

† Иногда, к сожалению, он также выдает вам сообщение об ошибке, когда код действительно правильный и безопасный, но компилятор не может это доказать.
...