[Ur] Pattern Matching

[David Snider]

Let's say I rewrite that as:

fun zip a b =
   case (a, b) of
       (a :: as, b :: bs) => (a, b) :: zip as bs
     | _ => []

This throws a unification failure until I write:

fun blah () = (zip (1::[]) (2::[]))

At which point the compiler is able to infer the types and all compiles 
correctly

Is there some reason that the compiler can't/shouldn't default to:

fun zip [t] [t2] (a : list t) (b : list t2) : list (t * t2) =
   case (a, b) of
       (a :: as, b :: bs) => (a, b) :: zip as bs
     | _ => []

when unification isn't possible?

On 05/28/2013 09:26 AM, Adam Chlipala wrote:
> On 05/28/2013 06:15 AM, David Snider wrote:
>> In standard ML you can write
>>
>> fun zip _ _ = []
>>   | zip (a::as) (b::bs) = (a,b) :: (zip as bs)
>>
>> What would be the Ur equivalent of this kind of pattern matching?
>
> I'm assuming your code has a bug in the ordering of the patterns, 
> which I fix below.
>
> fun zip [t] (a : list t) (b : list t) : list (t * t) =
>   case (a, b) of
>       (a :: as, b :: bs) => (a, b) :: zip as bs
>     | _ => []
>
>
> _______________________________________________
> Ur mailing list
> Ur at impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur