Niklas Broberg n_broberg at hotmail.com
Sat May 15 17:42:03 EDT 2004

```>What about
>
>foo [/ (/ 2 (/ a _ /)* 3 /)* /] = a
>
>?  What is the type of a here?  I think it should be [[Int]].

Not quite, the type of a will be [Int].
The only context dependency of variable types is the difference between
linear and non-linear contexts. In linear context, variables have the types
you would normally expect in standard Haskell. In non-linear context, the
type is a list of what it would otherwise be, regardless of what and how
many enclosing non-linear regular pattern operators.

If you want a full trace of where the items in a come from, you need to do
it in several steps:

foo [/ (/ 2 b@:(/ _ _ /)* 3 /)* /] = map (map bar) b  -- here b :: [[[Int]]]
where bar [a, _] = a

The reason for b having type [[[Int]]] is that it binds to a pattern of type
[[Int]] (a repeating * enclosing a sequence).

In general: binding explicitly preserves the trace of the pattern it binds
to; binding implicitly preserves no trace at all. To see why this is so,
consider the following analogy:

bar :: Maybe (Maybe (Maybe Int)) -> (Maybe (Maybe Int), Maybe Int, Int)
bar (Just a@(Just b@(Just c))) = (a,b,c)

When binding a , you look at the type of the subpattern it binds to. When
looking at the value held by a on the right hand side, there is no way to
trace the context it appeared in before the pattern match.
When binding c, you also look at the subpattern it binds to, i.e. the
pattern c is equivalent to the pattern c at _. There is no trace of where it
comes from.
Now look at this regular pattern:

foo [/ a@:(/ _ b@:(/ _ c /) /) /] = (a,b,c)

What is the type of foo?
Well, the type of c is whatever it binds to, which is just an element of the
list (assuming Int). But since it is bound in non-linear context, its type
will be [Int]. This form of context dependence is the only one we ever need
to consider, where a variable is bound implicitly. And the only question is,
does it have a list type or not? Another way to look at it is to see that c
is equivalent to c@:_ in non-linear context and c at _ in linear context.
b is bound explicitly using the @: operator, so the type of b is a list of
whatever it binds to. No context dependence. What it binds to is a a
sequence, i.e. a list, so the type of b will be [[Int]].
a is bound explicitly using the @: operator, so the type of a is a list of
what it binds to. No context dependece here either. It too binds to a list,
so its type will be [[Int]].
Thus,

foo :: ([[Int]], [[Int]], [Int])

>And then which special syntax for implicit binding am I supposed to use?
>Is it
>
>foo [/ (/ 2 (/ a@:(/_ _/) _ /)* 3 /)* /] = a
>
>or maybe
>
>foo [/ (/ 2 (/ a@::(/_ _/) _ /)* 3 /)* /] = a

The former. We have added the @: operator as a a non-linear counterpart of
the linear @. Adding more : won't add more levels of lists...

>? And what's the type?  [[[Int]]]?

Not quite right here either, the type will be [[Int]]. The first enclosing
list comes from the fact that the subsequence (/ ... /) has type list
(whatever will be matched against it is a sequence of items), and the second
enclosing list comes from the use of the non-linear binding operator @:.

Hopefully I make sense (more than before?).
I'm starting to think maybe our context dependent approach to implicit
bindings isn't very good after all since it seems to confuse a lot of
people. Perhaps variables bound inside regular patterns should always be
non-linear... of course that would still be context dependent when compared
to normal Haskell patterns, but perhaps still less confusing?

Anyway, thanks for the interest and the comments =)

/Niklas

_________________________________________________________________
The new MSN 8: advanced junk mail protection and 2 months FREE*
http://join.msn.com/?page=features/junkmail

```