Language extension proposal

[C T McBride]

Hi

> There's nothing wrong with this in principle; the difficulty is that
> when you say
>
> 	mantissa + 4
>
> you aren't saying which float type to get the mantissa of.  Earlier
> messages have outlined workarounds, but in some ways the "real" solution
> is to provide a syntax for type application.  A polymorphic function
> should be applied to a type argument; these type arguments are always
> implicit in Haskell, but are explicit in System F.

You're quite right. I'd argue that instance derivations are also implicit
arguments (they're a bit like elements of a datatype family). I'd further
argue that it should never be compulsory to keep something implicit. It
should always be possible to explain to the stupid machine exactly what
you want.

> If we could only figure out a good syntax for
> (optional) type application, it would deal rather nicely with many of
> these cases.  Trouble is, '<..>' gets confused with comparisons.  And
> when there are multiple foralls, it's not obvious what order to supply
> the type parameters.

It's as obvious (or not) as remembering the order of arguments expected by
any function, and in a dependently-typed language it's exactly that. My
counsel would be to make Haskell's type-level programming language follow
the functional idiom as much as is practicable. If you think of it as not
so much extending Haskell's type system, but as grabbing for Haskell a
bigger slice of a richer theory, the obvious question is `why stop now?'.
Syntactically, it'd be prudent to ensure that what's chosen for this
extension doesn't make the next extension uglier or more difficult.

The approach we take to implicit syntax in Epigram is a small variation
on Pollack's system from the early nineties. It goes like this

(1) We have a postfix operator _ (pronounced `sub' for `subscript') which
      means `make the first argument explicit'; it also prefixes the
      variable in a quantifier to indicate that the argument is implicit
      by default; functions with implicit arguments are by default
      applied to unknowns

      e.g.  nil  :  all _ x : * . List x

      so    nil      means  nil applied to an unknown x
            nil _    means  nil unapplied (thus still `polymorphic')
            nil _ X  means  nil explicitly applied to X

(2) We have a symbol ? which means `I don't know or care what goes here',
      used to make the machine try to figure out an explicit argument.

      so   nil _ ?  also means  nil applied to an unknown x

      By convention  f ___ x  is short for  f _ ? _ ? _ x  and so on,
      making it relatively easy to pick out specific arguments to make
      explicit.

In Haskell, I suppose that type arguments in forall situations would be
implicit by default, and type arguments to higher kind symbols would be
explicit by default, so you probably don't need to mark up the binders at
declaration time. However, I reckon the sub operator is a useful one. Note
that it's not `type application' but rather `making polymorphism
explicit', allowing the distinction between polymorphic objects and their
instances to be made precisely, an issue kind of fudged in the current
Haskell presentation of higher-rank polymorphism. Type application is a
useful by-product.

> It'd be useful in other situations too.  For example, one could have
> lambdas at the type level, if one was willing to instantiate them
> explicitly.
> 	sequence :: forall (m:*->*) (a:*).  [m a] -> m [a]
> 	data STB a s = s -> (a,s)		-- Oops: got the
> parameters backwards
>
> 	....sequence<\b. ST b MyState, Int>...

Quite so. This sort of thing happens all the time, e.g. when you have

  data Tree node leaf
     = Leaf leaf
     | Node (Tree node leaf) node (Tree node leaf)

You might well want to fmap an operation across the node data, but oh dear
it's not the last argument of the type constructor. You might also want
to fmap across all the x's in a Tree (f x) (g x). It's no big deal to
figure out the code for the fmap instance given the lambda abstraction.

Even more useful is the construction of abstractions which just weren't
there before.

  data Term = Var String | ...

Suppose I forgot to make my representation polymorphic in variable names.
(Or suppose I have too many interesting substructures to be able to
abstract them all at once.) I should be able to express Term as something
like

 (\ string . data Term = Var string | ... ) String
   -- categorists may read data Term = ... | ... as mu Term . ... + ...

and still get fmap (renaming) built for me. Indeed that particular idiom
could well be so handy that it deserves an even shorter syntax like

 (Term \\ String)

As with any functional programming language, strength comes from the
ability to express useful abstractions. The type level is no different
to the term level in this respect.

Cheers

Conor