Я пытаюсь реализовать своего рода молнию для индексированных по длине списков, которые возвратят каждый элемент списка в паре со списком, в котором этот элемент будет удален. Например. для обычных списков:
zipper :: [a] -> [(a, [a])]
zipper = go [] where
go _ [] = []
go prev (x:xs) = (x, prev ++ xs) : go (prev ++ [x]) xs
Итак,
> zipper [1..5]
[(1,[2,3,4,5]), (2,[1,3,4,5]), (3,[1,2,4,5]), (4,[1,2,3,5]), (5,[1,2,3,4])]
Моя текущая попытка реализовать ту же самую вещь для индексированных по длине списков:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
data Nat = Zero | Succ Nat
type One = Succ Zero
type family (+) (a :: Nat) (b :: Nat) :: Nat
type instance (+) Zero n = n
type instance (+) (Succ n) m = Succ (n + m)
data List :: Nat -> * -> * where
Nil :: List Zero a
Cons :: a -> List size a -> List (Succ size) a
single :: a -> List One a
single a = Cons a Nil
cat :: List a i -> List b i -> List (a + b) i
cat Nil ys = ys
cat (Cons x xs) ys = Cons x (xs `cat` ys)
zipper :: List (Succ n) a -> List (Succ n) (a, List n a)
zipper = go Nil where
go :: (p + Zero) ~ p
=> List p a -> List (Succ q) a -> List (Succ q) (a, List (p + q) a)
go prev (Cons x Nil) = single (x, prev)
go prev (Cons x xs) = (x, prev `cat` xs) `Cons` go (prev `cat` single x) xs
Похоже, что это должно быть довольно просто, но, как представляется, нет никакого способа передать GHC, например, + является коммутативным и ассоциативным, или что нуль является тождественным, я сталкиваюсь с множеством проблем, когда средство проверки типов (понятно) жалуется, что не может определить, что a + b ~ b + a или a + Zero ~ a.
Нужно ли добавлять какие-то объекты-доказательства (data Refl a b where Refl :: Refl a a и др.) или есть ли способ сделать эту работу просто добавлением более явных сигнатур типа?
