[Haskell-cafe] Re: type families and type signatures

[Tom Schrijvers]

> Hi Tom,
>
> It seems we are thinking of different things.  I was referring to
> the characterization of a type of the form P => t as being "ambiguous"
> if there is a type variable in P that is not determined by the
> variables in t; this condition is used in Haskell to establish
> coherence (i.e., to show that a program has a well-defined semantics).

[...]

> Technically, one could ignore the ambiguous type signature for
> bar, because the *principal* type of bar (as opposed to the
> *declared type*) is not ambiguous.  However, in practice, there
> is little reason to allow the definition of a function with an
> ambiguous type because such functions cannot be used in practice:
> the ambiguity that is introduced in the type of bar will propagate
> to any other function that calls it, either directly or indirectly.
> For this reason, it makes sense to report the ambiguity at the
> point where bar is defined, instead of deferring that error to
> places where it is used, like the definition of bar'.  (The latter
> is what I mean by "delayed" ambiguity checking.)

Thanks for explaining the ambiguity issue, Mark. I wasn't thinking about 
that. We have thought about ambiguity. See Section 7.3 in our paper

http://www.cs.kuleuven.be/~toms/Research/papers/draft_type_functions_2008.pdf

Note that neither Definition 3 nor Definition 4 demands that all 
unification variables are substituted with ground types during type 
checking. So we do allow for a form of ambiguity: when any type is valid 
(this has no impact on the semantics). Consider the initial program

 	type family F a

 	foo :: F a -> F a
 	foo = id

You propose to reject function Foo because it cannot be used 
unambiguously. We propose to accept foo, because the program could be 
extended with

 	type instance F x = Int

and, for instance, this would be valid:

 	foo2 :: F Char -> F Bool
 	foo2 = foo

If you look at the level of the equality constraints:

 	(F Char -> F Bool) ~ (F alpha -> F alpha)

we normalise first wrt the instance F x = Int, and get

 	(Int -> Int) ~ (Int -> Int)

which is trivially true. In this process we do not substitute alpha. So 
alpha is ambiguous, but any solution will do and not have an impact on 
program execution. GHC already did this before type functions, for this 
kind of ambiguity, it substitutes alpha for an arbitrary type. That's not 
unreasonable, is it?

Cheers,

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/