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
