search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 644 forks source link

Move `abs` out of the `Neg` interface: not every number has a positive-definite absolute value. #3500

Closed Niriel closed 6 years ago

Niriel commented 7 years ago

I am writing modules to implement Dual and Split-Complex numbers. Unlike Real or Complex numbers, we have to be extremely careful with the use of the words "absolute value" and "modulus".

Reals, complex, dual, split-complex, quaternions, octonions, biquaternions and combinations thereof have a "modulus" property that derives from the notion of conjugation. Said modulus may not always be positive (split-complex). If the modulus is positive, it may still not be positive-definite (dual). Only when the modulus has all the required properties can it be promoted to "absolute value". Some of these numbers do not have an absolute value, only a modulus, even though they can be negated.

Matrices and tensors can also be negated, but even the notion of modulus is ill-defined, bringing us one more step farther from an absolute value.

I would like to suggest that abs be taken out of Neg and placed into its own interface.

david-christiansen commented 7 years ago

This sounds reasonable to me. Will you please submit a pull request?

Niriel commented 7 years ago

I would, if I had a Linux machine. My laptop is dead, and my current windows desktop makes no sense to me. I'll install a Linux VM and try to do just that.

One worry, however: this will break some existing code. How do I deal with that?

david-christiansen commented 7 years ago

The right way to break existing code is to announce your intentions and reasons on the mailing list ahead of time, then make the change and submit a PR, then announce your intentions one more time prior to merging. Make sure that the file CHANGELOG contains a description of what happened and how to fix broken code so that it shows up in the release notes.

Niriel commented 7 years ago

All right, I've got my VirtualBox. Getting to work.

ahmadsalim commented 6 years ago

@Niriel Any update?

Niriel commented 6 years ago

Yeah. The change was trivial and I got Idris to compile with an Abs interface separated from Neg. Here are my commits from last year which implement this fix.

https://github.com/Niriel/Idris-dev/commits/absolute_value

I haven't made a Pull Request because the Google Groups discussion didn't reach a conclusion.

https://groups.google.com/d/msg/idris-lang/DXDbM50_Wug/jLP2fN30CQAJ

In short: Prelude makes simplifications for the sake of convenience. Making a correct algebraic tower would ideally be better than including small patches like mine but it's a hard job. However, small improvements may be better than nothing.

I don't know, guys. I'm a noob, I can't predict the implications of this change. My branch is one year old; I can make it up to date if you want.

ahmadsalim commented 6 years ago

@Niriel Yeah, I can not find any major complains against it. You are welcome to update the PR if you like.

Niriel commented 6 years ago

Working on it. New laptop, needs some new ssh keys and all.

Niriel commented 6 years ago

I've updated my branch to match the latest master. It compiles, but I don't manage to run the tests. make test ends with "For running the test suite against Node, node must be installed.". I don't know what it means. I didn't add any test myself, I'm just trying see if I broke anything (would be weird, but ok).

ahmadsalim commented 6 years ago

@Niriel Just use make test_c please. Also you are welcome to open a PR with the updates, then we can check whether they broke anything with travis afterwards.

Niriel commented 6 years ago

Same problem with test_c. Actually my problem is two-fold. make compiles idris and installs it into a cabal sandbox

neel@spacetime:~/sources/idris/dev$ which idris
./.cabal-sandbox/bin/idris

but make test and make test_c both expect an executable idris in dist/build/idris/. So I create that directory and a symbolic link.

neel@spacetime:~/sources/idris/dev/dist/build/idris$ ln -s `which idris` idris

And then, both make test and make test_c do find the executable but then complain about Node, whatever that is. "For running the test suite against Node, node must be installed."

justjoheinz commented 6 years ago

Just for your interest:

node is a server side runtime for Javascript, required in the test suites to test against the javascript code backend. see http:/nodejs.org

As for getting the tests to run itself, I cannot help you, as I have no experience in compiling and testing idris

Markus

2017-11-12 12:43 GMT+01:00 Niriel notifications@github.com:

Same problem with test_c. Actually my problem is two-fold. make compiles idris and installs it into a cabal sandbox

neel@spacetime:~/sources/idris/dev$ which idris ./.cabal-sandbox/bin/idris

but make test and make test_c both expect an executable idris in dist/build/idris/. So I create that directory and a symbolic link.

neel@spacetime:~/sources/idris/dev/dist/build/idris$ ln -s which idris idris

And then, both make test and make test_c do find the executable but then complain about Node, whatever that is. "For running the test suite against Node, node must be installed."

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/idris-lang/Idris-dev/issues/3500#issuecomment-343731188, or mute the thread https://github.com/notifications/unsubscribe-auth/AAX75ETSsCDsghzQcCTUcIxKqC0YHkp_ks5s1tnJgaJpZM4KcH9o .

ahmadsalim commented 6 years ago

@Niriel Yeah, it seems that the tests require nodejs anyway. Just open a PR please then and then we can see whether they fail via Travis.

jfdm commented 6 years ago

Idris ships with two codegens: the C reference codegen; and a JS codegen. The test suite checks to see if you have node installed prior to running the tests. In the past, if we do not check for node when accepting updates to tests the expected results can become mangled.

We should really make sure the test runs only when running the JS tests, but I am not sure how to achieve this with the current test setup.

Niriel commented 6 years ago

Thanks for explaining this Node business. I'll see if I can install it.

I opened the pull request.

jfdm commented 6 years ago

@Niriel to be honest, you don't need to install node, our CI infrastructure will run the required tests for the JS codegen. We normally ask people to run tests prior to merging to identify faults quicker. In this case, if you can get the shipped libraries to compile with your changes using default idris, then that is reasonable to me. Our CI tests will pick anything outstanding.

corazza commented 6 years ago

Congratulations @Niriel, your mathematical pedantry broke the Idris book:D (pg. 197)

Niriel commented 6 years ago

@corazza > There's an Idris book? Where?

corazza commented 6 years ago

@Niriel here! https://www.bookdepository.com/Type-driven-Development-with-Idris-Edwin-Brady/9781617293023

I haven't read a lot of programming books (near) cover-to-cover, but I still have to say how good this one is. It covers a large breadth of concepts but things build upon each other, they aren't just thrown at you. Excellent intuition-building. Focus is on practical aspects of development but theoretical concepts are touched upon and contextualized, really nice read buy it haha (although I suppose most people here are already experts and don't have much to gain?)