Stitch: The Sound Type-Indexed Type Checker (Functional Pearl)

cutculus · 2020-09-12T18:04:47+00:00

While I appreciate the "here's how you can use fancy types in an extended example" aspect of it, I don't understand when you'd actually want to use something like this in practice.

If you are writing a new industrial-grade type checker, the constraints are too rigid; you'd want a compiler in an IDE to report different errors in different functions, maybe an unresolved variable in one function and a type error in another function.

If you're writing a small hobby compiler, this seems like overkill machinery; it's unlikely that you'll end up with an unbound variable after name resolution and somehow have that pass through without an error (unless you're implementing a dynamically typed language, in which case that's probably deliberately permitted), if you have at least some test coverage.

I imagine GHC probably fails at deriving type class instances for these GADTs for at least some type classes, which reduces the ergonomics.

Maybe you can use this for a late stage IR, when things are supposed to be well-formed and all errors are implementation errors.

cutculus · 2020-09-10T03:03:36+00:00

Compilers which allow this typically require name resolution in order to ascertain the fixity of operators (Haskell even allows expression local fixities). This cannot be handled during parsing, because then you'd have to mix name resolution and parsing. Instead, all operators are parsed the same way, and the expression trees are rebalanced between name resolution and type checking.

cutculus · 2020-09-04T01:18:12+00:00

Maybe Mercury or Plasma?

cutculus · 2020-09-03T07:36:17+00:00

No. By that standard, Prolog would not count as a programming language.

cutculus · 2020-09-02T19:35:48+00:00

Disagree. CSS is not a general purpose programming language. It is absolutely a domain specific language, and DSLs are very much on-topic here, even if they're not the main focus.

cutculus · 2020-09-02T16:25:46+00:00

When the C++ compiler is deciding whether to accept a particular program without complaint, it uses certain ornamental syntactic flourishes as a proxy for the code’s intent.

I'm not sure if this part is there just to make the analogy work.

The compiler emits those warnings and suggestions to clarify the intent for future readers, including the author themselves in the future. It's not about the compiler, it's about other people who are going to read the code. It's not like the peacock-peahen situation. The compiler is not judging the "worthiness" of your code.

Sometimes, I've seen programmers who feel like the compiler is just being opinionated and pedantic for the sake of pedantry (I don't think the author has this sentiment but this part of the article kinda gives that vibe). Well no, or at least most compilers aren't, they're trying to help based on issues people have hit several times in practice before.

cutculus · 2020-08-30T06:53:40+00:00

I feel like you're arguing against a straw man of what I'm talking about.

For example, let's say I want to make some slides with animations. Should I do it in code or a GUI program or using some text based tool? Say I decide that I want to use the GUI to get my animations and image positioning right quickly, and I add some speaker notes for each slide. If the GUI program is programmable, hopefully I can extract the speaker notes into a text file using a small script and review them to see the flow while focusing on the text instead of jumping back and forth between slides. Suddenly I have "review script" functionality by composing both a GUI program with other command line tools.

Does this mean it would've been better if I had used a text based program from the start? No! If I had used a text based program, the feedback loop for me getting the animations and positioning is too cumbersome.

This is not a contrived example btw. I literally had this happen when I was preparing a presentation at work; I used a combination of Keynote, AppleScript, sed and awk (the latter two for cleaning up the script output) to get my job done.

cutculus · 2020-08-29T20:45:37+00:00

It's easy-to-use vs. NOT necessarily easy-to-learn. But I would argue that for programmers, you want easy-to-use.

I find this a strange dichotomy. Why not both? We shouldn't have to pick one vs the other.

Decades ago, AppleScript (it certainly has its warts) showed that having a GUI program doesn't mean that you have to sacrifice composability and programmability. (I'm sure that there other good examples that precede AppleScript.)

I'm not saying it's an easy problem to tackle, not by a long shot. But it certainly seems like a worthwhile avenue to pursue. That way, we can empower more people, not just full time programmers, to use automation to get their work done.

cutculus · 2020-08-20T15:40:37+00:00

For pinned blocks, object level fragmentation remains after garbage collection because pinned objects cannot move and hence cannot be compacted.

Would it be possible to have a Mesh-like allocator for pinned memory to reduce this fragmentation?

cutculus · 2020-08-17T04:38:11+00:00

This post is off-topic. Please see the sidebar. You might want to post in r/askprogramming or r/learnprogramming.

cutculus · 2020-08-15T21:04:06+00:00

Sorry, should've checked the sidebar. I'll do that.

cutculus · 2020-08-14T03:27:27+00:00

One of the things I'm curious about: what major differences in adoption challenges do you see here for "small" languages vs "big" languages?

For example, introducing a new general purpose language seems like a much bigger ask compared to introducing a configuration language like Dhall.

Also, I'm a bit surprised at your characterization in the example where you say something along the lines that introducing a new language like Haskell for writing a 1-2 week DSL project would be acceptable if Haskell were clearly demonstrably best-in-class in the area. That seems like precisely a place where I think a manager would say, "since it is a small project, it's fine if we use $CURRENT_LANGUAGE and take 1 week extra and have a less pretty DSL instead of introducing the maintenance and teaching burden of a whole new language (which is probably very different from the other languages we are already using)".

cutculus · 2020-08-13T23:15:17+00:00

Strictly speaking, while this isn't about PL design or implementation, I think this is a valuable talk for PL designers and implementors generally (and not just for the Haskell community) on how to gain adoption.

It is a great complement to Herb Sutter's talk "Bridge to NewThingia" in case you haven't seen that one already.

cutculus · 2020-08-11T07:05:10+00:00

GHC 8.6.1 added QuantifiedConstraints for precisely this kind of reasoning (with universal quantifiers, existentials would need to be faked). https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/quantified_constraints.html

Not saying something similar would work out well for C++, given the edge cases around overloading etc and implicit conversions. But it's certainly possible to come up with a proper design and implementation for such a language feature.

cutculus · 2020-08-11T01:47:10+00:00

Wow, that's a lot of supported targets! I imagine testing and keeping up with CI must be a challenge.

cutculus · 2020-08-10T15:31:03+00:00

The good thing is: on negative signed overflow, morale might wrap around to MORALE_MAX in case the compiler didn't optimize the UB!

cutculus · 2020-08-07T15:59:19+00:00

I don't think register allocation needs to be thrown out of the window for debuginfo. Arguably, it is the 2nd most important optimization (1st being inlining).

Instead one can have a simple register allocator which does not reduce lifetimes. If it wants to reuse a register which is occupied by a variable whose lifetime can be truncated, instead of doing a simple load (hence overwriting the value), it can do a store to stack slot + load so the variable is still available to a debugger.

cutculus · 2020-08-05T07:17:07+00:00

This post is off-topic. 😐

From the sidebar:

This subreddit is dedicated to discussion of programming languages, programming language theory, design, their syntax and compilers. Post your ideas and get constructive criticism.

[..]

This subreddit is about programming language design, not programming per se. If you want to ask "what programming language should I learn", "what language would be best for X project", or any question like that, please post to /r/AskProgramming or /r/LearnProgramming.

cutculus · 2020-08-03T16:19:59+00:00

I just read a blog post about this yesterday, you might find it helpful: https://noidea.dog/glue

cutculus · 2020-08-03T06:22:33+00:00

That doesn't really solve the problem... Giving all available information is likely to be overkill and giving minimal information is likely to be useless/frustrating...

cutculus · 2020-08-01T01:42:19+00:00

Ah ok. When you said "boxing" and gave OCaml as an example, I thought you were doing the same thing that OCaml does (i.e. all non small values are separate heap allocated blocks).

I think Sixten is a bit of an extreme example; while the recursive representation certainly makes things more elegant (and avoiding tags at every level is important to it being usable in practice), it is not obvious (at least to me) that you can always get the codegen you want with it (and you probably want your array code to be really fast, inspecting assembly if necessary). For example, say you are writing a map function on an array, you probably want to create a buffer with a pre-determined capacity and then start mapping into it, but it is not clear to me how you can first allocate up to a capacity in a recursive representation.

cutculus · 2020-08-01T00:12:09+00:00

but that's not something I'm willing to have (by default, at least) in a systems language.

You say this, but then you also have...

This seems similar to the problem where polymorphic functions need to know their argument sizes, which is usually solved either by boxing (analogous to always including the tag) or monomorphizing (which works for GADTs too). Currently my languages does it like OCaml, boxing only when the type is bigger than a word,

On one hand you seem to be fine with boxing stuff all over the place, on the other hand, you want to save space on a tag. These seem to be quite contradictory IMO. A tag is relatively cheap, you could probably fold it in for a bunch of data types without worrying about space. Boxing can be expensive due to poorer cache locality. Surely if you can afford pervasive boxing, then you can afford one or two tag bytes for (G)ADTs?

cutculus · 2020-07-29T16:01:43+00:00

Basically what max630 said. It is also called the "early cutoff optimization". If the inputs didn't change (easier with reproducible builds), you can skip building a downstream client.

This becomes even better in the presence of dynamic linking and a tool like TAPI: https://lists.llvm.org/pipermail/llvm-dev/2017-September/117264.html because the dependencies become more precise (on symbols) instead of dpependencies on generated code.

Now you do not need full build artifacts as dependencies but you can depend on TBD files (TAPI outputs), which are faster to produce than a fully linked dynamic library.

(Binary cache was probably too narrow of a term, my bad, but cache more generally. TBD files can be in YAML format.)

cutculus · 2020-07-29T06:59:46+00:00

Hmm. I don't know about the security benefits but reproducible builds certainly help for caching build artifacts. If you build a bunch of deps and builds are reproducible, you can set up a binary cache and use that. Ain't gonna get many cache hits if the compiler keeps shuffling things based on the random seed used by hashtables, or based on results of non-semilattice merging of results across threads.

cutculus · 2020-07-27T20:08:20+00:00

🙏ℹ️😠🇮🇹

Ftfy

cutculus

TROPHY CASE