semiquot

Stream: general

[Mario Carneiro]

A minor advertisement for data/semiquot because I think it's a cool idea. I've mentioned this approach before, but this data type makes it easy to work with nondeterministic functions using quotient types.

An application is in fp/basic, floating point numbers. Previously, we had to keep track of messy NaN payload data, which is not reliably handled across different processors, causing some unavoidable nondeterminism. Now, there is only one NaN value, and functions that leak NaN payload data (like float.sign) are semiquot so that they are allowed to return anything in that case. (We don't currently have a float.bits function that gives the bitwise representation of a float, but that would of course leak NaN payload data so it would also be semiquot.)

[Patrick Massot]

Is this meant only for programming or could be useful for maths?

[Mario Carneiro]

It has some interesting mathematical structure, being an ordered monad with some filter-like closure properties, but in classical lean it is equivalent to the collection of nonempty subsets of A

[Mario Carneiro]

It's most interesting when viewed constructively

[Patrick Massot]

Ok, thanks for confirming I was not in the target audience of this message.

[Mario Carneiro]

I think the correct answer is it is meant for verified programming, which of course involves both programming and math, but the math is probably not so interesting to you

[Patrick Massot]

Thanks for the advertisement anyway, I think it's a good idea to advertise each new stuff in mathlib here