Как я могу обработать Проверку. Ошибка в моем ViewModel вместо кода моего Представления позади?

1136 Следующее - это трюк, но это довольно безопасный трюк, поэтому попробуйте его дома. Он использует некоторые из новых интересных игрушек, чтобы испечь инварианты порядка порядка в mergeSort.

{-# LANGUAGE GADTs, PolyKinds, KindSignatures, MultiParamTypeClasses,
    FlexibleInstances, RankNTypes, FlexibleContexts #-}

У меня будут натуральные числа, просто для простоты.

data Nat = Z | S Nat deriving (Show, Eq, Ord)

Но я определю <= в классе типов Prolog, так что средство проверки типов может попытаться определить порядок неявно.

class LeN (m :: Nat) (n :: Nat) where
instance             LeN Z n where
instance LeN m n =>  LeN (S m) (S n) where

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

data OWOTO :: Nat -> Nat -> * where
  LE :: LeN x y => OWOTO x y
  GE :: LeN y x => OWOTO x y

Мы хотели бы знать, что каждые два числа действительно можно заказать, если у нас есть их представление во время выполнения. В наши дни мы получаем это, построив одноэлементное семейство для Nat. Natty n - это тип копий времени выполнения n.

data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

Проверка того, какие числа существуют, во многом похожа на обычную булеву версию, за исключением доказательств. Этап требует распаковки и повторной упаковки, потому что типы меняются. Вывод экземпляра хорош для логики.

owoto :: forall m n. Natty m -> Natty n -> OWOTO m n
owoto Zy      n       = LE
owoto (Sy m)  Zy      = GE
owoto (Sy m)  (Sy n)  = case owoto m n of
  LE -> LE
  GE -> GE

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

data Bound x = Bot | Val x | Top deriving (Show, Eq, Ord)

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

class LeB (a :: Bound Nat)(b :: Bound Nat) where
instance             LeB Bot     b        where
instance LeN x y =>  LeB (Val x) (Val y)  where
instance             LeB (Val x) Top      where
instance             LeB Top     Top      where

А вот упорядоченные списки чисел: OList l u - это последовательность x1 :< x2 :< ... :< xn :< ONil такая, что l <= x1 <= x2 <= ... <= xn <= u. x :< проверяет, что x находится выше нижней границы, затем накладывает x в качестве нижней границы на хвосте.

data OList :: Bound Nat -> Bound Nat -> * where
  ONil :: LeB l u => OList l u
  (:<) :: forall l x u. LeB l (Val x) =>
          Natty x -> OList (Val x) u -> OList l u

Мы можем написать merge для упорядоченных списков точно так же, как если бы они были обычными. Ключевым инвариантом является то, что если оба списка имеют одни и те же границы, то же происходит и их слияние.

merge :: OList l u -> OList l u -> OList l u
merge ONil      lu         = lu
merge lu        ONil       = lu
merge (x :< xu) (y :< yu)  = case owoto x y of
  LE  -> x :< merge xu (y :< yu)
  GE  -> y :< merge (x :< xu) yu

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

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

data NATTY :: * where
  Nat :: Natty n -> NATTY

natty :: Nat -> NATTY
natty Z      =                           Nat Zy
natty (S n)  = case natty n of Nat n ->  Nat (Sy n)

Нам нужно верить, что этот перевод дает нам NATTY, который соответствует Nat, который мы хотим отсортировать. Это взаимодействие между Nat, Natty и NATTY немного разочаровывает, но это то, что требуется в Haskell только сейчас. Получив это, мы можем построить sort обычным способом «разделяй и властвуй».

deal :: [x] -> ([x], [x])
deal []        = ([], [])
deal (x : xs)  = (x : zs, ys) where (ys, zs) = deal xs

sort :: [Nat] -> OList Bot Top
sort []   = ONil
sort [n]  = case natty n of Nat n -> n :< ONil
sort xs   = merge (sort ys) (sort zs) where (ys, zs) = deal xs

Меня часто удивляет, сколько программ, которые имеют для нас смысл, могут иметь такой же смысл для проверки типов.

[Вот какой-то запасной комплект, который я собрал, чтобы увидеть, что происходит.

instance Show (Natty n) where
  show Zy = "Zy"
  show (Sy n) = "(Sy " ++ show n ++ ")"
instance Show (OList l u) where
  show ONil = "ONil"
  show (x :< xs) = show x ++ " :< " ++ show xs
ni :: Int -> Nat
ni 0 = Z
ni x = S (ni (x - 1))

И ничего не было спрятано.]