[Haskell-cafe] Wincomplete-uni-patterns and bidirectional patterns

[Olaf Klinke]

> For functions types, there is only one equivalence class, because
> there
> is only one way to pattern-match a function. Observe that two
> elements
> can be distinguished by a set of patterns if and only if there is one
> element in the pattern set that already distinguishes them. Do
> pattern
> synonyms refine the equivalence relation induced by ordinary
> constructors? No.

What I said is only true in the absence of view patterns. 
With view patterns, a pattern match is no longer guaranteed to
terminate, since the viewing function could diverge on the value being
matched. Consider

-- diverges on infinite lists
end :: [a] -> [a]
end xs = case tl xs of
    [] -> []
    (_:xs') -> end xs'

pattern Finite <- (end -> [])
isFinite :: [a] -> Bool
isFinite xs = case xs of
    Finite -> True
    _ -> False

Notice that isFinite is no longer a clopen but an open: It either
returns True or diverges. Moreover, view patterns introduce fine-
grained clopens on function spaces, like

pattern Q <- (($ 4) -> 3)

We must conclude that in the presence of the ViewPatterns extension,
the equivalenve relation induced by pattern matching is: 
"x~y whenever there is no function v and no pattern P such that (v x)
and (v y) can be distinguished by P." It should not be hard to prove
that deciding coverage by view patterns such as Finite would solve the
halting problem. 

Olaf