partial type signatures/annotations/declarations..
Martin Sulzmann
sulzmann at comp.nus.edu.sg
Tue Mar 7 04:49:27 EST 2006
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
More information about the Haskell-prime
mailing list