Written in Idris2: a demo of non-Euclidean geometry using WebGL

[James Cook]

I just published something I had a lot of fun making: a demo of
non-Euclidean geometry using WebGL (written in Idris2, of course).

See the blog post:

https://www.falsifian.org/blog/2022/01/17/s3d/

Or the source:

https://sr.ht/~falsifian/s3d/

It makes heavy use of the idris2-dom library.

Other notes:
* It includes a library for constructive solid geometry. You probably
don't want to use it, because I don't really know what I'm doing, but
I had fun making it.
* It requires this unmerged pull request:
https://github.com/idris-lang/Idris2/pull/2100
If there's anything I could do to get that merged let me know!
Alternatively, if you don't think it's a good idea, I can try to work
around the issue, but it will be tricky because List.length is being
called through a library rather than directly by my own code.

--
James

[James Cook]

On Tue, Jan 18, 2022 at 04:43:44AM +0000, James Cook wrote:
> I just published something I had a lot of fun making: a demo of
> non-Euclidean geometry using WebGL (written in Idris2, of course).
>
> See the blog post:
>
> https://www.falsifian.org/blog/2022/01/17/s3d/
>
> Or the source:
>
> https://sr.ht/~falsifian/s3d/

It's possible some of the modules I wrote could be useful for others.
I didn't really bother checking whether they already exist in other
packages. All are at https://git.sr.ht/~falsifian/s3d/

* Data.DefaultMap: A map with a default value. A key not having a value
is the same as a key having the default value.
* Data.Linear.SizedArray: Arrays with the length in the type.
(The handling of numbers is hacky and optimized for speed.)
* Math.LinearAlgebra has some vector and matrix stuff. It could use some
cleaning up, though. Especially the matrix inverse implementation.
* SolidGeometry: I don't know if I should recommend using this, but it's
an implementation of constructive solid geometry that worked well enough
for my purposes.
* Test.TestTree: I hacked this together to organize my unit tests.

--
James