mathstructs.hs

{-# LANGUAGE NoImplicitPrelude #-}

import Data.Bool (Bool, (&&), (||))
import Numeric.Natural (Natural)
import Prelude (Int, (+), (-))

{- |
마그마(Magma)는 집합과 '닫힌' 이항 연산자 (이항 연산의 결과가 집합에 속함)

(𝕄, •) ⊢ ∀ a, b ∈ 𝕄 ⟹ a • b ∈ 𝕄.
-}
class Magma a where
    (•) :: a -> a -> a

-- | 마그마의 예시는 자연수와 덧셈 (ℕ, +)
instance Magma Natural where
    (•) :: Natural -> Natural -> Natural
    (•) = (+)

{- |
유사군(QuasiGroup)은 집합의 모든 원소에 대한 이항 연산의 결과가
라틴 방진 (n개의 원소만 쓰는 n x n 마방진)을 이루는 마그마

(Q, ∗) ⊢ ∀ a, b ∈ Q, ∃! x, y ∈ Q ⟹ a ∗ x = b ∧ y ∗ a = b
-}
class (Magma a) => Quasigroup a where
    (//) :: a -> a -> a
    (\\) :: a -> a -> a

{- |
유사군의 예시는 정수와 뺄셈(ℤ, -), 또는 {1, -1}과 곱셈

+----+----+----+
|  * | -1 |  1 |
+----+----+----+
| -1 |  1 | -1 |
+----+----+----+
|  1 | -1 |  1 |
+----+----+----+
-}
instance Quasigroup Natural where
    (//) :: Natural -> Natural -> Natural
    (//) = (-)
    (\\) :: Natural -> Natural -> Natural
    (\\) = (-)

instance Magma Bool where
    (•) :: Bool -> Bool -> Bool
    (•) = (&&)

instance Quasigroup Bool where
    (//) :: Bool -> Bool -> Bool
    (//) = (||)
    (\\) :: Bool -> Bool -> Bool
    (\\) = (||)

{- |
Unital Magma는 단위원을 가지는 마그마

(𝕄, •, e) ⊢ ∀ a ∈ 𝕄 ⟹ a • e = e • a = a
-}
class (Magma a) => UnitalMagma a where
    e :: a

instance UnitalMagma Natural where
    e :: Natural
    e = 0

{- |
루프(Loop)는 단위원을 가지는 유사군
-}
class (Quasigroup a) => Loop a

{- |
반군(Semigroup)은 결합법칙을 만족하는 마그마

(𝕊, •) ⊢ ∀ x, y, z ∈ 𝕊 ⟹ (x • y) • z = x • (y • z)
-}
class (Magma a) => Semigroup a

{-|
모노이드(Monoid)는 단위원을 가진 반군 (결합법칙 + 단위원)

(𝕄, •, e) ⊢ ∀ a ∈ 𝕄 ⟹ a • e = e • a = a
-}
class (Semigroup a) => Monoid a

{-|
Associative Quasigroup는 유사군과 반군을 동시에 만족하는 마그마
(= '나눗셈' + 결합법칙)

-}
class (Quasigroup a, Semigroup a) => AssociativeQuasigroup a

{-|
군은 역원이 존재하는 모노이드

(𝔾, •, e, ⁻¹) ⊢ ∀ a ∈ 𝔾 ⟹ a • a⁻¹ = a⁻¹ • a = e
-}
class (Loop a, AssociativeQuasigroup a, Monoid a) => Group a