[kazinator]

I don't see how support for multiple equalities makes something not a functional language.

Functional doesn't mean "the semantics of everything is tied to its printed syntax" so that if two things look the same in the syntax, they denote the same thing. (Right?)

Suppose we take Haskell and give it an equal operator which can tell that two bignums are different instances and not equal. Does it cease being functional? What if we don't use that operator anywhere in a program and don't even know it exists; how do we know the language is not functional?

[catnaroek]

> Functional doesn't mean "the semantics of everything is tied to its printed syntax" so that if two things look the same in the syntax, they denote the same thing. (Right?)

I don't care about syntax. I want to manipulate the values I care about, not object identities. I want to operate on numbers, strings, lists, trees, what have you. Not memory cells that allegedly contain representations of numbers, strings, lists, trees, what have you. This is strictly a semantic issue.

> I don't see how support for multiple equalities makes something not a functional language.

FWIW, what most languages call “physical” or “reference equality” is a special case of structural equality (which is always the prior notion). Structural equality of mutable cells (which have dedicated types in Haskell and ML) happens to be physical equality.

> Suppose we take Haskell and give it an equal operator which can tell that two bignums are different instances and not equal. Does it cease being functional?

Yes.

> What if we don't use that operator anywhere in a program and don't even know it exists; how do we know the language is not functional?

Then you're doing functional programming in a non-functional language.

[junke]

> What if we don't use that operator anywhere in a program and don't even know it exists; how do we know the language is not functional?

;-)

If a tree falls in a forest and no one is around to hear it, does it make a sound?

If a program satisfies a property but the compiler cannot prove it, can we still rely on it?

[catnaroek]

> If a program satisfies a property but the compiler cannot prove it, can we still rely on it?

It's very simple: You can rely on what you can prove. This applies both to compiler authors and compiler users. That sometimes one can prove things the other can't shouldn't come off as a surprise. Neither party has all the information: The compiler author doesn't know the intended meaning of the program submitted to the compiler by the user. The user doesn't (need to) know the internal details of how the compiler works.