[Haskell-cafe] Pattern matching does not work like this?
haberg at math.su.se
Wed Jul 15 08:30:50 EDT 2009
On 15 Jul 2009, at 13:22, Luke Palmer wrote:
> If ++ could be pattern matched, what should have been the result of
> "let (x++y)=[1,2,3] in (x,y)"?
> It will branch. In terms of unification, you get a list of
> f :: [a] -> ([a],[a])
> f (x ++ y) = (x,y)
For an argument s, any pair (x, y) satisfying s = x ++ y will match.
That is, if s = [s_1, ..., s_k], the solutions j = 0, ..., k, x =
[s_1, ..., s_j], y = [s_(j+1), ..., s_k]. And for each one, a
potentially different value could given. That is, s could produce
> If this pattern branches, it could hardly be considered a function
> which takes lists and returns pairs. It would have to return
> something else.
So this would be a multi-valued function, which sometime is useful as
a concept. But if the choices are indexed, they can be reduced to a
single valued function. Like g(x,y) with the requirement that if x ++
y = x' ++ y', then g(x, y) = g(x', y').
This branching is what would happen if one tries to make a type theory
based on sets. (It is possible to implement Horn clauses as
unification branching.) The selection of branches correspond to a
choice in the proof tree.
More information about the Haskell-Cafe