Paul Stansifer

The type system can’t solve a parsing problem! (Well, in Unseemly, that’s not guaranteed to be true, but it’s true here.) The parser still needs to know what interpolation to...

The simple solution is implemented, I think, but there's an exciting ICP that happens in `beta.rs` when freshening `.[ ,[name], : Int . five].`. Everything about `bound_from_beta` looks super-wrong, but...

Implicit in the above is that pattens will be required to be irrefutable at their types. At the moment, that isn’t a big change, but it does seem to cut...

Now I think that compiling to a high-level language is probably a bit of a false economy. As issue #35 argues, having few core forms makes it easier to write...

I _think_ that an incremental parser should be possible (I don't know much about how suited an Earley parser is for that), and I definitely want to eventually have an...

I think it's fine to say "We don't know... " or "TODO: figure out why ..." or "Why doesn't ... ?"

I had thought that reversing might be doable by marking some type variables of a macro definition as covariant and some as contravariant. That won't work! You might have something...

Implementation... ugh, this seems tricky. We don't want to accidentally make `*[b: Int]*` a subtype of `*[b: ∀T. T]*` (or maybe I have that backwards). The point is that the...

Actually, I think that we have the exact same problem if we do the "normal" thing: we'd effectively be moving all of the ∀s up to the top, but we'd...

I wonder if the subtyping system is much too complicated. According to page 222 of https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf, the subtyping rule for foralls is really simple. Now, this particular problem (and the...