Динамическое построение значений с помощью GADT с использованием типов данных
Почему сложнее построить значения с помощью типов данных, а сопоставить их с шаблонами сравнительно легко?
{-# LANGUAGE KindSignatures
, GADTs
, DataKinds
, Rank2Types
#-}
data Nat = Zero | Succ Nat
data Direction = Center | Up | Down | UpDown deriving (Show, Eq)
data Chain :: Nat -> Nat -> * -> * where
Nil :: Chain Zero Zero a
AddUp :: a -> Chain nUp nDn a -> Chain (Succ nUp) nDn a
AddDn :: a -> Chain nUp nDn a -> Chain nUp (Succ nDn) a
AddUD :: a -> Chain nUp nDn a -> Chain (Succ nUp) (Succ nDn) a
Add :: a -> Chain nUp nDn a -> Chain nUp nDn a
lengthChain :: Num b => Chain (Succ Zero) (Succ Zero) a -> b
lengthChain = lengthChain'
lengthChain' :: forall (t::Nat) (t1::Nat) a b. Num b => Chain t t1 a -> b
lengthChain' Nil = 0
lengthChain' (Add _ rest) = 1 + lengthChain' rest
lengthChain' (AddUp _ rest) = 1 + lengthChain' rest
lengthChain' (AddDn _ rest) = 1 + lengthChain' rest
lengthChain' (AddUD _ rest) = 1 + lengthChain' rest
chainToList :: Chain (Succ Zero) (Succ Zero) a -> [(a, Direction)]
chainToList = chainToList'
chainToList' :: forall (t::Nat) (t1::Nat) a. Chain t t1 a -> [(a, Direction)]
chainToList' Nil = []
chainToList' (Add a rest) = (a, Center):chainToList' rest
chainToList' (AddUp a rest) = (a, Up):chainToList' rest
chainToList' (AddDn a rest) = (a, Down):chainToList' rest
chainToList' (AddUD a rest) = (a, UpDown):chainToList' rest
listToChain :: forall (t::Nat) (t1::Nat) b. [(b, Direction)] -> Chain t t1 b
listToChain ((x, Center): xs) = Add x (listToChain xs)
listToChain ((x, Up):xs) = AddUp x (listToChain xs)
listToChain ((x, Down): xs) = AddDn x (listToChain xs)
listToChain ((x, UpDown): xs) = AddUD x (listToChain xs)
listToChain _ = Nil
Я пытаюсь создать тип данных для управления структурой, похожей на список, с той разницей, что мы могли бы добавить стрелки к элементам. Кроме того, я требую, чтобы некоторые функции работали только со списками, где количество стрелок вверх и стрелок вниз точно равно 1.
В приведенном выше коде функция listToChain не компилируется, пока chainToList компилируется нормально. Как мы можем исправить listToChain код?
2 ответа
Если вы подумаете об этом немного, вы увидите, что нет никакого типа вашего listToChain может когда-либо работать, потому что он принимает значения (b, Direction) которые не имеют информации о направлении типа на уровне, и он все равно должен каким-то образом вычислять тип индексации направления Chain во время компиляции. Это явно невозможно, поскольку во время выполнения значения могут вводиться пользователем или считываться из сокета и т. Д.
Вам нужно либо пропустить промежуточный список и создать свою цепочку непосредственно из проверенных значений во время компиляции, либо вы можете заключить полученную цепочку в экзистенциальный тип и выполнить проверку во время выполнения, чтобы преобразовать экзистенциал в более точный тип.
Итак, учитывая экзистенциальную оболочку, как
data SomeChain a where
SomeChain :: Chain nu nd a -> SomeChain a
Вы можете реализовать listToChain как
listToChain :: [(b, Direction)] -> SomeChain b
listToChain ((x, Center): xs) = withSome (SomeChain . Add x) (listToChain xs)
listToChain ((x, Up):xs) = withSome (SomeChain . AddUp x) (listToChain xs)
listToChain ((x, Down): xs) = withSome (SomeChain . AddDn x) (listToChain xs)
listToChain ((x, UpDown): xs) = withSome (SomeChain . AddUD x) (listToChain xs)
listToChain _ = SomeChain Nil
используя вспомогательную функцию withSome для более удобного обёртывания и развёртывания экзисте.
withSome :: (forall nu nd. Chain nu nd b -> r) -> SomeChain b -> r
withSome f (SomeChain c) = f c
Теперь у нас есть экзистенция, которую мы можем обойти, скрывая точные типы вверх и вниз. Когда мы хотим вызвать такую функцию, как lengthChain это требует определенных повышений и понижений, которые нам нужны для проверки содержимого во время выполнения. Один из способов сделать это - определить тип-класс.
class ChainProof pnu pnd where
proveChain :: Chain nu nd b -> Maybe (Chain pnu pnd b)
proveChain функция занимает цепочку любого nu а также nd и пытается доказать, что это соответствует конкретному pnu а также pnd, Внедрение ChainProof требует немного повторяющихся шаблонов, но затем он может предоставить доказательства для любой желаемой комбинации взлетов и падений в дополнение к единому случаю, который нам нужен для lengthChain,
instance ChainProof Zero Zero where
proveChain Nil = Just Nil
proveChain (Add a rest) = Add a <$> proveChain rest
proveChain _ = Nothing
instance ChainProof u Zero => ChainProof (Succ u) Zero where
proveChain (Add a rest) = Add a <$> proveChain rest
proveChain (AddUp a rest) = AddUp a <$> proveChain rest
proveChain _ = Nothing
instance ChainProof Zero d => ChainProof Zero (Succ d) where
proveChain (Add a rest) = Add a <$> proveChain rest
proveChain (AddDn a rest) = AddDn a <$> proveChain rest
proveChain _ = Nothing
instance (ChainProof u (Succ d), ChainProof (Succ u) d, ChainProof u d) => ChainProof (Succ u) (Succ d) where
proveChain (Add a rest) = Add a <$> proveChain rest
proveChain (AddUp a rest) = AddUp a <$> proveChain rest
proveChain (AddDn a rest) = AddDn a <$> proveChain rest
proveChain (AddUD a rest) = AddUD a <$> proveChain rest
proveChain _ = Nothing
Выше требуется расширение языка MultiParamTypeClasses а также FlexibleContexts и я использую <$> от Control.Applicative,
Теперь мы можем использовать механизм проверки, чтобы создать безопасную оболочку для любой функции, ожидающей определенного увеличения и уменьшения
safe :: ChainProof nu nd => (Chain nu nd b -> r) -> SomeChain b -> Maybe r
safe f = withSome (fmap f . proveChain)
Это может показаться неудовлетворительным решением, так как нам все еще нужно обработать случай сбоя (т.е. Nothing) но по крайней мере проверка требуется только на верхнем уровне. Внутри данного f у нас есть статические гарантии относительно структуры цепочки, и нам не нужно проводить дополнительную проверку.
Альтернативное решение
Приведенное выше решение, хотя и простое в реализации, должно обходить и перестраивать всю цепочку каждый раз, когда оно проверяется. Другим вариантом является сохранение повышающих и понижающих отсчетов как единичных натуральных чисел в экзистенциале.
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
data SomeChain a where
SomeChain :: SNat nu -> SNat nd -> Chain nu nd a -> SomeChain a
SNat тип является значением уровня эквивалента Nat так, что для каждого вида Nat есть ровно одно значение типа SNat Это означает, что даже когда тип t из SNat t стерты, мы можем полностью восстановить его путем сопоставления с образцом по значению. По расширению это означает, что мы можем восстановить полный тип Chain в экзистенциальном просто путем сопоставления с образцом на натуральных объектах без необходимости обхода самой цепи.
Построение цепи становится немного более многословным
listToChain :: [(b, Direction)] -> SomeChain b
listToChain ((x, Center): xs) = case listToChain xs of
SomeChain u d c -> SomeChain u d (Add x c)
listToChain ((x, Up):xs) = case listToChain xs of
SomeChain u d c -> SomeChain (SSucc u) d (AddUp x c)
listToChain ((x, Down): xs) = case listToChain xs of
SomeChain u d c -> SomeChain u (SSucc d) (AddDn x c)
listToChain ((x, UpDown): xs) = case listToChain xs of
SomeChain u d c -> SomeChain (SSucc u) (SSucc d) (AddUD x c)
listToChain _ = SomeChain SZero SZero Nil
Но с другой стороны, доказательства становятся короче (хотя и с несколько волосатыми сигнатурами).
proveChain :: forall pnu pnd b. (ProveNat pnu, ProveNat pnd) => SomeChain b -> Maybe (Chain pnu pnd b)
proveChain (SomeChain (u :: SNat u) (d :: SNat d) c)
= case (proveNat u :: Maybe (Refl u pnu), proveNat d :: Maybe (Refl d pnd)) of
(Just Refl, Just Refl) -> Just c
_ -> Nothing
Это использует ScopedTypeVariables явно выбрать экземпляры класса типов для ProveNat мы хотим использовать. Если мы получим доказательство того, что натуральные значения соответствуют запрошенным значениям, тогда средство проверки типов с радостью разрешит нам вернуть Just c без дальнейшего изучения.
ProveNat определяется как
{-# LANGUAGE PolyKinds #-}
data Refl a b where
Refl :: Refl a a
class ProveNat n where
proveNat :: SNat m -> Maybe (Refl m n)
Refl Тип (рефлексивность) - это часто используемый шаблон, который заставляет средство проверки типов объединять два неизвестных типа, когда мы сопоставляем шаблон на Refl конструктор (и PolyKinds позволяет ему быть универсальным для любого вида, что позволяет нам использовать его с Natс). Так что пока proveNat принимает forall m. SNat m если мы можем сопоставить образец на Just Refl после этого мы (и, что более важно, проверка типов) можем быть уверены, что m а также n на самом деле того же типа.
Примеры для ProveNat довольно просты, но требуют, опять же, некоторых явных типов, чтобы помочь выводу.
instance ProveNat Zero where
proveNat SZero = Just Refl
proveNat _ = Nothing
instance ProveNat n => ProveNat (Succ n) where
proveNat m@(SSucc _) = proveNat' m where
proveNat' :: forall p. ProveNat n => SNat (Succ p) -> Maybe (Refl (Succ p) (Succ n))
proveNat' (SSucc p) = case proveNat p :: Maybe (Refl p n) of
Just Refl -> Just Refl
_ -> Nothing
proveNat _ = Nothing
Проблема не в том, что касается datakinds. В типе
listToChain :: forall (t::Nat) (t1::Nat) b. [(b, Direction)] -> Chain t t1 b
Вы говорите, что для любых типов t t1 b Вы можете включить список пар b и направления в Chain t t1 b... но это не относится к вашей функции, например:
listToChain _ = Nil
результат этого не работает для любого типа, но только когда t, t1 оба Zero, В этом смысл GADT, он ограничивает возможные типы.
Я подозреваю, что тип, который вы хотите дать вашей функции, является зависимым, что-то вроде
listToChain :: (x :: [(b,Direction)]) -> Chain (number_of_ups x) (number_of_downs x) b
но в Haskell это недопустимо, поскольку Haskell не имеет зависимых типов. Одним из решений является использование экзистенциальной
listToChain :: forall b. [(b, Direction)] -> exists (t :: Nat) (t1 :: Nat). Chain t t1 b
это почти действительно Хаскель. К сожалению, экзистенциалы должны быть обернуты в конструкторы
data AChain b where
AChain :: Chain t t1 b -> AChain b
и тогда вы можете сделать это так:
listToChain :: forall b. [(b, Direction)] -> AChain b
listToChain ((x, Center): xs) = case (listToChain xs) of
AChain y -> AChain (Add x y)
...