Hacker News Reader

Comment by smallnamespace | Hacker News Reader

I’m surprised the article discusses extensional equality for functions, then doesn’t mention why languages don’t try to derive it: it’s equivalent to solving the Halting Problem (per Rice’s Theorem).

View on HN

That's only for Turing complete languages. It's not true for total functions. Total functions can be written in Coq, Agda and Idris among others.

Funnily, in programming languages based on Martin Lof Type Theory, the topic of function extensionality is a whole rabbit hole for reasons other than the halting problem.

There is a distinction between intensional Martin Lof type theory and extensional Martin Lof type theory, which differ in their treatments of equality. First, one must distinguish between judgmental equality x = y, which is a statement in the mathematical metalanguage that two terms are equal, and propositional equality, which "internalizes" judgmental equality within the programming language through the equality type Id(A, x, y), the type of proofs that x and y are judgmentally equal. In extensional type theory, judgmental equality also follows from propositional equality, and together with the eta-conversion rule for functions, function extensionality is provable [0]. However, typechecking extensional type theory is undecidable [1].

Alternatively, in Homotopy Type Theory (HoTT), supports function extensionality is provable from the univalence axiom, which states that isomorphic types are equal [2]. Function extensionality is trivially provable in Cubical Agda [3], which gives a computational interpretation of HoTT's notion of equality.

[0] https://cstheory.stackexchange.com/questions/46331/extension...

[1] https://cs.stackexchange.com/a/112559

[2] https://ncatlab.org/nlab/show/function+extensionality#relati...

[3] https://agda.readthedocs.io/en/v2.6.0.1/language/cubical.htm...

Yeah, I didn't mean to insinuate that function extensionality is provable or testable in those languages, just that one can ensure that one is actually writing total functions today. I'm sure the same could be done in a simple or polymorphic type theory, I'm just not aware of one. Is there a Haskell extension like Idris's totality checking?

I was gonna say, just wait until the OP hears about HoTT.

Thanks though, I didn't know Cubical Agda exists.

> Is there a Haskell extension like Idris's totality checking?

There's LiquidHaskell https://ucsd-progsys.github.io/liquidhaskell-blog/

Even for things like regular expressions checking for equality can cost exponential time. Whether something is exponential or undecidable is pretty much irrelevant if you want to run the algorithm as part of compilation.

Good thing that's not relevant in general then.

I think Rice's theorem is a big hammer here: it's equivalent to the halting problem because one can just test extensional equality of

    given M: simulate M; return 1

and

    given M: return 1

Or is it even true of extensional equality for _total_ functions?

"I think Rice's theorem is a big hammer here"

It is certainly a big hammer, but as theoretical computer science tools go, it is pleasingly easy to use. Unfortunately it is pleasingly easy to use in much the same way high explosives are pleasingly easy to blow yourself up with, as it annihilates so many things that we'd rather like to keep. But, still... easy to use.

Reply on news.ycombinator.com