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