pittma

I am not the original author—this is adapted from an implementation by Shay Gueron, the author of that paper I linked, but I do agree that it's cool!

ymms were used here on purpose! With full-width registers, the IFMA insns have a deleterious effect on frequency, at least in the Icelake timeframe.

Cool stuff! This method is very similar to how AVX-512-optimized RSA implementations work too, as they also have to do Very Large Exponentiations. This paper[1] covers how RSA does its windowing, which includes the formula showing how the window size can be arbitrary. One additional thing AVX-512 RSA implementations do, though, is store the results of the multiplications for the range [0..2^{window-size}) in a table; then, for each window, that result is retrieved from the table[2] and only the shifting/repositioning has to be done.

1. https://dpitt.me/files/sime.pdf (hosted on my domain because it's pulled from a journal)

2. https://github.com/aws/aws-lc/blob/9c8bd6d7b8adccdd8af4242e0...

I have a pretty elaborate Hakyll site with custom routers and all kinds of junk (https://dpitt.me), but it's an old site that started as Django, then I built it from scratch with Sinatra, and then was Jekyll for years. There really is something special about a well-organized static site. For all the rewrites of this old thing, I can't imagine moving away from static site generation.

Hm, that's not how I'm reading this. An infinite loop is, by definition, partial. What I'm gathering from this is that that stuckness that the typechecker can encounter in the face of partiality is okay in Idris, that its typechecker just says, "welp, this is as far as I go."

> Totality is orthogonal to dependent types. You can absolutely have non-total programs at the type level: Rust has such programs today in fact!

Absolutely, the talk I linked to gets at this to some extent. In rust, partiality causes type checking to fail. You could use it on purpose!

> You can have an infinite loop in a total language like Agda or Idris: coinduction is the mechanism.

For sure, but the totality checker is appeased by sized-types, or at least that's how I know to do it in Agda. I've heard it can be done without them, but I'm not familiar with the approach. This is what I intended w/r/t structural recursion.

> This doesn't make a whole lot of sense to me.

This is because, as the authors state, to type check the program is to evaluate it, so before it can run you have proof that it is correct.

By opting out I'm more talking about the converse, to opt in when you need it. Kind of the opposite of Idris's %partial directive.

> You can be total over IO, and effects do not imply non-totality either.

That's fair, you're right. This is poorly stated.

You can, in fact, use traits to do type-level programming in Rust[1], but this is type-level programming; it isn't /dependent/ types. The biggest "blocker" for using dependent types is that programs must be /total/, because that program has to be evaluated for it to typecheck! If a program is not total, the typechecker has the potential of getting stuck. The two dependently-typed languages I've programmed in, Mostly Agda and a tiny bit of Idris, have totality checkers to aid in this. Generally this means that recursion is only allowed if its structural, and there can be no run-forever loops, i.e., no servers.

I think instead, for one of these languages, the ideal would be opt in should you need it. Dependent types are, by their nature, proof carrying[2], and there are times when you want this, but for a general-purpose programming language, also times that you do not. You can't be total over IO (or any effect for that matter), so, yeah, skip it when arg-parsing, but then opt-in when you're processing your financial transactions or actuating your robot.

[1] https://dpitt.me/talks/tt-for-rust/

[2] http://www.cs.nott.ac.uk/~psztxa/publ/ydtm.pdf

> Are you saying there have been studies that show Haskell's type system has not been correlated to higher correctness than say Java or Python, or are you saying you are unaware of any such studies?

On the contrary! Consider for instance: "Total Haskell is Reasonable Coq"[1]

1. https://arxiv.org/abs/1711.09286

It would appear that I accidentally a link or two.

https://github.com/auxoncorp/bounded-registers

https://github.com/auxoncorp/tnfilt

feL4 developer here. Happy to field questions, and to note that we'll keep introducing and extending the ergonomics for building complex applications, configuring platforms, and adding hardware support in the coming weeks/months.