[Haskell-cafe] Re: [Haskell] View patterns in GHC: Request for feedback

[apfelmus]

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