I am trying to prove associativity of type-level lists in such a way that will allow me to convert between equivalent types without carrying around any constraints.
Assuming the standard definition of concatenation:
type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)
Suppose, I am given a function:
given :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy ((a ++ b) ++ c)
given = Proxy -- Proxy is just an example
and I would like to call this function and then use associativity:
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)’
This type equality is not trivial indeed, so it is not a surprise that the compiler doesn’t understand it, however I can prove it! Unfortunately, I don’t know how to convince the compiler that I can.
My natural first thought is to do something like:
proof :: forall k (a :: [k]) (b :: [k]) (c :: [k]). (a ++ (b ++ c)) :~: ((a ++ b) ++ c)
proof = _
and then change my function to:
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
But I still have to define proof
and for this I need to perform induction on its type arguments. The only way to do induction on types in Haskell that I know is to define a type class, but I then I will have to add the corresponding constraint to the type of my
, which I don’t want to do – the fact that it calls given
and coerces the result is an “implementation detail”.
Is there any way to prove this kind of type equality in Haskell without resorting to unsafe postulates?
No, you cannot prove this without a typeclass constraint, because it isn't true. In particular, here is a counterexample:
Any ++ ([] ++ []) -- reduces to Any ++ []
(Any ++ []) ++ [] -- does not reduce
To rule out the (stupid) existence of Any
, you must use a typeclass that does not have an Any
instance; no other choice.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With