the nearly dependent near future, was Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde

[Conor McBride]

Hi Dan

On 14 Mar 2009, at 18:48, Dan Doel wrote:

> On Saturday 14 March 2009 1:07:01 pm Conor McBride wrote:
>>  I don't think the duplicate-or-plunge dilemma you
>> pose exhausts the options. At least, I seem no reason to presume
>> so and I look forward to finding out!
>
> I didn't mean to suggest that ATS is the best you can do. Merely  
> that you can
> still get a lot done without going very far beyond what is technically
> possible (though not enjoyable) in GHC today (to the point that  
> people will
> actually categorize your language as "dependently typed" when it  
> merely has a
> type language comparable in richness and convenience to the value  
> level, but
> is still mostly separate).

I'd certainly agree with that assessment.

[..]

> If you can do better than ATS, and have value-level stuff  
> automatically
> reproduced at the type level and suchlike, so much the better. I  
> fully support
> that. :)

Good! 'Cos that's what I'm going for. It certainly won't involve types
depending on arbitrary expressions -- or even on run-time data in the
first instance -- but by taking the approach of lifting what we can
from types to kinds and from values to types, we keep those options
open, as well as hiding the cruft.

Note: subject about to slide into something a tad more technical, but
I gotta tell you this one...

To echo your remarks above, I'm pretty sure one could go quite far even
with something as non-invasive as a GHC preprocessor. My opening gambit
would be to extend the grammar of kinds as follows, with a translation
(#) back to current kinds:

   kind ::= *                             #*                  = *
          | kind -> kind                  #(j -> k)           = #j -> #k
          | {type}                        #{t}                = *
          | forall x :: kind. kind        #(forall x :: j. k) = #k

Note that this forall abstracts type-level stuff in a given kind, not
kinds themselves, so the bound variable can only occur inside the {..}
used to lift types up to kinds. Correspondingly, when we smash the {t}
kinds all to *, we can dump the polymorphism.

Now populate the {t} kinds by lifting expressions to the type level:
these look like {e} where e :: t is built from fully applied
constructors and variables. That's certainly a total fragment!
The preprocessor will need to cook up the usual bunch of gratuitous
type constructors, one for each data constructor used inside {..} in
order to translate expressions to types. It will need to perform
tighter checks on class and data declarations (ideally by constructing
objects one level down which express an equivalent typing problem)
but GHC already has the necessary functionality to check programs.

It might be possible to cut down on the amount of {..} you need to
festoon your code with. On the other hand, it might be good to delimit
changes of level clearly, especially given existing namespace policies.

It's not much but it's a start, it's super-cheap, and it's compatible
with a much more sophisticated future. I program in this language
already, then I comment out the kinds and types I want and insert
their translations by hand. At the moment, I have to write types like

   data Case :: ({a} -> *) -> ({b} -> *) -> {Either a b} -> * where
     InL :: f {a} -> Case f g {Left a}
     InR :: g {b} -> Case f g {Right b}

rather than programs like, er... "either". But perhaps we could
also figure out how to translate "either" to a type function.

However, the numeric constraints project will need more than a
preprocessor, because it delivers specific new constraint-solving
functionality during type inference, rather than just the precooking
of first-order value unification problems as first-order type
unification problems. Indeed, with rank-n types, it could be quite
fun.

I'm sure there are devils yet in details, but the prospects for
not-quite-dependent types by re-use rather than hard labour look
quite good, and forwards-compatible with yer actual dependent
functions, etc, further down the line.

We live in interesting times!

All the best

Conor