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 > [email protected] > http://haskell.org/mailman/listinfo/haskell-prime _______________________________________________ Haskell-prime mailing list [email protected] http://haskell.org/mailman/listinfo/haskell-prime
