Hi > There's nothing wrong with this in principle; the difficulty is that > when you say > > mantissa + 4 > > you aren't saying which float type to get the mantissa of. Earlier > messages have outlined workarounds, but in some ways the "real" solution > is to provide a syntax for type application. A polymorphic function > should be applied to a type argument; these type arguments are always > implicit in Haskell, but are explicit in System F.
You're quite right. I'd argue that instance derivations are also implicit arguments (they're a bit like elements of a datatype family). I'd further argue that it should never be compulsory to keep something implicit. It should always be possible to explain to the stupid machine exactly what you want. > If we could only figure out a good syntax for > (optional) type application, it would deal rather nicely with many of > these cases. Trouble is, '<..>' gets confused with comparisons. And > when there are multiple foralls, it's not obvious what order to supply > the type parameters. It's as obvious (or not) as remembering the order of arguments expected by any function, and in a dependently-typed language it's exactly that. My counsel would be to make Haskell's type-level programming language follow the functional idiom as much as is practicable. If you think of it as not so much extending Haskell's type system, but as grabbing for Haskell a bigger slice of a richer theory, the obvious question is `why stop now?'. Syntactically, it'd be prudent to ensure that what's chosen for this extension doesn't make the next extension uglier or more difficult. The approach we take to implicit syntax in Epigram is a small variation on Pollack's system from the early nineties. It goes like this (1) We have a postfix operator _ (pronounced `sub' for `subscript') which means `make the first argument explicit'; it also prefixes the variable in a quantifier to indicate that the argument is implicit by default; functions with implicit arguments are by default applied to unknowns e.g. nil : all _ x : * . List x so nil means nil applied to an unknown x nil _ means nil unapplied (thus still `polymorphic') nil _ X means nil explicitly applied to X (2) We have a symbol ? which means `I don't know or care what goes here', used to make the machine try to figure out an explicit argument. so nil _ ? also means nil applied to an unknown x By convention f ___ x is short for f _ ? _ ? _ x and so on, making it relatively easy to pick out specific arguments to make explicit. In Haskell, I suppose that type arguments in forall situations would be implicit by default, and type arguments to higher kind symbols would be explicit by default, so you probably don't need to mark up the binders at declaration time. However, I reckon the sub operator is a useful one. Note that it's not `type application' but rather `making polymorphism explicit', allowing the distinction between polymorphic objects and their instances to be made precisely, an issue kind of fudged in the current Haskell presentation of higher-rank polymorphism. Type application is a useful by-product. > It'd be useful in other situations too. For example, one could have > lambdas at the type level, if one was willing to instantiate them > explicitly. > sequence :: forall (m:*->*) (a:*). [m a] -> m [a] > data STB a s = s -> (a,s) -- Oops: got the > parameters backwards > > ....sequence<\b. ST b MyState, Int>... Quite so. This sort of thing happens all the time, e.g. when you have data Tree node leaf = Leaf leaf | Node (Tree node leaf) node (Tree node leaf) You might well want to fmap an operation across the node data, but oh dear it's not the last argument of the type constructor. You might also want to fmap across all the x's in a Tree (f x) (g x). It's no big deal to figure out the code for the fmap instance given the lambda abstraction. Even more useful is the construction of abstractions which just weren't there before. data Term = Var String | ... Suppose I forgot to make my representation polymorphic in variable names. (Or suppose I have too many interesting substructures to be able to abstract them all at once.) I should be able to express Term as something like (\ string . data Term = Var string | ... ) String -- categorists may read data Term = ... | ... as mu Term . ... + ... and still get fmap (renaming) built for me. Indeed that particular idiom could well be so handy that it deserves an even shorter syntax like (Term \\ String) As with any functional programming language, strength comes from the ability to express useful abstractions. The type level is no different to the term level in this respect. Cheers Conor _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell