Coq typeclass resolution is Turing-complete

Re:Coq typeclass resolution is Turing-complete by haweemwho on Sunday April 16, 2023 @03:03PM (#35593230)

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?

[ Parent | on HN ]

Re:Coq typeclass resolution is Turing-complete by thaliaarchi on Sunday April 16, 2023 @03:16PM (#35593333)

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.

[ Parent | on HN ]

Re:Coq typeclass resolution is Turing-complete by IshKebab on Sunday April 16, 2023 @05:33PM (#35594474)

Yeah I've wondered about that. Especially the obsession with singly linked lists.

[ Parent | on HN ]