Ytukyg

Is the example below a correct definition of a semigroup?

instance Semigroup (CurrencyAmount Fixed2) where

  (<>) (CurrencyAmount a c) (CurrencyAmount _ EMPTY) = CurrencyAmount a c

  (<>) (CurrencyAmount _ EMPTY) (CurrencyAmount a c) = CurrencyAmount a c

  (<>) (CurrencyAmount a c1) (CurrencyAmount b c2) | c1 == c2 = CurrencyAmount (a + b) c1

  (<>) _ _ = error "currency mismatch"

I suppose this is a matter of semantics. The formal and classical mathematical definition of a Semigroup (A,<>) does requires <> to be a function <>:A×A→A, therefore total. But what is your set A? You need to establish some (naive) set theoretical based semantics for the (Haskell) types and functions you're working with.

• If the denotation of your types are carrier sets that include ⊥ as an element, then your Haskell functions will be interpreted as total mathematical functions. In this case you just have to make sure the required laws hold for all elements including ⊥. And in your case they do.




• If instead you consider a model of sets (without ⊥) and partial functions, then to match the classic formal mathematical definition of Semigroup you'd need to make sure <> is total in that setting. And in your case it isn't.

I don't know whether there is a fixed convention. The second, stricter interpretation seems preferable. But the first is a sensible generalisation.

That said have you considered the possibility of using GADTs to distinguish between different currencies at the type level?

I don't think it's valid.

Most of the lawful type classes in Haskell (e.g. Semigroup, Monoid, Functor, Monad, etc.) derive their laws from mathematics (e.g. category theory).

Mathematics is based on axioms; that is, assertions about the underlying fabric of numbers, geometry, and similar. By definition, axioms can't be proven, but you usually accept them because they make intuitive sense (e.g. the Peano axioms). In a sense, mathematics is built on a foundation of intuition.

The reason that type classes like the above are lawful is that the laws ensure that the instances behave like you'd expect them to behave.

In Haskell, there's great emphasis on being able to reason about the code, mostly by just looking at the type signatures of functions. One reason you, as a reader, can feel confident about doing this is that whenever a lawful type class is involved, you know that it'll behave in a non-surprising manner.

Most mathematical functions are total (there are exceptions, e.g. division by zero, but exceptions should be drawn from mathematics itself). In light of the above, I'd argue that there's a strong implicit expectation that a type class that derives its laws from mathematics is expected to be total.

The above instance isn't total, which means that it'll behave in a surprising manner for certain inputs. I wouldn't consider it a valid Semigroup instance.