Class updates

[garyb]

Resolves #61, #62

I went with the name EuclideanRing rather than EuclideanDomain, it seemed to fit better with our other Ring-terminology classes, and seems to be an acceptable name for the structure also.

Re: HeytingAlgebra. I did go with largest and smallest in the end. Although that strays from truth terminology it shouldn't really matter, as it's a lattice too, and from that point of view those names are just as reasonable.

I also added the Kleene 3VL for Ordering... it's true that (&&) and (||) don't make a whole lot of sense from an ordering point of view, but it certainly satisfies the necessary laws. If it still seems like a bad idea that's fine, I can take it out again.

[paf31]

👍 Thanks for working on these. Looks great to me, for the most part:

I would keep the standard names, honestly, and I'd probably pick something like truth and falsehood for HeytingAlgebra, or tt and ff if we wanted terse names. As for the three-valued logic, I think it would be better to leave that for a library. Is there a reason to include it in Prelude? It doesn't really belong with Ordering, and the only connection seems to be that both types have three values.

[garyb]

I wasn't suggesting we use Ordering as a 3VL, only that by treating it as one we get a fully law abiding instance. The motivation is not again, as especially with a (HeytingAlgebra b) => HeytingAlgebra (a -> b) instance there are some nice things that can be done. I guess my point is: there is a lawful instance, it's sometimes useful, so why not?

I'm not sure I agree that true and false are necessarily better terms that top and bottom or largest and smallest... given that it's a bounded lattice with implication operation here, which doesn't seem especially truthy in particular. But anyway I've realised, it doesn't matter! My concern was about cluttering up the namespace of anyone who imports the Prelude (given that one and two letter names are the common for local variables), but since the Prelude is re-exporting now, I can just not import tt / ff and that can be avoided.

[paf31]

Given the existence of Down to turn an ordering around, I'd prefer not to add a potentially confusing HeytingAlgebra Ordering instance to Prelude. What's a case where you'd use not with the function instances? I suspect it'd be just as simple to use Down in those cases.

[paf31]

Also, why not reuse the names top and bottom, since they're in different modules anyway?

[garyb]

Yeah, I guess, or not Down but invert:

xs' = sortBy (not compare) xs
xs' = sortBy (\x -> invert <<< compare x) xs

The first is still much nicer though 😉

I think I'd rather go with tt / ff than introduce an alternative top / bottom, as then the question will be why it isn't just Bounded in the first place.

edit: invert not reverse

[paf31]

It's shorter, but I don't know if it's nicer. I would find it quite hard to figure out exactly which HeytingAlgebra the not referred to.

I don't think the existence of an involution which happens to be not for some unrelated HeytingAlgebra is enough to justify the instance.

I think I'd rather go with tt / ff than introduce an alternative top / bottom, as then the question will be why it isn't just Bounded in the first place.

Well, at least we know the answer 😄 I'm not fussed either way though.

[garyb]

Ok, it's gone.

How does the rest of it look, in particular I wanted to check that:

• degree a = |a| for Int
• implies = eq for Boolean

Are good implementations?

[paf31]

p ==> q = not p || q, so

implies true true = true
implies false true = true
implies true false = false
implies false false = true

The degree implementation is good, see https://en.wikipedia.org/wiki/Euclidean_domain#Examples.

[garyb]

Oops, that's actually what I used for the 3VL too as I found it elsewhere... thanks.

[paf31]

This looks good to me, but I'd be very grateful if @jonsterling and/or @freebroccolo would take a look the at the new hierarchy before it gets merged.

[garyb]

Oh, too late 😄 but we can always change stuff again while it's still in RC mode.

[paf31]

Oh haha, I should have looked first. That's fine, as you say, we're still only at RC 2.