deriving over renamed types

[C T McBride]

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