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