On Tue, Jun 2, 2015 at 10:14 PM, Matt Oliveri <atma...@gmail.com> wrote:
> On Tue, Jun 2, 2015 at 11:24 AM, Jonathan S. Shapiro <s...@eros-os.org> > wrote: > > > So: I really like the idea, but I'm not convinced it should be > incorporated > > into BitC. A middle position would be to leave a placeholder syntax for > it > > and do this type of discharge using an external tool for those programs > that > > need it. > > Maybe it'd be better to let the hypothetical future refinement type > system designer design the syntax too. They hypothetically ought to > know what they're doing better than us. Quite possibly. The general issue here is that refinement types (and lots of other property languages) need to mix expressions in with types. The C# attribute-sublanguage is an illustration of this. From a syntactic perspective, it mainly comes down to ensuring that you have a syntactic "hook" in the grammar for everything you might want to attach a property to. C# notably omitted hooks on types and sequence points, for example. Sequence point attributes could easily be added to the syntax. Not so easily on types. shap
_______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
