>Koen Claessen wrote:
>> We should allow "partial type specification". The programmer is
>> allowed to specify as much information about the type as (s)he wants.
>>
>> The partial type specification would be taken as a "skeleton",
>> merely filled in by the type inference algorithm.
>> foo :: (..) => a -> (..) -> (..)
>> foo :: (..) => (..)
>>
>> So, we are allowed to use (..) at any place in the context (or maybe
>> even type), to show the compiler that you know "something" should be
>> there.
Frank A. Christoph wrote:
>I like the idea, but I was surprised about the syntax. I was expecting
>something like this:
>
> foo :: (?c1, ?c2) => a -> b -> c
> bar :: (Bar a) => a -> ?t -> ?t -> ?s
>
The advantage of this syntax is that you can indicate that two parts of a
>type should be identical. Think of it as "metaquantification," and the
>binder is invisible, like in Haskell's usual syntax for type variables.
Just as Frank, I had a feeling of deja vu when reading Koen's message
but was surprised by the proposed syntax (the same goes for Frank's
message, though:-). I, too, find myself wanting to give partial type
annotations sometimes, refining them with more information only when
necessary (to avoid overspecification during program evolution).
To me, the problem is simply that type annotations are taken to be
exact specifications, ignoring the partial orderings provided by
the theory. So, if I write
foo :: C a => a -> b
when the inferred type happens to be
foo :: C [c] => [c] -> d -> e
the system complains. And rightly so, because what I wanted to write was
a partial specification, which I would want to write as
foo :<= C a => a -> b
Read e :<= t as "the type of e should be bounded by t". Choose a better
symbol if you like -- the idea is to keep the syntax of types unchanged,
and to introduce a language-level symbol for the existing partial
ordering of constrained type schemes instead.
Wouldn't this be simpler than introducing new concepts such as type
"skeletons" or "metaquantifications"?
Claus
