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

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


singleton-type haskell dependent-type
person NioBium    schedule 10.07.2016    source источник
comment
Вы можете удалить предупреждение в from', добавив функции storeHead :: Store e (s ': ss) -> e s и storeTail :: Store e (s ': ss) -> Store e ss и использовать их в магазине после того, как вы сопоставите AtHead или InTail.   -  person cchalmers    schedule 10.07.2016
comment
Два экземпляра HasElemC пересекаются. GHC сочтет невозможным снять ограничение HasElemC, потому что он не проверяет предварительные условия при поиске доказательства. К счастью, есть известный прием с использованием семейств типов и UndecidableInstances. (На самом деле это одно из немногих удачных применений семейств логических типов.)   -  person Benjamin Hodgson♦    schedule 10.07.2016
comment
Спасибо, chalmers, это сработало. Спасибо, Бенджамин. В моем случае с перекрытиями все в порядке: мне не нужны функции, полиморфные в ss. Хотя они мне могут понадобиться в будущем.   -  person NioBium    schedule 10.07.2016
comment
@NioBium Я думаю, вы меня неправильно поняли: HasElemC бесполезен из-за того, как вы определили свои экземпляры. Попробуйте написать x = HasElem "a" '["a"]; x = hasElem. Он не будет проверять тип.   -  person Benjamin Hodgson♦    schedule 11.07.2016
comment
Нет, я тебя понимаю. Мой код, использующий from, выполняет проверку типов и работает правильно. Вам просто нужно отметить экземпляр AtHead OVERLAPPING/InTail экземпляр OVERLAPPABLE. Вы говорите, что не должно?   -  person NioBium    schedule 11.07.2016
comment
NioBium, я думаю, может быть, @BenjaminHodgson может просто не любить перекрывающиеся экземпляры настолько, что он не слишком старался научиться их использовать; очень часто лучше научиться не делать. К сожалению, семейный трюк типа будет более придирчивым. Например, семейство типов откажется выбирать экземпляр с использованием полиморфного неравенства, такого как a /~ (q ': a), потому что семейства типов могут представлять бесконечное количество типов. Перекрывающиеся экземпляры с радостью это сделают, потому что это не влияет на безопасность типов.   -  person dfeuer    schedule 11.07.2016

Ответы (1)


arrow_upward
8
arrow_downward

Не используйте логические значения! Кажется, я продолжаю повторять сам по этому поводу: логические значения имеют крайне ограниченную полезность в программировании с зависимым типом и чем раньше вы отучите эту привычку, тем лучше.

Контекст 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-выражении:

from' :: HasElem s ss -> Store e ss -> e s
from' AtHead (Cons element store) = element
from' (InTail i) (Cons element store) = from' i store

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

person Benjamin Hodgson♦    schedule 10.07.2016
comment
Спасибо. Я просто пытался не изобретать велосипед. Все еще надеюсь, что кто-то предоставит решение в синглтонах Haskell, если оно существует. Какой смысл поднимать все эти функции на уровень типов, если вы не можете использовать их в доказательствах? - person NioBium; 10.07.2016
comment
Что ж, синглтоны — это (и singletons) один из способов использования GADT и типов данных. Проверочные термины, такие как Elem, являются другим. Они естественным образом не вписываются в структуру синглтона, потому что они не синглтоны! - person Benjamin Hodgson♦; 11.07.2016