On Tue, Jul 1, 2014 at 2:58 PM, Jonathan S. Shapiro <[email protected]> wrote: > Matt: > > On Tue, Jul 1, 2014 at 10:12 AM, Matt Oliveri <[email protected]> wrote: >> >> The dependently-typed languages I'm most familiar with, Coq and Agda, >> don't try to separate types and terms into sub-grammars... > > > That's more or less what I thought. But it creates some interesting > grammatical issues, notably at type-qualified expressions. If you have > something like > > expr ':' type > > that can end up turning into > > expr : expr : type ... > > and so forth.
Coq is right associative here, so that e0 : e1 : e2 means e0 : (e1 : e2). There's no fundamental problem with right associativity or simply banning it. In the homotopy type theory book, and likely other discussions of type theory, e0 : e1 is considered a judgement and is outside of the expression syntax, so in particular e0 : e1 : e2 is banned. That seems a bit heavy handed for a programming language. > And there are things in the type language that are not > expressions. For example the names of the core types in the language. How > does agda resolve this sort of thing? Why should core types be treated differently at the grammar level? Can't they just be in-scope at the start of every module, and treated as normal identifiers? In a dependently typed world view there's no difference between core types and prelude functions such as +. Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
