partial type signatures/annotations/declarations..

[Martin Sulzmann]

FYI, Chameleon supports a combination of lexically scoped
and partial type annotation. The latest Chameleon version
is a broken (fix on its way). Though, besides the implementation
there's also a concise formal description. See
[July 2005] Lexically Scoped Type Annotations
http://www.comp.nus.edu.sg/~sulzmann/lexical-annot.ps

Martin

Claus Reinke writes:
 > >    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
 > 
 > _______________________________________________
 > Haskell-prime mailing list
 > Haskell-prime at haskell.org
 > http://haskell.org/mailman/listinfo/haskell-prime