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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe