About That Type Theory

I got the new bugzilla to work (kind of time consuming, but surprisingly straightforward), and … I guess it’s a bit of an improvement. In the process of converting the htaccess files of bugzilla into domtool config, I discovered that you can’t put filesMatch inside of directory thanks to some fancy context nesting (directory and location both establish context Location; <FilesMatch> is only valid in a <Directory> so you lose…).

I … kind of stabbed at things aimlessly until it worked and then did it again and came up with adding a Directory context and allowing filesMatch inside of that. This means we’d need a new filesMatchAll or something to do what the current version does (sensible, since <FilesMatch> under a virtual host matches all sub-directories i.e. different behavior, different action … luckily, zero HCoop members are using filesMatch).

context Location;
+context Directory;

extern type location;
{{A valid URI prefix}}

extern val location : location -> ^Vhost & Location => [Vhost & !Location];
-extern val directory : your_path -> ^Vhost & Location => [Vhost & !Location];
+extern val directory : your_path -> ^Vhost & Directory & Location => [Vhost & !Directory & !Location];
{{Set some configuration specific to a URI prefix or filesystem directory,
respectively.}}

extern type regexp;
{{PCRE regular expression}}

-extern val filesMatch : regexp -> ^Vhost & Location => [Vhost & !Location];
+extern val filesMatch : regexp -> ^Vhost & Location => [^Vhost & Directory & Location];
{{Mark nested configuration to only apply to filenames matching the regexp.}}

Problem: my reading of the language reference implies that there is only one context on top of the stack at a time, and there is no sequencing operator for matching a chunko of the stack. So my Directory & Location type might only check because of an accidental property of the type checker. Relying on accidents for things is clearly a bad idea…

I’m pretty sure being able to push more than one context onto the stack at once is a desirable property, so I have to wonder if this intentionally works.

I spent a couple of hours digging around in the type checker code and yow! It seems like it ought to be sensible, but it’s doing unfamliar things in familiar ways so I guess it’s time to get out the ol’ pencil and paper and trace through the checking process for an expression I know is correct to get a feel for how it all works. Or: plead for Adam to page this bit of knowledge back in and tell me if I’m an idiot or not if I agree to worship static type systems.

The last couple of months have been strange; I look back on the last three and a half years of hcoop and think I didn’t do enough, and then I realize that I only recently had the watershed moment where slamming my head against UNIX enough times led to me knowing what I’m doing. The worst part is nothing is too complicated, but the breadth of knowledge required is astounding.

Except for domtool, which requires that I learn how to exercise discipline with types instead of living in the delightfully inconsistent freewheeling Land of Lisp.

About That Type Theory by clinton is licensed under a Creative Commons Attribution-NoDerivatives 4.0 International License.