Hi all, > At 2002-04-03 15:14, Hal Daume III wrote:
> >> type FM = FiniteMap > >> type FM a b = FiniteMap a b > > > >I wasn't aware there was (supposed to be) a difference > >between these two declarations? Is there? On Wed, 3 Apr 2002, Ashley Yakeley wrote: > type FM a b = FiniteMap a b > > ...This defines FM as a pseudo-type-constructor. It has no kind, but must > be specified with two arguments each of kind (*) so as to become a > type-constructor (a type) of kind (*). In effect, type synonyms introduce a macro facility, but because they must be fully applied, they introduce no new normal forms for types. This makes things simpler from one point of view, but simplicity is subjective. Here, we trade simplicity of comprehension (for the machine) for simplicity of composition (for us). I don't think we've landed the best deal. > Unfortunately Haskell does not have lambda over types, otherwise the two > could be the same. And then one could do things such as > > type M b a = a -> b; > instance Cofunctor (M b) where ... Yes, please! More, please! type Id a = a type Comp f g x = f (g x) instance Monad Id where return = id a >>= f = f a instance (Functor f,Functor g) => Functor (f `Comp` g) where fmap = fmap . fmap In particular, if Id were a Monad, we could adopt the useful habit of writing monadically lifted combinators (fold operators, etc), from which the unlifted versions could be readily recovered. > ...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. The existing post-Hindley-Milner aspects of Haskell's type system are too useful for type inference to be worthy of such veneration. [warning: drum-thumping Ulsterman on soap box] (*) Two points in this regard Pragmatically, there is no reason why extensions of the type system which break type inference should preclude the use of type inference for `old' programs which sit within the sublanguage where inference remains possible. If the machine is smart enough to figure out a program's type, by all means let it. But if not, we must be able to say what me mean. This is already the Haskell approach: we can and should take it further. Design remains important. The division of labour between humans and machines should be as clear as possible---we should be able to tell which parts of the program we must write, and which the machine can construct automatically. `Macbeth programming' (throwing miscellaneous rats, bats and insects into the cauldron until the magic happens) must be avoided. Dogmatically, type inference is in any case a bad rationalization of how it is that a program comes to have a type. In a strongly typed language, types define the spaces where programs are found, not the other way around! If we don't have at least some idea what the type is, we have no business writing the program. We should always be willing to write type signatures. (*) Further analysis The trouble, as things stand, is that we don't get any payoff for writing type signatures, other than the machine's grudging acceptance of our weirder programs, and a vague sensation of puritan worthiness. Explicit or not, we are forced to maintain the type discipline in our heads as we code. Typechecking is _summative_: the typechecker is a policeman who shows up at the end of the process and thumps us if we've got it wrong. Whilst the standard undergraduate cry of `Nasty typechecker won't let my program work!' is misguided (I typically respond `What program?'), it is at least understandable given that the typechecker plays no _formative_ role in the construction of programs which _do_ work. Type-directed editing (as opposed to mere syntax-directed editing) is a way to extract benefit from the work we put into writing a type signature. A choice of type has consequences for the choice of program, and we can use the machine to propagate those consequences, where current practice requires us to engineer coincidences between types and programs. In effect, the production of non-criminal code can benefit from parenting as well as policing. Rebellious teenagers will doubtless persist in loitering on street corners, writing their programs with a spraycan. This crime is its own punishment. As I've argued before, the need for type-directed editing, as pioneered in proof assistants based on dependent type theory, arises even without dependent types. The currently implemented extensions to Haskell's type system already introduce enough computation at the type level to make self-imposed type discipline a major headache. Polymorphic recursion requires care; multi-parameter type classes require serious dedication. It doesn't take a genius to see that things are getting out of hand, although it may take a non-genius to see the need for help. (*) You can probably tell where I'm going with this Returning whence this started, I think it's a very good idea to upgrade from type synonyms to type-level functional programs, given the right typechecking support. For much the same reasons that I prefer Haskell to Prolog at the term level (clearer operational semantics, better support for higher-order programming, etc), I'd like to write type-level programs functionally, rather than via Horn clauses in instance declarations. In this setting, it also makes sense to add type-level data (`datakinds', as it were). One might write datakind Nat = Zero | Suc Nat type Vector :: Nat -> * -> * Vector Zero a = () Vector (Suc n) a = (a,Vector n a) type Matrix :: Nat -> Nat -> * -> * Matrix m n a = Vector m (Vector n a) and so on. Inductively defined datakinds offer a more tightly analysed presentation of generic operators than full-on pattern-matching over *. They also offer a much simpler and more powerful means to impose invariants on data structures than coding with nested types. Going further, inductively defined relations on types might well deliver much of the useful functionality for which we currently need multi-parameter classes, with the bonus of a ready-made language of instances which could be supplied explicitly wherever inference is inadequate. I can imagine that some might react `that's too much like dependent types' whilst others might complain `that's not enough like dependent types'. To the former, I'd suggest that Haskell already supports too many clumsy fakes of fairly elementary dependent types (via type classes, nested types, etc) and that adding a better fake might help tidy things up. Naturally, I have more sympathy with the latter position, but I'm trying to be prudent with its purpose. What happens if we just remove the distinction between type- and term-level programs, perhaps taking * :: *? Term-level programs can do bad things like fail to terminate (but so can type-class programs) or fail to match (but so can generic programs), so why not go all the way? From an implementation perspective, I'd argue that removing the distinction between Haskell's static and dynamic languages would be an interesting area of study, but not exactly achievable by evolution. From a more principled perspective, I'd argue that the existing bad static behaviour is no excuse for worse. The point of treating type-level programming as programming is to _improve_ static behaviour: the static language should resemble the dynamic language, but without the criminal tendencies. Looking to the future, dependent types offer a revolutionary change in functional programming. I believe this revolution is both necessary and inevitable. I also believe it can be bloodless, even joyous. I hope that Haskell will begin to step cautiously, but consciously, in that direction. Turning `type' declarations from macros to programs would be a good first move. It's long past time to accept that we've outgrown type inference. I'll stop thumping my drum now. Conor _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell