deriving over renamed types

[C T McBride]

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