[Haskell-cafe] Microsoft PhD Scholarship at Strathclyde

[Conor McBride]

Hi Dan

On 14 Mar 2009, at 14:26, Dan Doel wrote:

> On Saturday 14 March 2009 8:12:09 am Conor McBride wrote:
>> Rome wasn't burnt in a day.
>>
>> Of course I want more than just numerical indexing (and I even
>> have a plan) but numeric constraints are so useful and have
>> so much of their own peculiar structure that they're worth
>> studying in their own right, even for languages which do have
>> full dependent types, let alone Haskell. We'll carry out this
>> project with an eye to the future, to make sure it's compatible
>> with full dependent types.
>
> One should note that ATS, which has recently been generating some  
> excitement,
> doesn't have "full" dependent types, depending on what exactly you  
> mean by
> that.

I'm really impressed by the results ATS is getting, and by DML
before it. I think these systems do a great job of showing
what can be gained in performance by improving precision.

>
> For instance, it's dependent typing for integers consist of:

I certainly want

>
>  1) A simply typed static/type-level integer type

which looks exactly like the value-level integers and has a
helpful but not exhaustive selection of the same operations.

But this...

>  2) A family of singleton types int(n) parameterized by the static  
> type.
>     For instance, int(5) is the type that contains only the run-time  
> value 5.
>  3) An existential around the above family for representing arbitrary
>     integers.

...I like less.

> where, presumably, inspecting a value of the singleton family  
> informs the type
> system in some way. But, we can already do this in GHC (I'll do  
> naturals):
>
>  -- datakind nat = Z | S nat
>  data Z
>  data S n
>
>  -- family linking static and dynamic
>  data NatFam :: * -> * where
>    Z :: NatFam Z
>    S :: NatFam n -> NatFam (S n)
>
>  -- existential wrapper
>  data Nat where
>    N :: forall n. NatFam n -> Nat
>
> Of course, ATS' are built-in, and faster, and the type-level  
> programming is
> probably easier, but as far as dependent typing goes, GHC is already  
> close (I
> don't think you'd ever see the above scheme in something like Agda  
> or Coq with
> 'real' dependent types).

Which is why I'd rather not have to do that in Haskell either. It
really hurts to go through this rigmarole to make this weird version
of Nat. I'd much rather figure out how to re-use the existing
datatype Nat. Also, where the GADT coding really doesn't compete
with ATS is in dealing with constraints on indices that go beyond
unification -- numbers have more structure and deserve special
attention. Numerical indexing systems need to carry a big stick for
"boring algebra" if we're to gain the power but keep the weight down.

But wherever possible, I'd prefer to avoid doing things an awkward
way, just because we don't quite have dependent types. If the above
kludge is really necessary, then it should at least be machine-
generated behind the scenes from ordinary Nat. I'd much rather be
able to lift a type to a kind than have a separate datakind feature.
Apart from anything else, when you get around to indexed kinds, what
you gonna index /them/ with? Long term, I'd far rather think about
how to have some sort of dependent functions and tuples than muddle
along with singletons and weak existentials.

> So this sort of type-level vs. value-level duplication with GADTs  
> tying the
> two together seems to be what is always done in ATS. This may not be  
> as sexy
> as taking the plunge all the way into dependent typing ala Agda and  
> Coq, but
> it might be a practical point in the design space that GHC/Haskell- 
> of-the-
> future could move toward without too much shaking up. And if ATS is  
> any
> indication, it allows for very efficient code, to boot. :)

I'd certainly agree that ATS demonstrates the benefits of moving
in this direction, but I think we can go further than you suggest,
avoiding dead ends in the design space, and still without too
much shaking up. 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!

To be honest, I think the real challenge is to develop good libraries
and methodologies for working with indexed types (and particularly,
indexed notions of computation: what's the indexed mtl?). There are
lots of promising ideas around, but it's hard to build something
that scales whilst the encodings are so clunky. A bit of language
design, even just to package existing functionality more cleanly,
would really kick the door open. And yes, I am writing a research
proposal.

All the best

Conor