Cogent Macros

[zilinc]

Just as a reminder and placeholder for now. No concrete ideas atm.

[liamoc]

Macros are something I want too. We may look to Rust for inspiration here.

[liamoc]

I think macros would allow us to avoid baking in too much syntactic sugar (although we probably still want it for error handling).

[zilinc]

A semi-related things is, having quasiquotation we can probably get rid of the .ac files.

[zilinc]

Rust's macros look more intuitive than TemplateHaskell for systems users.

[liamoc]

Yes I don't think we'll want anything even close to TemplateHaskell.

[zilinc]

thinking about it more, handling indentations in macros could be challenging; in particular we don't always have the more explicit form with delimiters.

[liamoc]

Indentations are part of concrete syntax. Why would it matter to macros?

[zilinc]

Am I missing anything? You need to write concrete syntax in the macro definitions. E.g.

macro_def X ($pat:p) = [| | Success p -> 0 |]

foo : <Success U8 | Error ()> -> U8
foo x = x | Error _ -> 1
              X (v)

Does X match on x or on 1?

[liamoc]

We shouldn't allow that. Macros should work on abstract syntax.

[liamoc]

In particular, you wouldn't be able to quote a pattern without the scrutinee, because the quote needs to be a well-formed syntactic unit.

[liamoc]

So you could have:

macro X x (pattern p) = [| 
    $x | Success $p -> 0  
       | Error _ -> 1
     |]

foo :  <Success U8 | Error ()> -> U8
foo x = X x v

[zilinc]

But still,

macro_def X ($exp:a) = [| a | Success p -> 0
                                             | Error _ -> 1 |]

How do you align the two guards?

We'll have a macros meeting this Wed so I'll see then what the use cases are and how expressive macros we want.

[liamoc]

Same rules apply as with parentheses. The |'s need to line up.

[liamoc]

Macros must work on abstract syntax, and they must be hygienic with variable names. If they don't have those features, they're an immense source of bugs (just look at the C preprocessor)

[liamoc]

In Lisp, the grandfather of macro systems, you literally just take a parenthesised expression and quote it by putting a ' or the word quote in front.

Our quoting brackets or quoting mechanism should be parsed identically to parentheses.

[zilinc]

Hmmm. Don't know if it's powerful enough if we want to use them to generate ad hoc polymorphic functions, generate glue functions to convert between C and Cogent data structures, etc.

[liamoc]

Having Cogent be the macro language is going to be troublesome, because Cogent is not Turing complete and doesn't even have recursion or loops.

So, we'll have to layer a macro language over the top. The easiest language to use would be a dynamically typed, turing-complete language where the only data type is Cogent abstract syntax trees (Lisp goes one step further and replaces Cogent with Lisp here)

Exactly what operations you need would be hard to say in advance, but I presume you'll need:

• Some conditional structure, perhaps pattern matching on (cogent) syntax trees
• Preservation of variable hygiene - it should never be possible to examine a (local) variable name programmatically.
• Recursion

We could statically type the language too, but seeing as it runs at compile time any way there may not be any reason to do that.

This should be powerful enough to do anything you want to do.