4 ms·

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 th

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).

JadeNB 7y ago
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?
- jerf 7y ago
  "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.
guerrilla 7y ago
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.
- TheAsprngHacker 7y ago
  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/extensional-type-theory-and-function-extensionality/46342#46342 https://cstheory.stackexchange.com/questions/46331/extension... [1] https://cs.stackexchange.com/a/112559 https://cs.stackexchange.com/a/112559 [2] https://ncatlab.org/nlab/show/function+extensionality#relation_to_the_univalence_axiom https://ncatlab.org/nlab/show/function+extensionality#relati... [3] https://agda.readthedocs.io/en/v2.6.0.1/language/cubical.html https://agda.readthedocs.io/en/v2.6.0.1/language/cubical.htm...
  - guerrilla 7y ago
    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.
    - ghostwriter 7y ago
      > Is there a Haskell extension like Idris's totality checking? There's LiquidHaskell https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
- adrianN 7y ago
  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.
  - guerrilla 7y ago
    Good thing that's not relevant in general then.

JadeNB 7y ago

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?

jerf 7y ago
"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.

guerrilla 7y ago

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.

TheAsprngHacker 7y ago
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/extensional-type-theory-and-function-extensionality/46342#46342 https://cstheory.stackexchange.com/questions/46331/extension... [1] https://cs.stackexchange.com/a/112559 https://cs.stackexchange.com/a/112559 [2] https://ncatlab.org/nlab/show/function+extensionality#relation_to_the_univalence_axiom https://ncatlab.org/nlab/show/function+extensionality#relati... [3] https://agda.readthedocs.io/en/v2.6.0.1/language/cubical.html https://agda.readthedocs.io/en/v2.6.0.1/language/cubical.htm...
- guerrilla 7y ago
  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.
  - ghostwriter 7y ago
    > Is there a Haskell extension like Idris's totality checking? There's LiquidHaskell https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
adrianN 7y ago
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.
- guerrilla 7y ago
  Good thing that's not relevant in general then.