Viewing profile — syrak

You need very little to make a Prolog-like language Turing-complete (lists and recursive predicates). And so Haskell's type system only needs one (or two) extensions to be Turing-c…

I learned a lot from this and your other comment here! The way I connected the dots when I read about Clear (and OBJ) is that it let me explain free algebras by example, by just sh…

IMO your view, if not common, is kinda intuitive from the point of view of someone trained in set theory/classical logic (i.e., most people before they find an interest in type the…

Thanks for sharing this! These tidbits of history are fascinating.

Thanks! Here we go: "Note: In versions of Miranda before release two (1989) it was possible to associate "laws" with the constructors of an algebraic type, which are applied whenev…

That's surprising! I (author of the blog) just repeated what's in the 1985 paper. The feature might actually have been removed, or never even been implemented. One would have to fi…

Is that something he did to people who mis-cited his language?!

Author here. It's funny you mention this. I was (am still) writing a post about it, and I went on a rant that while it's a (fun!) way to do "algebra with types", it's not actually …

That point is discussed in the paper: circle-freeness is Pi^0_2 in the arithmetic hierarchy, so there isn't a reduction to halting (Sigma^0_1) in the usual sense of a mapping betwe…

The paper in the OP discusses this claim in section 3, and mentions that Kleene came even before that: > We would note that Kleene seems, however, to have already had the self-refe…

For verified Rust there is also https://github.com/creusot-rs/creusot

The write up is pretty nice https://sugawarayuuta.github.io/charcoal/ Since that's the point of comparison, what's the Go standard library's strategy? Is it inherently slower than …

This post is rendered at https://sugawarayuuta.github.io/charcoal/

Even if you had a verified SMT checker, you also need to prove that the encoding of the problem in SMT is correct, i.e., that a proof does translate to a valid register allocation …

I've learned quite a lot about editing from "Style: Lessons in Clarity and Grace." It presents some tricks to restructure and improve the flow of sentences, and through that proces…

> If the underlying premise is flawed, who cares if the methodology is correct? How do we know the premise is flawed? > The first step should be to show that the github dataset can…

> It's not clear to me that it has any use at all if you don't have higher-order functions. The very origin of defunctionalization is to emulate higher-order functions in a languag…

O(N + M) is not equivalent to O(N) if you make no assumptions about the relative growths of N and M, that's why it's actually meaningful to keep both terms around. You can only red…

> I do wonder why people keep building more systems of this kind. Not a lot of languages have higher-inductive types which is the main advertised feature here. At least they're mis…

> I've never read a code base where I thought the type system was doing a good job of being a DSL for describing business requirements Would refinement types help in that respect? …

> In this case it is hard to be sure that the function must behave in the correct way because of its type. I would argue that in this case it is quite easy to ensure that it does t…