[Haskell-cafe] Re: how to write a list builder? fixpoint?

[oleg at pobox.com]

> class BuildList a r  | r-> a where
>     build' :: [a] -> a -> r
>
> instance BuildList a [a] where
>     build' l x = reverse$ x:l
>
> instance BuildList a r => BuildList a (a->r) where
>     build' l x y = build' (x:l) y

> So they key here appears to be that the type-checker can distinguish 
> between function application and other uses of an expression?

I'm sorry I'm late with the reply.

Indeed, the trick is straightforward -- merely basic
typechecking. Indeed, let us consider an expression

	build' [] 'a' 'b' ++ []

or, in a more abstract syntax

	(++) ((build' [] 'a') 'b') []

We make use of the familiar typing rule

G |- e1: t1->t2    G |- e2: t1  <===> G |- (e1 e2) : t2

where G is the typing environment (which associates types with the variables
that appear free in expressions e1 and e2). The typing rule can be applied
in either direction.

Operator (++) has the type [t1] -> [t1] -> [t1]. Given that fact and
applying the typing rule twice, we infer that ((build' [] 'a') 'b')
has the type [t1], [] has the type [t1], and so the whole expression
has the type [t1]. We have inferred that
	((build' [] 'a') 'b') :: [t1]
Applying the rule in reverse direction, we find that
	(build' [] 'a'):: t3->[t1]   'b':: t3
Or, because 'b' has the type Char, t3 unifies with Char, which gives
us
	(build' [] 'a') :: Char->[t1]

Applying the typing rule several more times, we find
	[]:: t4
	'a' :: t5
	build':: t4 -> t5 -> (Char->[t1])
or
	[]::t4
	build' :: t4 -> Char -> (Char->[t1])

>From the declaration of the BuildList class, we know that 
	build' :: [a] -> a -> r
unifying the two signatures, we find
	build' :: [Char] -> Char -> (Char->[t1])

Of the two instances of BuildList, the second obviously matches.
The functional dependency r->a essentially tells us that 'r' is the
primary key in the instance selection. That is, if we use (Char->[t1])
to match with the second parameter of the instance and found the
matching instance, we can be sure that it is the only matching instance
-- no matter how many instances are added in the future or contained
in other modules. So, we commit to the second instance and 
assign the type to build' in the original expression as
	build'_2 :: [Char] -> Char -> (Char->[t1])

However, the second instance of BuildList includes the term
"build' (x:l) y", and we have to type in turn. We know that
	(x:l)::[Char]
	(build' (x:l) y)::[t1]
from which we determine, with the same typing rule,
	build'::[Char] -> t6 -> [t1]
or, unifying with the signature for build',
	build'::[Char] -> Char -> [t1]
Again, we search for the appropriate instance of BuildList. Now, the
first instance matches. Again, we can commit to it. Unifying 
'a' with Char and [t1] with [a] gives us
	build'_1 :: [Char] -> Char -> [Char]

and the type of the whole (++) expression as [Char]. Typechecking succeeds,
and we were able to unambiguously choose instances.

The details of the actual typechecking algorithm most likely differ,
yet the general idea -- and the outcome -- are the same.