The dependently-typed languages I'm most familiar with, Coq and Agda, don't try to separate types and terms into sub-grammars. That would be kind of against the grain, since types can be used as terms (of universe type). I guess that's too far in for BitC? I think I remember some extension of Haskell that used a "lift" construct to make terms-in-types explicit. But that seemed pretty annoying. It's hard when you've overloaded intro forms to be type constructors too. Perhaps by looking at the kind of the type constructor, you don't really need the lifts to be explicit. But that would mean the parse of a type expression is ambiguous until type checking...
On Tue, Jul 1, 2014 at 12:35 PM, Jonathan S. Shapiro <[email protected]> wrote: > Can somebody point me at examples of languages that (a) have dependent type > and (b) do it with a decently clean grammar? Dependent type tends to mix the > expression sub-grammar with the type sub-grammar, and the grammars for this > can be tricky. I want to look at some of the existing language > specifications to see how they managed to keep the two parts of the grammar > clean. > > > Jonathan _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
