Использование идиоматического логического равенства (синглтоны)
Я хочу создать структуру данных для хранения элементов, помеченных на уровне типа с помощью Symbol. Это:
data Store e (ss :: [Symbol]) where
Nil :: Store e '[]
Cons :: e s -> Store e ss -> Store e (s ': ss)
data HasElem (a :: k) (as :: [k]) where
AtHead :: HasElem a (a ': as)
InTail :: HasElem a as -> HasElem a (b ': as)
class HasElemC (a :: k) (as :: [k]) where hasElem :: HasElem a as
instance HasElemC {OVERLAPPING} a (a ': as) where hasElem = AtHead
instance HasElemC a as => HasElemC a (b ': as) where hasElem = InTail hasElem
from :: HasElemC s ss => Store e ss -> e s
from = from' hasElem
from' :: HasElem s ss -> Store e ss -> e s
-- from' _ Nil = undefined
from' h (Cons element store) = case h of
AtHead -> element
InTail h' -> from' h' store
вроде работает, если вы пренебрегаете тем фактом, что компилятор предупреждает меня, что я не предоставляюfrom' _ Nil определение (почему это, кстати? есть ли способ заставить это остановиться?) Но что я действительно хотел сделать в начале, так это использовать библиотеку синглетонов идиоматическим способом, вместо того, чтобы писать свой собственный код уровня типа. Что-то вроде этого:
import Data.Singletons.Prelude.List
data Store e (ss :: [Symbol]) where
Nil :: Store e '[]
Cons :: Sing s -> e s -> Store e ss -> Store e (s ': ss)
from :: Elem s ss ~ True => Store e ss -> e s
from (Cons evidence element nested) = ???
К сожалению, я не мог понять, как преобразовать контекст в пропозициональное равенство. Как вы можете использовать строительные блоки из библиотеки singletons, чтобы делать то, что я пытаюсь сделать?
Ответы на вопрос(1)
Не используйте логические значения! Мне кажетсядержать повторяющий себя на этот счет: булевы значения чрезвычайно ограничены в программировании с зависимой типизацией, и чем раньше вы не выучите эту привычку, тем лучше.
Elem s ss ~ True контекст обещает вам, чтоs вss где-то, но это не говоритгде, Это оставляет вас в беде, когда вам нужно произвестиs-значение из вашего спискаss, Одного бита недостаточно для ваших целей.
Сравните это с вычислительной полезностью вашего оригиналаHasElem тип, который структурирован как натуральное число, дающее индекс элемента в списке. (Сравните форму значения какThere (There Here) что это изS (S Z).) Для производстваs из спискаss вам просто нужно разыменовать индекс.
Тем не менее, вы все равно должны быть в состоянииоправляться информация, которую вы выбросили и извлечьHasElem x xs значение из контекстаElem x xs ~ True, Хотя это утомительно - вам нужно искать в списке предмет (что вы уже сделали для того, чтобы оценитьElem x xs!) и устранить невозможные случаи. Работа в Агде (определения опущены):
recover : {A : Set}
(_=?_ : (x : A) -> (y : A) -> Dec (x == y))
(x : A) (xs : List A) ->
(elem {{_=?_}} x xs == true) ->
Elem x xs
recover _=?_ x [] ()
recover _=?_ x (y :: ys) prf with x =? y
recover _=?_ x (.x :: ys) prf | yes refl = here
recover _=?_ x (y :: ys) prf | no p = there (recover _=?_ x ys prf)
Однако вся эта работа не нужна. Для начала просто используйте богатый информацией термин.
Кстати, вы должны быть в состоянии остановить GHC, предупреждая вас о неполных шаблонах, выполнивElem сопоставляя на левой стороне, а не вcase-expression:
from' :: HasElem s ss -> Store e ss -> e s
from' AtHead (Cons element store) = element
from' (InTail i) (Cons element store) = from' i store
К тому времени, когда вы окажетесь в правой части определения, для сопоставления с образцом будет слишком поздно, чтобы уточнить возможные конструкторы для других терминов слева.
singletons это) один конкретный способ использования GADT и типов данных. Доказательства какElem другие. Они не вписываются в единую структуру, потому что они не одиночки!
from'добавив функцииstoreHead :: Store e (s ': ss) -> e sа такжеstoreTail :: Store e (s ': ss) -> Store e ssи использовать их в магазине после того, как вы сопоставилиAtHeadили жеInTail.fromделает проверку типа и работает правильно. Вам просто нужно пометить экземпляр AtHead OVERLAPPING / экземпляр InTail OVERLAPPABLE. Вы говорите, что это не должно?HasElemCявляетсябесполезный из-за того, как вы определили свои экземпляры. Попробуйте написатьx = HasElem "a" '["a"]; x = hasElem, Это не будет проверка типа.HasElemCэкземпляры перекрываются. GHC сочтет невозможным выполнитьHasElemCограничение, потому что он не проверяет предварительные условия при выполнении пробного поиска. К счастью, естьхорошо известный трюк с использованием семейства типов иUndecidableInstances, (На самом деле это одно из немногих хороших применений семейств булевых типов.)a /~ (q ': a)потому что семейства типов могут представлять бесконечные типы. К счастью, перекрывающиеся экземпляры будут делать это, потому что это не влияет на безопасность типов.