deriving over renamed types

[Lennart Augustsson]

I just just wanted to say that I agree with almost everything Conor said.
I find it a little odd that the extension to Haskell that allows explicit
forall
does not also allow you use explicit type application (and type lanbda).

    -- Lennart

C T McBride wrote:

> 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
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell