Dan Licata wrote:
apfelmus wrote:
The idea is to introduce a new language extension, namely the ability to pattern match a polymorphic type. For demonstration, let
class ViewInt a where view :: Integer -> a
instance ViewInt [Bool] where view n = ... -- binary representation
data Nat = Zero | Succ Nat
instance ViewInt Nat where view n = ... -- representation as peano number
be some views of the integers. Now, I'd like to be able to write
bar :: (forall a . ViewInt a => a) -> String bar Zero = ... bar (True:xs) = ...
This doesn't make sense to me:
Zero :: Nat
and therefore
Zero :: ViewInt Nat => Nat
but you can't generalize from that to
Zero :: forall a. ViewInt a => a
E.g., Zero does not have type ViewInt [Bool] => Bool
Yes, the types of the patterns don't unify. But each one is a specialization of the argument type. Note that the type signature is bar :: (forall a . ViewInt a => a) -> String which is very different from bar :: forall a . ViewInt a => a -> String Without the extension, we would write bar as follows bar :: (forall a . ViewInt a => a) -> String bar x = let xNat = x :: Nat in case xNat of Zero -> ... _ -> let xListBool = x :: [Bool] in case xListBool of True:xs -> ... In other words, we can specialize the polymorphic argument to each pattern type and each equation may match successfully.
Maybe you wanted an existential instead
No. That would indeed mean to pick the matching equation by analysing the packed type, i.e. some equations don't match since their patterns have the wrong type. I think that such a thing violates parametricity. Regards, apfelmus