Site Design Planning 2018-09-12

Tags:
By Max Woerner Chase

In this post:

So, I'm trying out this week something along the lines of "a small project, plus idle speculation about other things".

For the little project, I'm trying to fix an issue I noticed with the code block rendering.

Basically, I expect that the line numbers next to code blocks should line up with the code.

Currently, the line numbers and the code have a vertical offset between them, at least in Firefox and I think Safari.

It appears that this offset derives in some way from the presence of a horizontal scrollbar at the bottom of the code block, that is only present for the code and not the line numbers.

I'm not sure exactly how I'm going to stop the offset from happening, but that's what I want to get done this week. Nice, simple, small-scope goal.

What I know is, the code block is a table, with I believe two cells. One for the line numbers, one for the code. The cells are supposed to be the same height, but they are less the same height than I want them to be.

Next time, I try to figure out "what must I do to cause 'this cell needs horizontal scrolling' to affect both cells the same way?"

("Max, this sounds like a quick project."

If it were truly quick, I would have just done it. The preliminary research for this was super obnoxious.)

In the idle musings/speculation side of things, I haven't stopped messing with Ghosts of Departed Types.

I've implemented enough of the stuff from the first three sections to understand the motivation at the beginning of the fourth. So, what I want to have, and do not have currently, is a means of associating type-level information to particular values in a program, and type-level proofs constructed from those values, that can be required by functions in order to compile.

Now, the ability to define named struct alternatives was useful. What I'm leaning towards saying is, the newtypes need trait implementations, and to get the trait implementations you want, you need to control the newtype. But, what if the newtype is a simple wrapper around a core Named value, so interconversion is just a matter of adding or removing the newtype. So, instead of a custom parallel to Named, there'd be more invocations of named, and sorting a named vector with a named comparator would produce the type-level assertion "this list was sorted by this comparator"... well, the name would have to be associated with the sorting, actually... At first, I didn't see the utility in wrapping another phantom type around data, when the point of the types in question is to refer to type-level data that doesn't necessarily relate to the actual value; I'm not sure whether "Oh yeah, data in Rust usually has to support mutability" is a justification.

I feel like I might be leaning towards a design where there's just a massive closure-onion thing. Like, there doesn't seem to be a way to "leak" names out of their associated closures, so I'd better use one approximately every time I'd use a let-binding? Write a sort function that only guarantees the value is sorted inside its closure.

Would library authors want to expose their newtypes? The way I'm thinking about it, it shouldn't hurt.

What I don't have a clear mental image of is how the proof types are introduced and processed. From skimming that part of the paper, it looks like it's possible to hand-unify the types, but there's also talk of type-system extensions. My inclination for now is to start with hand-unification and try to improve the ergonomics within the confines of the language. Applying type transformations in Rust suggests to me a trait for "apply this rule" where the input is a restricted domain built up from how the trait is implemented for the rule, and the result is held in an associated type. It would be possible to cut down on the syntactic clutter some by defining type aliases.

Also, with only one "true" NamedStruct, just expose nice interfaces to everything with inherent methods, drop the macro. (This code is so pre-1.0, it's not released in any form.)

Overall this looks like a promising idea, but I sense I should step back from it for a while.