Использование идиоматического логического равенства (синглтоны)

Я хочу создать структуру данных для хранения элементов, помеченных на уровне типа с помощью 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, чтобы делать то, что я пытаюсь сделать?

[email protected], [email protected]

 cchalmers10 июл. 2016 г., 13:51
Вы можете удалить предупреждение вfrom' добавив функцииstoreHead :: Store e (s ': ss) -> e s а такжеstoreTail :: Store e (s ': ss) -> Store e ss и использовать их в магазине после того, как вы сопоставилиAtHead или жеInTail.
 NioBium10 июл. 2016 г., 23:38
Нет я вас понимаю Мой код используетfrom делает проверку типа и работает правильно. Вам просто нужно пометить экземпляр AtHead OVERLAPPING / экземпляр InTail OVERLAPPABLE. Вы говорите, что это не должно?
 Benjamin Hodgson10 июл. 2016 г., 23:18
@NioBium Я думаю, вы меня не так поняли:HasElemC являетсябесполезный из-за того, как вы определили свои экземпляры. Попробуйте написатьx = HasElem "a" '["a"]; x = hasElem, Это не будет проверка типа.
 NioBium10 июл. 2016 г., 21:43
Спасибо, Чалмерс, это сработало. Спасибо, Бенджамин. Перекрытия в моем случае хороши: мне не нужны полиморфные функции в ss. Хотя они могут понадобиться мне в будущем.
 Benjamin Hodgson10 июл. 2016 г., 21:23
Ваши дваHasElemC экземпляры перекрываются. GHC сочтет невозможным выполнитьHasElemC ограничение, потому что он не проверяет предварительные условия при выполнении пробного поиска. К счастью, естьхорошо известный трюк с использованием семейства типов иUndecidableInstances, (На самом деле это одно из немногих хороших применений семейств булевых типов.)
 dfeuer11 июл. 2016 г., 05:43
NioBium, я думаю, что @BenjaminHodgson может просто не понравиться частично совпадающим экземплярам, ​​чтобы он не слишком старался научиться их использовать; очень часто лучше научитьсяне к. Семейный трюк типа, к сожалению, будет более разборчивым. Например, вещь семейства типов откажется от выбора экземпляра, используя полиморфное неравенство типаa /~ (q ': a) потому что семейства типов могут представлять бесконечные типы. К счастью, перекрывающиеся экземпляры будут делать это, потому что это не влияет на безопасность типов.

Ответы на вопрос(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

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

 Benjamin Hodgson10 июл. 2016 г., 23:11
Ну синглтоны есть (аsingletons это) один конкретный способ использования GADT и типов данных. Доказательства какElem другие. Они не вписываются в единую структуру, потому что они не одиночки!
 NioBium10 июл. 2016 г., 21:47
Спасибо. Я просто пытался не изобретать колесо. Все еще надеясь, что кто-нибудь найдет решение в синглетонах на Хаскеле, если таковое существует. Какой смысл поднимать все эти функции до уровня типа, если вы не можете использовать их в доказательствах?

Ваш ответ на вопрос