On Wed, Jun 3, 2015 at 10:22 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Tue, Jun 2, 2015 at 10:14 PM, Matt Oliveri <[email protected]> wrote: >> On Tue, Jun 2, 2015 at 11:24 AM, Jonathan S. Shapiro <[email protected]> >> 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.
Ah. But on the other hand, you could also just make your own parser for surface syntax with the same look and feel as C# (or not), but change things to leave room for whatever you need to add. Then you could strip out the extra stuff to translate the "unrefined" parts to C#. And hypothetical future refinement type system designer can do the same for BitC. They might not be satisfied with your attempt to provide enough hooks either. They might appreciate an open-source, well-documented parser though. Maybe I'm not understanding the importance of strict compatibility at the surface syntax level. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
