partial type signatures/annotations/declarations..

[Claus Reinke]

>    instead of introducing holes in types and contexts to leave
>    parts of a declaration unspecified, why not use type subsumption?

it has been pointed out to me that I should be more specific about 
what I mean with this suggestion (not least to ensure that I don't
suggest to use subsumption the wrong way round, thanks!-):

- first, subsumption: 

    (P => t) subsumes (Q => r) 
    iff 
    exists substitution th. (r = th(t) && th(P) |- Q)

    [where |- is entailment between sets of predicates]
 
    in words: a qualified type qt1 is subsumed by a qualified type qt2
    (we write: qt1 <= qt2) precisely if qt1 is a substitution instance of 
    qt2 whose constraints are implied by the substition instance of qt2's 
    constraints.    

- next, its use for partial type declarations:

    a qualified type is subsumed if its type part is more specific, and its
    constraint part is implied. so we could declare a qualified type for an 
    expression that, instead of being the precise type of said expression,
    only has to be subsumed by the inferred expression type:

    we write (expr :<: qt_partial) iff: (expr :: qt) and (qt_partial <= qt).

    that means that the precise type can be more specific (variables
    instantiated), have more constraints (as long as the ones given are
    implied) and even different constraints (eg., of subclasses, or of
    other constraints that imply the ones given). this accounts for uses
    of placeholders (_) in both types and constraints in the alternative
    option.

    note that, currently, declarations can already be more specific than 
    the inferred type:

        f :: Int -> Int -> Int
        f x y = x+y
    
    partial type declarations would permit us to declare types that are
    more general than the inferred type, allowing us to omit type info
    that we want to leave inferred (or specifying part of a type without
    having to specify all of it):

        f :<: Int -> a -> Int
    or
        f :<: Int -> a
    or
        f :<: Fractional a => a -> a -> a

    pro: would easily allow for omission of type details or parts
            of context (a type with more context, or with more specific
            type components, is subsumed by the declaration)
 
    cons: while this accounts for the explicit parts of the alternative
            option (_), that option implicitly assumes that other type
            variables cannot be instantiated, and that contexts without
            _ cannot be extended.

            as long as we only specify an one-sided bound, the inferred
            type could be more specific than we'd like (we can't say
            that we don't want context, or that some type variable
            must not be instantiated)

hope I got it the right way round this time?
claus

ps. I can't find the original thread, but this came up again last
     year, and Oleg suggested, that for the special case of function
    signatures, the same effect could be had by adding extra fake
    clauses (similar to fake clauses commonly used for trace or seq):

    http://haskell.org/pipermail/haskell-cafe/2004-August/006606.html

    this does not work for other places where type declarations
    are required, but would be awkward or impossible to give in
    full, but at least for functions, Oleg's fake clauses might be a 
    possible desugaring (unless our clever optimising compiler
    removes them as dead code;-):

        -- f' :: Int -> a -> Int
        -- f' :: Int -> a
        -- f' :: Fractional a => a -> a -> a
        f' :: Eq a => c -> b -> a
        f' = undefined

        f x y | False = f' x y
        f x y = x+y