[HN Gopher] Coq typeclass resolution is Turing-complete
___________________________________________________________________
Coq typeclass resolution is Turing-complete
Author : thaliaarchi
Score : 51 points
Date : 2023-04-16 16:34 UTC (6 hours ago)
(HTM) web link (thaliaarchi.github.io)
(TXT) w3m dump (thaliaarchi.github.io)
| manyoso wrote:
| But Coq is strongly normalizing... it always halts. What gives?
| thaliaarchi wrote:
| This is the automatic resolution of some instance satisfying a
| typeclass constraint, and is not related to the termination of
| functions. This does not call a function. If you compare it to
| the relational definition I give at the end of the semantics
| section, the typechecker does not similarly infer satisfying
| constructers for the relation. Proof tactics can also diverge,
| but that's different.
| tlringer wrote:
| Typeclass resolution is implemented as a layer of automation
| that is above the type-checking kernel, so much like with
| nonterminating tactics, if it doesn't halt you mostly just end
| up with confusing automation that doesn't help you prove
| something, but you shouldn't be able to prove false. Mostly
| it's a usability nightmare for typeclasses, and in the case of
| this post also a way for hilarity to ensue.
| nextaccountic wrote:
| > Mostly it's a usability nightmare for typeclasses
|
| And also for Rust traits, C++ templates, etc (those are all
| nonterminating)
| fpoling wrote:
| It just gives up after running for too long as any Turing-
| complete type checkers are doing.
| yodsanklai wrote:
| Any practical consequences?
| thaliaarchi wrote:
| Author here! I had a hunch that the typeclass resolution engine
| in the Coq typechecker could be Turing-complete, so I proved it
| by implementing a variant of Brainfuck in it. Feedback welcome.
| ashton314 wrote:
| I'm shocked you didn't just start with white space. ;)
|
| I'm excited to dig through this more. Nice work!
| wellanyway wrote:
| Not a feedback, question. How do you feel doing work like this
| in a world where people see javascript as a acceptable
| language? Second, somewhat related, what would be the biggest
| problem preventing wide, industry adoption of Coq/other formal
| methods?
| rowanG077 wrote:
| I don't think people find Javascript an acceptable language.
| The meteoric rise of TypeScript proves that.
| thaliaarchi wrote:
| I think there are varying levels of assurance that developers
| need while writing software. I tend towards stricter
| languages with more guarantees, like Rust with its borrow
| checker and Coq with its powerful types and proofs. This
| doesn't need to be a universal preference, though; my
| preferred work is in compilers, which requires a high degree
| of assurance, and I study programming languages formally.
|
| The largest barrier to greater adoption of languages like Coq
| with proof systems built-in is the formal background needed
| to get started. I think that Rust has done an excellent job
| at making stronger systems more accessible, but it takes a
| lot of conscious work.
|
| With JavaScript, I think the idea that performance in
| language design can be an afterthought, made up for by world-
| class optimizing JIT compilers, is fundamentally wrong. It
| doesn't give users a meaningful way to easily reason about
| the performance of the programs they write. The main
| implementation of Python, pythonc, is essentially an
| interpreter over an unoptimized bytecode format, giving it
| poor performance. I think performance considerations should
| be a fundamental part of the language design.
| haweemwho wrote:
| Thanks for your perspective.
|
| I'm wondering how this squares with the tendency of formal
| language theory folks to push for functional languages.
| It's clearly a preferred approach if rigorous correctness
| is your main goal, but don't functional languages like
| Haskell suffer from the fundamental issue that reasoning
| about runtime performance is really hard?
| thaliaarchi wrote:
| Haskell is notoriously difficult to reason about runtime
| performance, but that is due to its lazy evaluation, not
| because it is functional. Lazy evaluation can cause
| hidden space leaks, where expressions have not yet been
| evaluated, so maintain references to other values. Most
| functional programming languages are not lazy.
| IshKebab wrote:
| Yeah I've wondered about that. Especially the obsession
| with singly linked lists.
| User23 wrote:
| > The largest barrier to greater adoption of languages like
| Coq with proof systems built-in is the formal background
| needed to get started.
|
| I believe this to be a language problem and not a
| conceptual problem. All that you need to pragmatically
| formalize semantics is Hoare triples and basic predicate
| calculus[1]. Anyone that can understand an if statement
| already has the necessary conceptual machinery. The so-
| called "formal methods" community delights in over
| complicating the problem with gadgets like category theory.
| Which is ironic, because they're introducing the same kind
| of unnecessary complexity that causes the problem that
| they're trying to solve.
|
| [1] ok that's not utterly strictly true because arrays (or
| mutable functions, as I like to think of them) present some
| subtleties, but those are more a problem for the definers
| rather than the users.
| thaliaarchi wrote:
| I was referring to how the communities of these languages
| typically frame the problem, so you need formal
| background to read the materials published on it. As you
| say, this is a major barrier. This is where Rust shines,
| in that they've framed the language in terms of how its
| used, developed accessible documentation, and steered
| away from delving into the theory behind it.
| tromp wrote:
| How does the famous largest number contest winner loader.c fit
| into this? Its search for well typed programs has to be
| halting...
| thaliaarchi wrote:
| I was not familiar with loader.c, so I did some digging[0]. It
| implements the Calculus of Constructions, which Coq is based
| upon, and generates all programs encoded lower than some value.
| The search is halting, though very long.
|
| From the analysis[1] in the contest:
|
| > {loader.c}, diagonalizes over the Huet-Coquand `calculus of
| constructions'. This is a highly polymorphic lambda calculus
| such that every well-formed term in the calculus is strongly
| normalizing; or, to put it another way, a relatively powerful
| programming language which has the property that every well-
| formed program in the language terminates. The program's main
| function is called D. ... D works approximately as follows:
| given an argument x, it iterates over all bit strings with
| binary value less than or equal to x, and, if such a bit string
| codes for a well-formed program (`term' in lambda-calculus
| language), it runs the program (`strongly normalizes the term'
| in lambda-calculus language.) The return value of D is then
| obtained by packaging together the return values of all these
| programs. The program's return value is D@@5(99).
|
| [0]: https://googology.fandom.com/wiki/Loader%27s_number
|
| [1]: http://djm.cc/bignum-results.txt
___________________________________________________________________
(page generated 2023-04-16 23:01 UTC)