On Nov 15, 2016 12:24 AM, "wren romano"
subst :: a :~: b -> f a -> f b subst Refl x = x
I'm all for adding this function, but do note that the type is suboptimal since GHC lacks general functions (and higher-order pattern matching) at the type level. Which means we'll actually end up wanting a family of different "subst" functions to cover all the (relevant) cases the definition above would cover in a language like Agda, Coq, etc.
Yes, we will, but those can be written using `subst` and one or more auxiliary types without additional "primitive" eliminators (see below).
E.g.,
Prelude> let x :: Either Bool Int; x = Right 42
Prelude> :t (`subst` x) (`subst` x) :: Int :~: b -> Either Bool b
When I might've really wanted/meant (Bool :~: b -> Either b Int)
We can write newtype Flip f x y = Flip { unFlip :: f y x } subst2 :: a :~: b -> f a x -> f b x subst2 eq = unFlip . subst eq . Flip The subst2 function will work on the left side of Either.