[Haskell-cafe] Quantifying Partial Type Annotations

[Brandon Moore]

Philippa Cowderoy wrote:
> 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.
The intention is that the unknown variable might eventually get a 
concrete type, but you'd rather let the typechecker work it out?

I think in the language of the GHC typechecker you would say your 
quantifier introduces a "wobbly" type variable, rather than the "rigid" 
type variables of 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?
I discussed something similar a while ago, in connection with the 
discussions about alternate notation for class constraints, except I 
suggested copying the quantifier around with the synonym. This lets you 
write types like
type P a = some b . (b -> a, a)
or otherwise make a type synonym that asserts some part of your type is 
an instance of a certain scheme without fixing concrete types or 
requiring full parametricity.

More abstractly, type synonyms exist to name and reuse parts of type 
signatures. If you introduce partial type signatures, it seems fitting 
to extend type synonyms to naming and reusing part of partial type 
signatures as well.

> 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
Daan Leijen calls it "some".
It's implemented in Morrow, and described in his paper on existential 
types. He translates type annotations to type-restricting functions,
where

e :: forall a . T
becomes
(ann :: (forall a . T) -> (forall a . T)) e

and
e :: some a . T
becomes
(ann :: forall a . T -> T) e

Writing type signatures for things unpacked from existentials is another 
nice use for this quantifier. The some a. can unify with the skolem 
constant from the unpacking. One of his examples:

type Key a = { val :: a, key :: a -> Int }

absInt :: exists a. Key a
absInt = { val = 1, key i = i }

one1 = (\x -> x.key x.val) (head [absInt])
one2 = let x :: some a. Key a
x = absInt
in x.key x.val

Brandon