wtf wrote: ↑Fri Nov 29, 2019 12:53 am
In the Mython interpreter, the Boolean expression

evaluates to True

How can somebody who claims to understand Homotopy Type Theory be so ignorant of

Type Systems?!?

I am going to do this in C++ so that you can convince yourself this has nothing to do with Python or Interpreted languages.

I can do it in Haskell too if you are going to fuss about "pure functions".

This is about

polymorphism and the meaning of the "==" operator when applied to incompatible types. Comparing a String to an Integer is a meaningless notion unless you implement an

Identity Type that does it.

In intensional type theory under the propositions as types paradigm, an identity type (or equality type) is the incarnation of equality. That is, for any type A and any terms x,y:A, **the type IdA(x,y) is “the type of proofs that x=y” or “the type of reasons why x=y”**.

In this particular case you want a function which takes (String, Integer) as inputs and returns a Boolean. This is called a

Type signature.

https://repl.it/repls/BiodegradablePleasedBit
Code: Select all

```
#include <iostream>
using namespace std;
bool identity(string a, int b) {
/* magic sauce required here by the Genius-Mathematician */
return 0;
};
int main() {
string a = "0000";
int b = 4;
cout << identity(a, b) << endl;
return 0;
}
```

This is the practical implication of the Curry-Howard isomorphism.

**0000 == 4 => True** is a proposition. You need to prove that proposition by writing the implementation of the

**bool identity(string a, int b)** function above.

So go right ahead and prove it.