15 Nov
2016
15 Nov
'16
12:24 a.m.
On Mon, Nov 14, 2016 at 12:21 PM, David Feuer
I propose that we add the eliminator subst as a function:
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. 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) -- Live well, ~wren