On 2 July 2014 07:58, 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. 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?
In Idris, which is fresher in my mind, : may appear in several places, where it is a required keyword in the grammar. It may appear in the form of a type declaration as in "foo : bar -> baz", it may appear in a datatype declaration as "data Foo : Type -> Type", and it may appear within a pi expression "(x : Foo) -> rest" which describes an argument of type Foo which is bound in the remainder of the signature. At expression level, 'the' works much like ':'. For example, "the Nat 7" unifies Nat with the type of the literal 7. -- William Leslie Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
