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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe