[Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
dan.doel at gmail.com
Sat Mar 14 14:48:29 EDT 2009
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
> 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
More information about the Haskell-Cafe