Paul Stansifer

So… I’m really not sure how to deal with the fact that Scheme syntax and typical type syntax are so different. Here’s an idea I need to write down to...

Another option, which operates on a totally different axis, is to syntactically mark name introductions. A cute idea I had from long ago puns on a convention in written English:...

Let's see how this looks, integrated with... uh "syntax-for-syntax" (i.e., special punctuation-y forms for things that have specifically to do with syntax): ``` (extend-syntax expr (macro (t) ((lit default-token "for")...

What would Unseemly look like with the "most normal" syntax (Scheme expressions plus Rust types)? ``` (extend-syntax Expr (macro (T) ((lit default-token "for") (name elt-pat Pat) (lit default-token "in") (name...

Maybe part of the problem is with the language; we're writing `...[,value, >> ,[value], ]...` instead of `,,,[value],,,`. After all, Scheme has `unquote-splicing` (good ol' `,@`). This means that we...

Actually, no, I don't think we can merge splicing and unquote. The motivating example for #38, `'[Expr | .[ ...[,a, >> ,[a], : Int ]... . ].]'`, is a case...

Maybe we could, at the dotdotdot, squirrel away an index 0 somehow, start evaluating, and, when we come to the driven interpolation, pick the indexed result from its output. The...

I'd forgotten: splice healing isn't even used by `...[ ]...` (it does roughly the second suggestion in the previous comment). The only place it's needed is for subtyping `:::[ ]:::`....

Actually, according to TAPL, we can encode existential types as universal types. We might still want to have existential types (I think it's important that types "bottom out" to a...

For the long-term solution to this problem, maybe we say that, if the grammar goes `Nt1 ::= Nt2 | …`, then `Nt2` is a subtype of `Nt1`?