[Haskell-cafe] Quantifying Partial Type Annotations

[Philippa Cowderoy]

I've done a bit more thinking about partial type annotations (as proposed 
on the Haskell' list), and I have a somewhat more concrete proposals for 
some of the extensions to them that perhaps also makes more sense of the 
original basic idea as well. I'm sending it to the Cafe this time as it's 
a bit early to consider this for standardisation.

I'd like to propose a new quantifier for type variables, which for now 
I'll call unknown[1] - correspondingly I'll talk about "unknown-quantified 
variables" and probably "unknown variables" where it's not ambiguous. 

Unknown quantifiers will never be introduced by the typechecker without a 
corresponding annotation - only propagated inwards. Whereas universal type 
variables must not accumulate additional constraints during typechecking 
(and in a traditional Hindley-Milner implementation only become 
universally quantified during a generalisation step), unknown type 
variables can - indeed this is their raison d'etre. Furthermore, they are 
never propagated 'outwards' - either the variable is constrained 
sufficiently that it can be replaced with a monotype or, having otherwise 
finished typechecking the corresponding term, the unknown quantifier is 
replaced with a forall.

For example:

add' :: unknown x. x -> x -> x
add' = (+)

add'' :: unknown x. x -> x -> x
add'' x y = (x::Int) + (y::Int)

will typecheck, resulting in these types when the identifiers are used:

add' :: forall x. Num x => x -> x -> x
add'' :: Int -> Int -> Int

It's probably also sensible to allow "wildcard" variables written _, 
generated fresh and implicitly unknown-quantified much as universal 
variables are now.

Type synonyms seem to present an interesting question though - it seems to 
me most sensible to hang on to the quantification at top-level and 
generalise it only as we finish type-checking a module, rather than 
copying out the quantifier anew each time. Any comments?

The amount of thinking I've done about interactions with rank-n variables 
is limited - I guess we'd need to prohibit unifying with type variables 
that're of smaller scope than the unknown variable? I'm don't think I can 
see any other worrying issues there.

Unknown variables in method declarations seem... meaningless to me, 
they're not proper existentials and I don't think there's a sane meaning 
for them that isn't a kludge for associated types instead. I don't think 
they belong in instances for similar reasons.

Incidentally, I think there's also a cute use case in .hs-boot files, 
where an unknown-quantified variable could be used to tie some knots in a 
manner similar to the way recursive bindings are checked now. If so, I 
have an interesting use for this.

[1] Other names that have occurred to me are "solve" (as in "solve for 
x"), and "meta" (by analogy to metavariables in the typechecker - because 
by the time we've finished checking the annotated term we'll have removed 
the quantifier), but unknown seems by far the strongest to me. No doubt 
someone'll suggest a far better name shortly after I post this!

-- 
flippa at flippac.org

There is no magic bullet. There are, however, plenty of bullets that 
magically home in on feet when not used in exactly the right circumstances.