Hi On Fri, 5 Apr 2002, Ashley Yakeley wrote:
> At 2002-04-04 05:57, C T McBride wrote: > > >> ...which would be very useful, but would probably have unpleasant > >> consequences for type inference... > > > >To my mind, this is not a credible objection. The horse has already > >bolted; there's no point in trying to shut the stable door. > > Perhaps I should say "type decidability". Currently Haskell can always > calculate whether one type-constructor is a substitution-instance of > another, and therefore whether two type-constructors are the same. This > may not be possible if you have full type lambdas, as in general there is > no way of calculating whether two functions are the same. That's fair enough, up to a point. Higher-order unification is undecidable, and does not in any case yield unique most general unifiers. It's inevitable that if there are more things we could possibly be saying, it's harder for the machine to guess which one we mean. My point, however, is that we should not restrict what we can say, just because machines have limitations. Instead, we should ensure that we who (hopefully) know what we mean, should be able to tell the machine. In this respect, it's reasonable to allow both `big lambda', abstracting over types and other higher kind things, and `big application' (absent, thus far, from the relevant proposals), allowing those abstracted parameters to be instantiated explicitly. That's what we do in dependent type theory (except that there's no distinction between big and little lambda), and proof assistants like Agda, Coq and Lego all have decidable typechecking, with much richer type systems than Haskell's. I have one foot on the platform and one on the train here: I'm currently implementing a dependently typed programming language in Haskell, and thinking about type system extensions for Haskell is an occupational hazard. The joy of Hindley-Milner is that you never have to write a big lambda or a big application, but it doesn't mean they aren't there. The machine inserts big lambdas via let-polymorphism and big applications via first-order unification. By careful restriction of the solutions available for higher-kind unknowns---only type constructors or polymorphic parameters---Haskell ekes out a little more automation. Not unreasonable. But instead of restricting the usage of big lambda and big application to only those which can be kept implicit, why not allow them optionally to be made explicit, and use the existing mechanisms to provide reasonable (but obviously not most general) defaults when this option is not exercised? Again, there's an established precedent for this in type theory. Pollack's `Implicit Syntax' has been around for ten years, and precisely allows you to indicate that an argument will by default be inferred (via unification, if possible) but can in any case be given explicitly. So, if we had, say, a monadically lifted fold operator mfoldr :: forall m. Monad m => forall a,b. (a -> b -> m b) -> m b -> [a] -> m b we could use this for Maybe, [], IO, etc as it stands, but we could also define foldr by something like foldr = mfoldr{Id} That's certainly cheaper, and much less frustrating than the `packaging' option newtype Id a = An a instance Monad Id ... A proposal which serves a different purpose but pushes in this general direction is Kahl and Scheffczyk's `Named Instances' idea. They're interested (rightly, in my opinion) in providing an explict but optional language of witnesses for the class constraints which appear in type schemes. Their proposal recognizes and does not interfere with the fact that, for many simple programs, there's an obvious default choice of instance which the machine can safely be left to fill in. However, they provide the means to specify an instance whenever a non-obvious behaviour is desired, or when (as is often the case with multi-parameter classes) there is no obvious behaviour anyway. It's a good idea, which I would like to see taken further. It seems to me desirable to seek a better integration of type-level programming via classes and the type-level nearly-programming which is made available by higher-kind polymorphism. I'm beginning to have some ideas about how this can be done---again based on existing technology in dependent type theory---but now's not the right time to push that particular boat out. So, let me summarize with two points: [Scientific] If we want to do wacky stuff, we should be under no illusion about preserving type inference (as opposed to type checking)---we must say what we mean. The maintenance of type inference is an untenable excuse for preventing us from saying what we mean. If we make big lambda and big application available but optional, we can keep the existing level of annotation in existing programs by using the existing inference engines as defaulting mechanisms. [Political] There is a great deal of work in type theory which is becoming more and more relevant to functional programming as the type systems used in the latter become richer. Similarly, type theorists are becoming more and more interested in programming. It's inevitable that as these communities drift closer in terms of what they study, more and more ideas from one will pop up in the other. We all need to read more. I know I do. Thanks to everyone who's said `read this' in response to my original message. Cheers Conor _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell