[Haskell-cafe] Microsoft PhD Scholarship at Strathclyde

[Dan Doel]

On Saturday 14 March 2009 1:07:01 pm Conor McBride wrote:
> 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.

Well, I don't actually like it, either. Finding this out rather disappointed 
me.

> 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!

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).

So adding more faux dependent typing (like ATS or Omega) isn't just wasting 
time when we should be figuring out how to compile Agda efficiently, because 
simply making type-level programming easy, while maintaining a strict divide 
between values and types may well be good enough in practice, until the Agdas 
and Epigrams come into their own.

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. :)

-- Dan