Я пытаюсь доказать ассоциативность списков на уровне типов таким образом, чтобы я мог выполнять преобразование между эквивалентными типами без каких-либо ограничений.
Принимая стандартное определение конкатенации:
type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)
Предположим, у меня есть функция:
given :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy ((a ++ b) ++ c)
given = Proxy -- Proxy is just an example
, и я хотел бы вызвать эту функцию и затем использовать ассоциативность:
my :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy (a ++ (b ++ c))
my = given @k @a @b @c -- Couldn't match type ‘(a ++ b) ++ c’ with ‘a ++ (b ++ c)’
Это равенство типов не является тривиальным действительно, поэтому неудивительно, что компилятор этого не понимает, однако я могу это доказать! К сожалению, я не знаю, как убедить компилятор, что я могу.
Моя первая естественная мысль - сделать что-то вроде:
proof :: forall k (a :: [k]) (b :: [k]) (c :: [k]). (a ++ (b ++ c)) :~: ((a ++ b) ++ c)
proof = _
и затем изменить мою функцию на:
my :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy (a ++ (b ++ c))
my = case proof @k @a @b @c of Refl -> given @k @a @b @c
Но я все еще должен определить proof, и для этого мне нужно выполнить индукцию для аргументов его типа. Единственный способ индукции для типов в Haskell, который я знаю, это определить класс типов, но тогда мне придется добавить соответствующее ограничение к типу my, что я не хочу делать - тот факт, что он вызывает given и приводит к результату, является «деталью реализации».
Есть ли способ доказать равенство типов в Haskell без обращения к небезопасным постулатам?